Add Tool: Verus

[elanortang]

Tool Name

Verus

Description

Verus is a 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 of the code. Rather than adding run-time checks, Verus instead relies on powerful solvers to prove the code is correct. Verus currently supports a subset of Rust (which we are working to expand), and in some cases, it allows developers to go beyond the standard Rust type system and statically check the correctness of code that, for example, manipulates raw pointers. This includes support for concurrent code.

Tool Information

• Does the tool perform Rust verification?
• Does the tool deal with unsafe Rust code?
• Does the tool run independently in CI?
• Is the tool open source?
• Is the tool under development?
• Will you or your team be able to provide support for the tool?

Comparison to Other Approved Tools

Kani: Kani focuses on memory safety reasoning; its support for reasoning about functional correctness is limited at present. Since Kani is a model checker, it inherits both the advantages and disadvantages of model checking with respect to deductive verification tools like Verus, which focus on functional correctness verification. At the moment, Kani does not support verifying concurrent code.

VeriFast: VeriFast operates via symbolic execution, using separation logic to represent memory. Verus relies on the Rust borrow-checker and linear ghost types (inspired by ideas from separation logic) to automate much of the reasoning, allowing for lightweight SMT queries. Both tools are capable of reasoning about functional correctness properties of unsafe Rust, in single- and multi-threaded programs.

Flux: Flux is a refinement type checker which can prove safety properties. By restricting specifications to decidable fragments of first-order logic, it trades expressivity for strong automation. Verus, by comparison, makes the tradeoff in the other direction. At the moment, Flux does not appear to support verifying concurrent code.

Licenses

MIT license

Steps to Use the Tool

The documentation linked here includes directions for installing Verus, both on the command line and in the experimental VS Code extension.

Artifacts & Audit Mechanisms

If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc.

Please see the full list of papers and projects that have used Verus to verify a number of quite complex systems.

Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests).

The list of papers linked above include discussions on Verus’s design, as well as paper proofs of soundness for some of its core components.

We provide an Architecture Overview to help with understanding Verus’s design and code organization.

The Verus CI currently includes over 3,500 tests, spread across the examples directory and the tests directory.

Versioning

Verus’s GitHub CI automatically publishes a weekly release with binary executables for our supported platforms. The release identifiers are built from the release date and commit hash.

CI

We have an existing CI workflow which builds the verus/verify-rustlib branch (which tracks the Rust standard library version that we are verifying, as opposed to the latest Rust version tracked on the main branch), and uses the resulting Verus binary to verify our copy of the Rust standard library. At present, it verifies all parts of the standard library to which we have added specs/assertions.