Developing provably correct Rust code with Verus
Summary
A Amazon Science blog post introducing Verus, an open-source Rust program verifier that checks code against formal specifications, enabling provable correctness and security guarantees. It explains how developers annotate Rust with preconditions and postconditions to enable fast feedback and how Verus can verify unsafe and concurrent code, including complex locking schemes, to restore machine-checked safety guarantees. It also notes real-world usage at Amazon (Nitro Isolation Engine) and in open-source projects, and discusses automation and potential AI-assisted proof generation.