Verus Tutorial and Reference
Summary
Verus enables static verification of Rust code to ensure functional correctness for low-level systems. It combines a Rust-based specification/proof language with a formal verification workflow that leverages SMT solving (e.g., Z3) while acknowledging scope limits and the need for manual proof where SMT falls short.