---
title: "EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation"
description: "AWS has introduced M9g and M9gd EC2 instances powered by Graviton5 CPUs, featuring the formally verified Nitro Isolation Engine to enforce virtual machine isolation. To prove the engine's correctness, engineers developed 330,000 lines of machine-checked mathematics using the Isabelle/HOL proof assistant. The system architecture separates hypervisor policy from isolation mechanisms, requiring the deprivileged Nitro Hypervisor to route all guest state modifications through the minimal Rust-based engine. Functional verification uses a restricted language subset called micro Rust, Separation Logic contracts specifying total correctness, and weakest-precondition calculus from the open-source AutoCorrode library. Finally, high-level transition relations and noninterference proofs ensure that memory integrity and guest confidentiality are preserved across every execution step."
---

# EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation

amazon.science · Dominic Mulligan, Nathan Chong · Jun 10, 2026

**Type:** Announcement

## Summary

AWS has introduced M9g and M9gd EC2 instances powered by Graviton5 CPUs, featuring the formally verified Nitro Isolation Engine to enforce virtual machine isolation. To prove the engine's correctness, engineers developed 330,000 lines of machine-checked mathematics using the Isabelle/HOL proof assistant. The system architecture separates hypervisor policy from isolation mechanisms, requiring the deprivileged Nitro Hypervisor to route all guest state modifications through the minimal Rust-based engine. Functional verification uses a restricted language subset called micro Rust, Separation Logic contracts specifying total correctness, and weakest-precondition calculus from the open-source AutoCorrode library. Finally, high-level transition relations and noninterference proofs ensure that memory integrity and guest confidentiality are preserved across every execution step.

## Context

The Nitro Hypervisor historically handled VM isolation alongside complex business logic, device drivers, and AWS-specific features, making formal correctness proofs difficult because the hypervisor was not designed for verification from the start.

## Approach / What changed

AWS distilled critical isolation logic into the Nitro Isolation Engine, a minimal separation kernel written in Rust that checks every guest state operation requested by the deprivileged hypervisor. Correctness was proved using 330,000 lines of Isabelle/HOL machine-checked mathematics, applying micro Rust semantics, Separation Logic contracts, weakest-precondition calculus via the AutoCorrode library, and noninterference proofs.

## Takeaways

- The Nitro Isolation Engine decouples isolation mechanisms from policy logic, leaving VM creation, resource allocation, and scheduling to the deprivileged Nitro Hypervisor.
- AWS formalized micro Rust, a restricted subset of Rust excluding traits and dynamic dispatch, with shallow embedding in Isabelle/HOL to make low-level code amenable to formal proofs.
- Confidentiality and integrity are mathematically guaranteed through noninterference, ensuring that two indistinguishable system states remain indistinguishable after state transitions.

**Tags:** [Architecture](https://yomu.fyi/topic/architecture), [AWS](https://yomu.fyi/topic/aws), [Open Source](https://yomu.fyi/topic/open-source), [Reliability](https://yomu.fyi/topic/reliability), [Rust](https://yomu.fyi/topic/rust)

- Source: [amazon.science](https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation)
- Source URL: https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation
- Ingested by Yomu: 2026-08-27T15:23:43.472Z

[Read original post](https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation)