# EC2's formally verified "isolation engine" provides mathematical assurance of virtual-machine isolation

DevFeed: [EC2's formally verified "isolation engine" provides mathematical assurance of virtual-machine isolation](<https://devfeed.tech/articles/ec2-s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation-7598.md>)

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

Author: Dominic Mulligan; Nathan Chong

Published: 2026-06-10T15:00:00Z

Content type: article

Language: en

Sources: [Amazon Science homepage](<https://devfeed.tech/sources/amazon-science-homepage.md>)

Topics: [Amazon EC2](<https://devfeed.tech/topics/amazon-ec2.md>), [Rust formal verification](<https://devfeed.tech/topics/rust-formal-verification.md>)

Tags: [amazon-web-services-aws](<https://devfeed.tech/tags/amazon-web-services-aws.md>), [autocorrode-library](<https://devfeed.tech/tags/autocorrode-library.md>), [automated-reasoning](<https://devfeed.tech/tags/automated-reasoning.md>), [aws-graviton5-security](<https://devfeed.tech/tags/aws-graviton5-security.md>), [cloud-and-systems](<https://devfeed.tech/tags/cloud-and-systems.md>), [confidentiality-integrity-proofs](<https://devfeed.tech/tags/confidentiality-integrity-proofs.md>), [ec2-virtual-machine-security](<https://devfeed.tech/tags/ec2-virtual-machine-security.md>), [formal-verification](<https://devfeed.tech/tags/formal-verification.md>), [formally-verified-hypervisor](<https://devfeed.tech/tags/formally-verified-hypervisor.md>), [isabelle-hol-proof-assistant](<https://devfeed.tech/tags/isabelle-hol-proof-assistant.md>), [kernel](<https://devfeed.tech/tags/kernel.md>), [memory-safety-verification](<https://devfeed.tech/tags/memory-safety-verification.md>), [nitro-isolation-engine](<https://devfeed.tech/tags/nitro-isolation-engine.md>), [nitro-system](<https://devfeed.tech/tags/nitro-system.md>), [provable-security](<https://devfeed.tech/tags/provable-security.md>), [rust](<https://devfeed.tech/tags/rust.md>), [rust-formal-verification](<https://devfeed.tech/tags/rust-formal-verification.md>), [security](<https://devfeed.tech/tags/security.md>), [security-privacy-and-abuse-prevention](<https://devfeed.tech/tags/security-privacy-and-abuse-prevention.md>)

## AI overview

Amazon describes formally verifying the Nitro Isolation Engine, a separation-kernel component that enforces isolation between EC2 virtual machines. The verification uses Isabelle/HOL and is deployed as an always-on feature for Graviton5 users.

## Source excerpt

Splitting the "separation kernel" off from the rest of the Nitro security system and using only a subset of the Rust programming language to code it enabled its formal verification.