EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
330,000 lines of machine-checked proofs in Isabelle/HOL verify that the Nitro Isolation Engine correctly enforces confidentiality, integrity, and memory safety between EC2 virtual machines on Graviton5.
Amazon Science · https://www.amazon.science/author/dominic-mulligan