Rust Deductive Verifier

cargo dv is a thin project-specific wrapper around cargo-verus. Verification and build commands are delegated to cargo-verus verify, cargo-verus focus, and cargo-verus build, while cargo dv keeps a few repository conveniences on top, such as bootstrapping the Verus toolchain, formatting Verus/Rust sources, generating docs, and running pre-commit checks.

Deployment

1. Put this repository as a directory dv in the root of your Rust project.

git clone [this-repo] dv

2. Add/modify the Cargo configuration file .cargo/config.toml in the root of your Rust project:

[alias]
dv = "run --manifest-path dv/Cargo.toml --bin dv --"
pre-commit = "run --manifest-path dv/Cargo.toml --bin pre_commit --"

3. Now, you can use the provided commands with cargo dv:

cargo dv verify --targets <target1> <target2> ...

Bootstrapping Verus

By default, cargo dv bootstrap builds the main branch of asterinas/verus. Use --branch to select another branch and repeat --build-arg to pass additional arguments to cargo-verus when it builds vstd.

The irc11 branch is hosted by verus-lang/verus, rather than the default asterinas/verus remote, and requires its weak-memory vstd modules to be enabled explicitly:

cargo dv bootstrap --upstream-verus --branch irc11 \
  --build-arg=--vstd-weak-memory

For compatibility with the irc11 branch's vargo spelling, DV translates --vstd-weak-memory to the vstd feature arguments --features weak-memory used by the current cargo-verus bootstrap path.

The same arguments are honored by upgrades:

cargo dv bootstrap --upgrade --upstream-verus --branch irc11 \
  --build-arg=--vstd-weak-memory

Optionally, if you want to use the pre-commit hook, you can add the rusty-hook to your project:

cargo install rusty-hook

Then, add the following to your .rusty-hook.toml file:

[hooks]
pre-commit = "cargo pre-commit"

[logging]
verbose = true