Isabelle/HOL, the Proof Assistant Behind the Nitro Isolation Engine

At re:Invent 2025, AWS unveiled the Nitro Isolation Engine (NIE) and announced that the security and correctness of this module were formally verified using Isabelle/HOL. NIE is introduced as the world's first formally verified cloud hypervisor, setting a new standard for cloud security.

Isabelle/HOL was chosen for its excellent balance of expressiveness, automation, proof readability, and scalability. The author walks through the levels of mathematical logic in order, from Boolean logic to first-order logic, higher-order logic, and dependent-type theories, summarizing that as expressiveness increases, automated proof becomes harder, but proof assistants bridge that gap.

The NIE verification used approximately 250,000 lines of formal proof, which included the Graviton-5 architecture specification, functional correctness proofs for the Rust code implementing hypercalls, and proofs of security properties. To accomplish this, the team implemented separation logic on top of Isabelle/HOL and leveraged both built-in automation and their own custom proof automation. As a result, this massive proof runs robustly and efficiently, completing in about 30 minutes on a regular laptop.

The strengths of Isabelle/HOL are cited as follows.

• User-configurable parser: allows a significant portion of Rust to be embedded in specifications
• type classes: provide natural overloading not only for numeric types but also for things like machine words
• locales: a lightweight module system for flexibly organizing specification hierarchies
• built-in automation: simplification, backchaining proof search
• Sledgehammer: one-click integration with external automated theorem provers
• counterexample-finding tools: quickly discover incorrect propositions
• code generation: generate code from executable higher-order logic specifications and use it for testing

A notable prior case cited is the verification of the seL4 microkernel. Isabelle has also been used in formalizing WebAssembly semantics, the Cogent verification framework, verification of CRDT algorithms used in distributed editing, verification of cryptographic protocols, and formalization of mathematical theorems. Isabelle is free and open source and runs on major operating systems.