---
title: "AWS can now mathematically prove your VMs are isolated"
url: https://daily.dev/posts/aws-can-now-mathematically-prove-your-vms-are-isolated-lyck4ka1b
source_url: https://thenewstack.io/graviton5-nitro-isolation-engine
type: article
source: "The New Stack"
published: 2026-06-10T16:53:59.846Z
updated: 2026-06-10T16:54:22.696Z
tags: ["security", "aws", "infrastructure", "rust"]
reading_time: 4
upvotes: 0
comments: 0
language: en
---

> ## Documentation Index
> Fetch the complete documentation index at: https://daily.dev/llms.txt
> Use this file to discover all available pages before exploring further.

# AWS can now mathematically prove your VMs are isolated

**[The New Stack](https://daily.dev/sources/newstack)** · 4 min read · 0 upvotes · 0 comments

## Summary

AWS has announced the general availability of its Graviton5 processor, powering new EC2 M9g and M9gd instances. The chip doubles Graviton4's core count to 192, moves to TSMC's 3nm process, and delivers up to 25% better compute and 35% faster ML inference. The standout feature is the sixth-generation Nitro System's new Nitro Isolation Engine (NIE), a formally verified separation kernel written in Rust whose sole purpose is isolating VMs from each other. AWS used the Isabelle/HOL proof assistant to produce 330,000 lines of machine-checked mathematics proving the kernel's correctness — making it the first such formally verified component shipping in a production commercial cloud. The Nitro hypervisor still handles policy but must now request the NIE to perform any operation touching guest state. AWS is positioning Graviton5 for agentic AI workloads, with Meta, Snowflake, and Uber among early adopters.

## Full article

daily.dev links to this article rather than hosting it. Read it at the original source: <https://thenewstack.io/graviton5-nitro-isolation-engine>

## Similar posts on daily.dev

- [EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation](https://daily.dev/posts/ec2-s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolat-xondxkppx) · Lobsters · 0 upvotes · 0 comments
- [AWS Introduces Fifth-Generation Graviton Processor with M9g Instances](https://daily.dev/posts/aws-introduces-fifth-generation-graviton-processor-with-m9g-instances-yy6tpeuay) · InfoQ · 0 upvotes · 0 comments
- [AWS Graviton5 Reaches General Availability with 192 Cores and Formally Verified VM Isolation](https://daily.dev/posts/aws-graviton5-reaches-general-availability-with-192-cores-and-formally-verified-vm-isolation-kxxfhheec) · InfoQ · 0 upvotes · 0 comments
- [With Graviton5, AWS Promises a 25% Performance Boost](https://daily.dev/posts/with-graviton5-aws-promises-a-25-performance-boost-o7r1g2rhv) · The New Stack · 0 upvotes · 0 comments

---

Tags: [#security](https://daily.dev/tags/security), [#aws](https://daily.dev/tags/aws), [#infrastructure](https://daily.dev/tags/infrastructure), [#rust](https://daily.dev/tags/rust)

[View this post on daily.dev](https://daily.dev/posts/aws-can-now-mathematically-prove-your-vms-are-isolated-lyck4ka1b)