AWS has announced the general availability of its Graviton5 processor, powering new EC2 M9g and M9gd instances. The chip doubles Graviton4's core count to 192, moves to TSMC's 3nm process, and delivers up to 25% better compute and 35% faster ML inference. The standout feature is the sixth-generation Nitro System's new Nitro Isolation Engine (NIE), a formally verified separation kernel written in Rust whose sole purpose is isolating VMs from each other. AWS used the Isabelle/HOL proof assistant to produce 330,000 lines of machine-checked mathematics proving the kernel's correctness — making it the first such formally verified component shipping in a production commercial cloud. The Nitro hypervisor still handles policy but must now request the NIE to perform any operation touching guest state. AWS is positioning Graviton5 for agentic AI workloads, with Meta, Snowflake, and Uber among early adopters.
