Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine

Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine - Amazon Science

Close

Close

Social

bluesky

threads

twitter

instagram

youtube

facebook

linkedin

github

rss

Menu

Research

Research areas

Automated reasoning

Cloud and systems

Computer vision

Conversational AI

Economics

Information and knowledge management

Machine learning

Operations research and optimization

Quantum technologies

Robotics

Search and information retrieval

Security, privacy, and abuse prevention

Sustainability

Our scientific contributions

Publications

Research from our scientists and collaborators.

Conferences

Our experts present and discuss cutting-edge research at scientific meetings globally.

Research areas

Automated reasoning

Cloud and systems

Computer vision

Conversational AI

Economics

Information and knowledge management

Machine learning

Operations research and optimization

Quantum technologies

Robotics

Search and information retrieval

Security, privacy, and abuse prevention

Sustainability

Our scientific contributions

Publications

Research from our scientists and collaborators.

Conferences

Our experts present and discuss cutting-edge research at scientific meetings globally.

News & blog

The latest from Amazon researchers

Amazon Science Blog

Technical deep-dives and perspectives from our scientists.

News

Research milestones and recent achievements.

The latest from Amazon researchers

Amazon Science Blog

Technical deep-dives and perspectives from our scientists.

News

Research milestones and recent achievements.

Collaborations

Amazon Research Awards

Overview

Call for proposals

Latest news

Research stories

Recipients

Amazon Nova AI Challenge

Overview

Rules

FAQs

Teams

Research collaborations

Overview

Carnegie Mellon University

Columbia University

Hampton University

Howard University

IIT Bombay

Johns Hopkins University

Max Planck Society

MIT

Tennessee State University

University of California, Los Angeles

University of Illinois Urbana-Champaign

University of Southern California

University of Texas at Austin

Virginia Tech

University of Washington

Amazon Research Awards

Overview

Call for proposals

Latest news

Research stories

Recipients

Amazon Nova AI Challenge

Overview

Rules

FAQs

Teams

Research collaborations

Overview

Carnegie Mellon University

Columbia University

Hampton University

Howard University

IIT Bombay

Johns Hopkins University

Max Planck Society

MIT

Tennessee State University

University of California, Los Angeles

University of Illinois Urbana-Champaign

University of Southern California

University of Texas at Austin

Virginia Tech

University of Washington

Resources

Code and datasets

AGI Labs

Meet the team building useful AI agents.

Amazon Nova

Try Amazon’s frontier foundation models.

Code and datasets

AGI Labs

Meet the team building useful AI agents.

Amazon Nova

Try Amazon’s frontier foundation models.

Careers

Careers

Explore our open roles.

Amazon Scholars

Faculty research opportunities on industry-scale technical challenges.

Postdoctoral Science Program

Early-career research opportunities alongside experienced industry scientists.

Careers

Explore our open roles.

Amazon Scholars

Faculty research opportunities on industry-scale technical challenges.

Postdoctoral Science Program

Early-career research opportunities alongside experienced industry scientists.

Search

Submit Search

Automated reasoning

Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine

Isabelle/HOL's balance of expressiveness, automation, and scalability enabled the world's first formally verified cloud hypervisor.

By Larry Paulson

April 17, 2026

6 min read

Share

Share

Copy link

Email

X

LinkedIn

Facebook

Line

Reddit

QZone

Sina Weibo

WeChat

WhatsApp

分享到微信

x

Overview by Amazon Nova

Isabelle/HOL is a proof assistant used to formally verify the correctness and security of the Nitro Isolation Engine (NIE), the first formally verified cloud hypervisor, which provides resources to AWS clients while ensuring the security of customer data. It balances expressiveness, automation, proof readability, and scalability, making it suitable for formal verification tasks. Isabelle/HOL supports higher-order logic, allowing for the expression of complex mathematical statements and the verification of critical software. It has been used in various projects, including the verification of the seL4 microkernel, WebAssembly semantics, and cryptographic protocols.

Was this answer helpful?

At Amazon’s 2025 re:Invent conference, Amazon Web Services (AWS) announced the Nitro Isolation Engine (NIE), a software module tasked with providing resources to AWS clients while ensuring the security of customer data. AWS also announced the formal verification of the isolation engine’s correctness and security guarantees, using a proof assistant called Isabelle/HOL . As the first formally verified cloud hypervisor, NIE sets a new standard for cloud security.

Isabelle was originally developed at the University of Cambridge and Technische Universität München and includes numerous contributions from institutions and individuals worldwide.

A proof assistant is an automated tool that can help human users develop formal proofs — of mathematical theorems, the validity of hardware or software systems, or anything in-between. Several proof assistants are in common use, and we chose Isabelle/HOL because it struck the right balance among expressiveness, automation, proof readability, and scalability. So what do I mean by that? Logical reasoning by computer

There is no fixed language of mathematics, but we can create languages for expressing mathematical reasoning, just as programming languages express computational tasks. And just as programming languages involve trade-offs between expressiveness and performance, mathematical languages involve trade-offs between expressiveness and ease of automation. Automation is vital because the construction of a formal proof is both time consuming and extremely tedious, analogous to constructing a ship in a bottle.

Building a formal proof is like constructing a ship in a bottle: every piece must be assembled precisely within strict logical constraints. Isabelle/HOL provides the tools to make that painstaking process possible.

The most elementary mathematical language is Boolean logic, the world of the binary operators AND, OR, and NOT. Because this…