Developing provably correct Rust code with Verus
Verus is a new framework that integrates formal verification into the Rust programming language, enabling developers to write code with machine‑checked proofs of correctness. By extending Rust’s type system and providing a specification language, Verus lets programmers express invariants and verify them automatically. The project aims to improve safety in systems code while preserving Rust’s performance characteristics.