Dear colleagues,

At AWS re:Invent 2025 in Las Vegas, we announced the AWS Nitro Isolation Engine [1, 2, 3], a formally verified enhancement to the AWS Nitro System that enforces isolation between virtual machines hosted on AWS's new Graviton5-based EC2 instances.

Nitro Isolation Engine represents a significant deployment of mechanized proof in production infrastructure, and we therefore wanted to bring this to the attention of the formal methods and programming languages communities. This work builds directly on decades of advances in interactive theorem proving, program verification, and programming languages theory, alongside landmark projects—such as, seL4 [4], CertiKOS [5], SeKVM [6], and many others—that were inspirations for this work.

What is Nitro Isolation Engine?
Nitro Isolation Engine is a small, trusted computing base written in Rust that sits beneath the AWS Nitro Hypervisor, providing a security isolation boundary between the hypervisor and guest virtual machines, and between co-tenanted guest virtual machines. The Nitro Isolation Engine controls the critical hardware features required for isolating customer workloads, primarily control of Stage Two translation tables.

The verification effort
Nitro Isolation Engine was designed with verification in mind from the first line of code. Nitro Isolation Engine is subject to AWS’s existing rigorous engineering practices, including the deployment of property-based-testing and lightweight formal methods, for example the Kani bounded model checker for Rust [7].

Building atop this foundation, we have specified and verified the correctness of Nitro Isolation Engine in Isabelle/HOL [8]. Our model and proofs consist of around 260,000 lines of machine-checked models and proofs. Specifically, we have proved:

Functional correctness: Nitro Isolation Engine behaves as specified for all operations: virtual machine creation, memory mapping, instruction and data abort handling, and so on. As corollaries of our total verification style, we have also proven memory-safety, termination, and absence of runtime errors, providing our modelling assumptions are accurate.
Confidentiality: We prove a noninterference-style property demonstrating the confidentiality of guest virtual machine states, formalized as indistinguishability preservation up-to permitted flows of declassified information out of a guest.
Integrity: The integrity of guest virtual machine state is formalized as a safety property, showing that the private state of one virtual machine is unaffected by operations modifying another distinct virtual machine.
In addition, we have applied Iris [9] and Verus [10] to prove the correctness of the Nitro Isolation Engine’s concurrency primitives, including ticket locks, mutexes, and rendezvous barriers.

For functional verification, we defined μRust, a restricted subset of Rust expressive enough to write Nitro Isolation Engine but amenable to formal reasoning and embedded its semantics into Isabelle/HOL. Specifications are written in separation logic, and proofs proceed via weakest precondition calculus with custom automation. We have made our verification infrastructure open source as the AutoCorrode library [11] for Isabelle/HOL, which may be of independent interest.

Regards,
Automated Reasoning Group, AWS

[1]: https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U https://www.youtube.com/watch?v=3Gt-30Fm38U
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]: https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode