# Using Verus via Cargo

For projects with multiple crates, Verus provides a `cargo verus` subcommand
that integrates verification into the normal Rust Cargo workflow.

## Prerequisites

The `cargo-verus` binary must be in your `PATH`. It is included in the official
[Verus release packages](https://github.com/verus-lang/verus/releases) alongside the
`verus` binary.

Check that it is available by running:

```
cargo verus --help
```

## Starting a new project

The fastest way to create a new Verus project is:

```bash
# Binary project
cargo verus new --bin my_project

# Library project
cargo verus new --lib my_library
```

This creates a new directory with a correctly-configured `Cargo.toml`, an initial
`src/main.rs` (or `src/lib.rs`), and a `.gitignore`. The generated project already has
`vstd` as a dependency and the `[package.metadata.verus]` section described below.

## Updating an existing Rust project to support Verus

To enable verification for one or more of the crates in your project, add `vstd` as a
dependency as follows:

```sh
cargo add vstd
```

Then import the Verus prelude in each root module (e.g. `lib.rs` or `main.rs`):

```rust
use vstd::prelude::*;
```

To opt a crate into verification, include the following in its `Cargo.toml`:

```toml
[package.metadata.verus]
verify = true
```

If the crate is not in a workspace, also add the following to suppress warnings
about `cfg(verus_only)`:

```toml
[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
```

See below for more details.

Note that you can still use normal `cargo` commands (e.g., `cargo build`) on
crates and projects that include Verus annotations.

## The Verus prelude

Each verified crate needs to import the Verus prelude as follows:

```rust
use vstd::prelude::*;
```

## Cargo.toml configuration

Crates that should be verified must opt in by adding a `[package.metadata.verus]`
section to their `Cargo.toml`:

```toml
[package.metadata.verus]
verify = true
```

### Suppressing the `verus_only` lint

Verus enables a `verus_only` cfg flag during verification so that `use` statements for
ghost items can be guarded with `#[cfg(verus_only)]`. Since this flag is not declared in
`Cargo.toml`, Rust 1.80+ will emit a warning unless you suppress it:

```toml
[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
```

`cargo verus new` adds this automatically. See [Ghost Erasure](./erasure.md) for a full
explanation of `verus_only` and when to use it.

In a Cargo workspace, you should instead include the following in the root `Cargo.toml`:

```toml
[workspace.lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
```

Then ensure that each member crate's `Cargo.toml` has the following (which e.g. `cargo new` adds
automatically):

```toml
[lints.rust]
workspace = true
```

## Subcommands

### `cargo verus verify`

Runs verification on all crates that have `verify = true`, including dependencies.
Does **not** produce a compiled binary.

```bash
cargo verus verify              # Verify all of the crates
cargo verus verify -p my_crate  # Verify only my_crate and its dependencies
```

Use `verify` for day-to-day proof development. Incremental builds mean that only
changed crates are re-verified.

### `cargo verus focus`

Like `verify`, but skips re-verification of dependencies. Useful when you are only
iterating on root crates and their dependencies have not changed.

Unlike `verify`, `focus` stores its artifacts in a separate target directory
under `target/verus-partial`, so that a full `cargo verus verify` isn't misled
by the cached partial results.

```bash
# Verify all of the root crates, but not their dependencies
cargo verus focus
# Verify my_crate, but not its dependencies
cargo verus focus -p my_crate
```

Dependencies are still *built* (so their types are available), but their proofs are
not re-checked. `cargo verus verify` should be used before committing to ensure the project's
end-to-end proof is sound.

### `cargo verus build`

Verifies all opted-in crates **and** compiles them to native artifacts (libraries or
binaries). Use this when you want to ship a verified binary.

```bash
cargo verus build
cargo verus build --release
```

Note that Verus-annotated code can also be built with a normal `cargo build` command, if you prefer.


## Passing arguments

Arguments are split around `--`:

- **Before `--`**: forwarded to `cargo`
- **After `--`**: forwarded to every `verus` invocation

```bash
cargo verus verify -p my_crate --release -- --rlimit 60 --expand-errors
#                  ^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
#                  Cargo arguments            Verus arguments
```

Verus-relevant Cargo options must come before generic Cargo flags such as `--release`.
The Verus-relevant options are:
- `-p`/`--package`, `--workspace`, `--all`, `--exclude`
- `--features`, `--all-features`, `--no-default-features`
- `--manifest-path`, `--target-dir`
- `--frozen`, `--locked`, `--offline`
- `--config`, `-Z`

The `-Z` option must be written with a space, e.g. `-Z unstable-options`; the
compact form is not supported.

Common Verus arguments that can be passed this way include `--rlimit`,
`--expand-errors`, and `--log-all`.  You should typically avoid passing
crate-specific arguments this way.  For example, passing `--verify-module`
or `--verify-function` is unlikely to work, unless you have the same module/function
in every verified crate in your project and its dependencies.  To pass these
project-specific flags, see below for how to control which crates receive
which Verus arguments.

### Controlling which crates receive Verus arguments

By default, the Verus arguments after `--` are forwarded to **all** verified crates.
Use `--fwd-verus-args-to <target>` to narrow or widen the target.

| Value    | Effect                                                         |
|----------|----------------------------------------------------------------|
| `all`    | Forward to all verified crates, including dependencies (default for `verify`, `build`) |
| `roots`  | Forward only to the root (selected) crates (default for `focus`) |
| `deps`   | Forward only to dependency crates, not to root crates          |

```bash
# Only pass --rlimit to the root crate, not to its verified dependencies
cargo verus verify --fwd-verus-args-to roots -- --rlimit 60
```

Recall that you can also use the standard `cargo -p <crate_name>` to restrict
operation to a single crate (and potentially its dependencies).

## Multi-crate workspaces

In a workspace, each crate that should be verified must independently opt in by adding
`verify = true` to its `Cargo.toml` file. Crates without that setting are
compiled normally and are not passed through the Verus prover.

```bash
# Verify the entire workspace
cargo verus verify --workspace

# Verify a single crate and its verified dependencies
cargo verus verify -p my_crate
```

## Incremental verification

cargo-verus stores `.vir` files next to the compiled `.rlib` artifacts in the `target`
directory. Cargo's fingerprinting system detects when these files change and
automatically re-verifies downstream crates. Running `cargo clean` removes all
verification artifacts.