AWS just rolled out M9g and M9gd EC2 instances powered by Graviton5 CPUs, doubling previous core counts from 96 to 192. Alongside the hardware boost, they’ve shipped the Nitro Isolation Engine—a slimmed-down component of the Nitro Hypervisor dedicated solely to keeping virtual machines completely separate. The team modeled that engine in Isabelle/HOL, producing 330,000 lines of machine-checked proofs. That scale matches seL4’s verification, but this is the first time a formally verified hypervisor component has gone live in a commercial cloud. They broke the work into two halves: functional correctness (including no runtime errors or memory safety issues) and confidentiality/integrity properties. For the former, they created a μRust subset minus traits and dynamic dispatch, embedded its semantics in Isabelle/HOL, then wrote specs in Separation Logic with pre- and post-conditions guaranteeing total correctness. A weakest-precondition calculus, backed by custom proof automation in their open-source AutoCorrode library, checks every μRust routine against those specs. On the confidentiality side, they specified atomic high-level transitions for each hypercall, linked that to the low-level logic via refinement, and proved noninterference—ensuring no unauthorized information flows between VMs. The Nitro Hypervisor still handles VM creation, scheduling and resource allocation, but any operation touching guest state must go through the new Isolation Engine. That engine inspects every request against the formal spec before acting. Customer instances now run on production hardware with this always-on verified guard. At re:Invent 2025 they’ll dive deeper into the methodology, and their forthcoming white paper spells out assumptions, scope and proof details.