Developing provably correct Rust code with Verus

Amazon uses the open-source Verus tool to mathematically prove the correctness of critical Rust code, including key components of the Nitro Isolation Engine.