Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Big news from Amazon Web Services


view this post on Zulip Email Gateway (Dec 04 2025 at 19:16):

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