From: Lawrence Paulson <lp15@cam.ac.uk>
I am forwarding the following announcement, which Dominic Mulligan posted to LinkedIn earlier today. I played a part myself, but it was mainly to be chief kibitzer.
Larry
Over three years, lots of hard work, and 260,000 lines of Isabelle/HOL code later, the Nitro Isolation Engine (NIE) is finally announced alongside Graviton5.
Working with our colleagues in EC2, Annapurna, and AWS AppSec, we have been working to rearchitect the Nitro system for Graviton5+ instances around a small, trusted separation kernel. Written from scratch in Rust, we have additionally specified the behaviour of a core subset of the Nitro Isolation Engine kernel, verified that the implementation meets this specification, and additionally proved deep security properties—confidentiality and integrity—of the implementation.
Congratulations to all ARG team members and our colleagues in EC2, Annapurna, and AWS AppSec.
https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
Last updated: Dec 21 2025 at 20:24 UTC