Developing provably correct Rust code with Verus

Summary

Rust’s type system prevents many memory-safety bugs, but it does not prove that programs compute intended results, avoid leaks, or correctly handle every unsafe and concurrent operation. Verus is an open-source automated program verifier that checks Rust implementations against formal specifications for all possible inputs, using solvers to discharge proof obligations while developers provide guidance such as loop invariants. Specifications and proofs use Rust-like requires and ensures annotations written alongside the code, while ordinary Rust compilers ignore them and Verus typically returns feedback in under a second. The tool can prove properties of unsafe code, lock invariants, and concurrent systems, and Amazon has used it for key Nitro Isolation Engine primitives and other critical infrastructure.

Takeaways

1. 1

   Verus checks specifications against implementations for all possible inputs rather than only the cases covered by traditional tests.

2. 2

   Verus annotations are ignored by ordinary Rust compilers, allowing annotated code to be used by verified and unverified projects, including Cargo-based projects.

3. 3

   Amazon has used Verus to prove key primitives in the Nitro Isolation Engine and other critical infrastructure; open-source uses include certificate validation, persistent-memory logs, microkernels, and Kubernetes controllers.