Verus: A Static Analyzer for Verifying Rust Code Correctness

Verus is a static analysis tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions. Instead of runtime checks, Verus relies on powerful solvers to prove code correctness. Currently supporting a subset of Rust (with ongoing expansion), Verus allows developers to go beyond the standard Rust type system in some cases, statically checking the correctness of code manipulating raw pointers, for example. Verus is under active development; features may be broken or missing, and documentation is incomplete.