Amazon details using Verus to formally verify Rust code correctness

Amazon Science explains Verus, an open-source automated program verifier for Rust that checks code against formal specifications for all possible inputs.

Developers write specifications and proofs directly in Rust source using Rust-like syntax, and Verus returns feedback in under a second.

Amazon says it has used Verus to prove the correctness of key primitives in the Nitro Isolation Engine and other infrastructure.