# [How formal verification makes AWS Nitro the first formally verified cloud hypervisor - Amazon Science](https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation)
Today we announced the general availability of the new M9g and M9gd instances of Amazon Web Services’ (AWS’s) Elastic Compute Cloud (EC2), the first instance types powered by Graviton5, the latest generation of our general-purpose CPU. Graviton5 doubles the number of cores from the previous generation, from 96 to 192.
They’re also the first instance types to use the new Nitro Isolation Engine, a component of the Nitro Hypervisor whose sole job is isolating virtual machines (VMs) from each other. In this post, we explain how we used the Isabelle/HOL (higher-order logic) proof assistant — software that mechanically checks reasoning steps for adherence to the laws of logic — to prove that the Nitro Isolation Engine behaves correctly and enforces isolation between virtual machines. The Nitro Isolation Engine is the critical component of the first formally verified hypervisor to be deployed in a commercial cloud environment.
Our Isabelle/HOL model and proof comprise 330,000 lines of machine-checked mathematics. It’s comparable in scale to seL4, the landmark project that first demonstrated that realistic operating-system verification was feasible and was an inspiration for our own work. However, unlike seL4, the Nitro Isolation Engine is designed for a commercial cloud environment and ships on production hardware as an always-on feature for Graviton5 users.
Our talk at Amazon’s 2025 re:Invent conference introduces our formal-verification methodology. This blog post gives an informal overview of the main aspects of our formal-verification work and how they fit together.
## What is a separation kernel?
What is a separation kernel?
John Rushby coined the term “separation kernel” in 1981 to describe a minimal OS component that partitions a system into isolated compartments. The key idea: separate policy from mechanism. A separation kernel does not decide what to isolate, how to allocate resources, or which VMs to schedule: those decisions are made elsewhere. Instead, it focuses solely on enforcing isolation, and this clarity of purpose makes separation kernels much simpler to implement than full OS kernels.
Since its introduction in 2017, the Nitro Hypervisor has been responsible for enforcing isolation in EC2, but it also handles business logic, device drivers, and AWS-specific features. That complexity makes proving correctness much more difficult. Moreover, the Nitro Hypervisor was not designed for verification from the start.
Distilling the hypervisor’s critical isolation logic into a minimal component, the Nitro Isolation Engine, makes it small enough to verify and audit, giving customers unprecedented visibility into how isolation is enforced. We also wrote the Nitro Isolation Engine in Rust, a language that lends itself more naturally to formal verification.
The Nitro Hypervisor still handles policy — VM creation, resource allocation, migration, scheduling — but it is now deprivileged and must ask the Nitro Isolation Engine to perform any operation touching guest state. The Nitro Isolation Engine checks every request before acting.
## Specifications and proofs
Specifications and proofs
The two key parts of our work are specifications and proofs. Formal specifications precisely capture the expected behavior of the system, and proofs establish that the implementation meets those specifications.
Our theorems about the Nitro Isolation Engine address four types of properties:
…
EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation Lobsters: https://lobste.rs/s/efnxre/ec2_s_formally_verified_isolation_engine