Amazon Science on Mythryl: “The first formally verified hypervisor is now deployed in a…”

The first formally verified hypervisor is now deployed in a commercial cloud. The Nitro Isolation Engine is generally available today on Graviton5, backed by 330,000 lines of machine-checked mathematics:

amazon.scienceEC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolationSplitting the “separation kernel” off from the rest of the Nitro security system and using only a subset of the Rust programming language to code it enabled its formal verification.

10/6/26, 6:23 pm0 reposts0 likes

Post