# Tips and Expectations for Contributing to Verus

Thanks for contributing to Verus! Verus is an Open Source project and welcomes
contributions. Please report issues or start discussions here on GitHub.

We use GitHub discussions for feature requests and more open-ended conversations about
upcoming features, and we reserve GitHub issues for actionable issues (bugs) with
existing features. Don't worry though: if we think an issue should be a discussion (or
vice versa) we can always move it later.

## Reporting an issue

Verus has a convenient feature to record an execution run, along with necessary files (including the source to your crate) to help debug and fix issues. When reporting an issue, we would appreciate if you run Verus with this feature.

To record an execution run, simply add `--record` to the verus command that triggers the issue. This will produce a `.zip` file (named with the current date/time) that you can attach when opening a GitHub issue.

If you want to aid us in debugging (or are unable to share your full recording, which includes the full crate for us to be able to reproduce your issue), you can attempt to minimize the issue before recording it. For automatic minimization of a crate or file (producing a smaller file that triggers the same error), see [source/tools/minimizers/README.md](./source/tools/minimizers/README.md) for more details.

## Expectations when making a contribution

Verus is a verification tool, but it is not itself verified, so we use traditional software methods like testing and human review to ensure quality. Therefore, we have high standards for code changes.

As a new contributor, you should expect at least one review from a core contributor (e.g., @tjhance, @Chris-Hawblitzel, or @parno). The first reviewer will also determine if additional reviews are necessary.

In the PR description, please describe:

- What issue you're solving (please include a link to an existing GitHub issue if it exists)
- Changed behavior, if any
- A description of your code changes

For _opinionated changes_, such as those that add a feature or dramatically modify code architecture, we would highly recommend checking with the Verus team first (by opening a [GitHub Discussion](https://github.com/verus-lang/verus/discussions)) to save time and to ensure the direction is a desirable one.

### Policy for AI-generated and AI-assisted code

AI use is permitted, but all code produced via agentic AI must be disclosed in the PR. Regardless of how the code is produced, we expect the human contributor to take responsibility for the quality of the code. As a consequence of this position, **do not** list any tool (AI or otherwise) as a co-author. Instead, you can use `Assisted-by: <tool>:<model>`.

AI-assisted coding, or "vibecoding," carries a number of risks. These risks include both damage to overall code quality and the risk of overburdening the reviewers, as code can be generated faster than it can be reviewed. We will close a PR if we feel those risks cannot be satisfactorily managed, or if our time is abused.

We expect professionalism and common sense from contributors; you, the human author, are responsible for the pull request. Be prepared to receive feedback or to answer questions about the PR. **The PR description, along with subsequent PR discussion comments, must be human-written in all cases.**

## Building Verus from Source

**See [BUILD.md](BUILD.md) for how to build Verus from source.**

## Editing the source code of Verus

Before committing any changes to the source code,
make sure that it conforms to the `rustfmt` and `verusfmt` tool's guidelines.
We are using the default `rustfmt` settings from the Rust repository
(which also apply to the `verusfmt` formatting for the `vstd`).

If you are working on `vstd`, you will need to set up `verusfmt`, which ensures
`verus! { ... }` code has consistent formatting. You can ensures you are on the latest release of verusfmt
by following the [installation instructions](https://github.com/verus-lang/verusfmt/blob/main/README.md#installing-and-using-verusfmt).

To check the Verus and vendored dependencies' source code, and `vstd`'s formatting,
type the following from the `source` directory:

```sh
cargo make fmt --check
```

If the source code follows the guidelines, `cargo make fmt --check` will produce no output.
Otherwise, it will report suggestions on how to reformat the source code, and will output a
non-zero status code.

To automatically apply these suggestions to the source code, type:

```sh
cargo make fmt
```

If you want to use VS Code with `rust-analyzer` to edit the source code of Verus,
open Visual Studio Code on the root of the project (not `source`) and copy
`.vscode/settings.json.template` to `.vscode/settings.json` and then
edit that file to customize it for your local setup. For instance,
delete `[.exe]` if you're not using Windows and change it to `.exe` if
you are.

### Running `verusfmt` manually

Make sure you are in `source` or one of its subdirectories
(verusfmt picks up the configuration in `source/rustfmt.toml`), and run:

```sh
# To format a specific file
verusfmt <file>.rs

# To format all of vstd at once (on *nix)
find vstd -name \*.rs -print0 | xargs -0 -n1 verusfmt

# To format all of vstd at once (on Windows Powershell)
Get-ChildItem -Path .\vstd -Filter *.rs -Recurse | ForEach-Object { verusfmt $_.FullName }
```

## User-facing documentation

The CI publishes some user facing documentation, including the ["verusdoc" (modified rustdoc) of `vstd`](https://verus-lang.github.io/verus/verusdoc/vstd/), as well as a [tutorial guide](https://verus-lang.github.io/verus/guide/).

To manually build the `vstd` documentation, run,

```sh
cd source
./tools/docs.sh
```

The output of the command will tell you where the HTML is generated.

Meanwhile, the tutorial guide can be found in `source/docs/guide/`. From that directory, run `mdbook serve` to run a local webserver to render the guide as HTML.

## Internal code documentation

Commenting the code is strongly encouraged. Use `///` to create comments
that [`rustdoc`](https://doc.rust-lang.org/rustdoc/what-is-rustdoc.html) can
automatically extract into HTML documentation.

You can compile the current documentation by running (in the `source` directory)

```sh
RUSTC_BOOTSTRAP=1 cargo doc
```

which will produce documentation files, e.g., `./target/doc/rust_verify/index.html`

## Running tests for the Rust-to-VIR translation, and inspecting the resulting vir/air/smt

After building Verus and `vstd`, you can run `rust_verify_test` as follows:

```sh
cargo test -p rust_verify_test
```

You can run a single test file and a specific test within with the following:

```sh
cargo test -p rust_verify_test --test <test file> <test name>
```

`cargo nextest run` is also supported. To install `nextest`, see [https://nexte.st/book/installation.html](https://nexte.st/book/installation.html).

See `cargo help` for more info on the test flags.

If you need to pass additional command-line arguments to the verifier in tests, for example to print the
erased rust ast, you can use the `VERUS_EXTRA_ARGS` environment variable, like this:

```sh
VERUS_EXTRA_ARGS="--print-erased-spec" cargo test -p rust_verify_test --test refs -- --nocapture test_ref_0
```

It can be useful to inspect the intermediate representations used by Verus (VIR, AIR, SMTLIB);
you can log the VIR, AIR, and SMTLIB for a test with:

```sh
VERUS_EXTRA_ARGS="--log-all" cargo test -p rust_verify_test --test refs -- --nocapture --exact test_ref_0
```

This will output the log files in `rust_verify_test/.verus-log`. Only run one test at
a time when using this flag, so that the logs are not overwritten by other tests.

You may find that every time you run a test it takes minutes to start because
all of Verus is getting rebuilt. This shouldn't happen. If it does, it's
likely because you're running an IDE that uses `rust-analyzer` in the
background, and it's invalidating the build cache. To prevent this, you need
to configure your IDE for Verus development. See above for how to do
this for VS Code.

### Measuring test coverage

See: **[Nightly Coverage Report](https://verus-lang.github.io/verus/dev/coverage/)**

`tools/coverage.sh` reports how much of the verifier the `rust_verify_test`
suite exercises. Run it from `source/`:

```
./tools/coverage.sh                    # whole suite
./tools/coverage.sh --test bitvector   # narrow to one suite
```

This writes the reports to `coverage/`. Open `coverage/index.html` in a browser
for the annotated source view, or read the text summary with `cat
coverage/coverage.txt`. An `lcov` file (`coverage/coverage.lcov`) is also
written for external tools.

The tests run the verifier as a spawned subprocess, so the script instruments
that `rust_verify` binary (not the test binary), and gathers coverage from those
processes.

### Line count tests

Some of the tests for the `line_count` tool (located in `source/tools/line_count`) use [`cargo-insta`](https://docs.jj-vcs.dev/latest/templates/#commit-keywords). This is a testing mechanism that makes it nice to test against snapshots of the output of a tool.

`cargo-insta` is not needed to run the tests, but it provides a nice interface for accepting/rejecting new snapshots on test failure.
This can be useful, for instance, if one of your changes changes the way `line_count` computes the line attribution split, making the snapshots change.
If you find you need `cargo-insta`, it can be installed with `cargo install cargo-insta`.

## Contributing to the standard library (`vstd`)

### What to contribute

Verus aims to curate `vstd` along similar lines to how Rust curates `std`.
Ideally, `vstd` should contain a set of minimal shared abstractions (and proofs
about them) to enable the larger Verus community to develop their own
abstractions and proof techniques. A particularly important use case for
`vstd` is supporting the abstractions needed to provide specs for Rust's `std`,
so that people developing with Verus can use standard Rust constructs without
relying on external dependencies.

If your contribution doesn't fall into this minimal subset, it may
be better off as an independent package published on [crates.io](https://crates.io),
which the community can then integrate via `cargo verus`. See the
[Best Practices](best-practices-for-publishing-verusverified-code-on-cratesio) below.

### Guidelines for developing `vstd` contributions

When contributing _trusted specifications_ for the Rust standard library to `vstd`,
the absolute most important consideration is soundness. Since `assume_specification`
and external trait specifications are unchecked, they can easily
[subvert Verus's guarantees](https://verus-lang.github.io/verus/guide/external_trait_specifications.html?highlight=assume_spec#soundness-warning).
To help mitigate this risk, please follow these guidelines:

1. Specifications should be written in a concise, easy-to-read style, using the
   simplest, clearest constructs possible. A necessary, but not sufficient
   step, is typically to abstract complex implementation types into
   mathematical types; e.g., we abstract both `HashSet` and `BtreeSet` as a
   mathematical `Set`; `Vec` as a mathmematical `Seq`, etc.
2. Please consult the corresponding Rust documentation for the function. Then
   write your formal specification so as to make it easy to compare it with the
   informal documentation.
3. The assumed precondition should be strong enough to rule out unsafety and panics.
4. We strongly recommend consulting the function's implementation to look
   for corner cases that are not mentioned in the documentation (e.g., some
   functions may clone or copy their arguments, which may not be apparent from
   the function signature) or for places where the code and the documentation disagree.
5. Despite the point above, it's important that implementation details **not "leak"**
   into the specification. See above regarding keeping specifications simple and abstract.

Stylistically, inside `vstd`:

- We add a `lemma_` prefix to the name of a lemma (i.e., a `proof fn`) to make its purpose explicit.
- We try to make lemmas associated functions when possible, e.g., `my_map.lemma_remove_keys_len(keys)`, not `lemma_remove_keys_len(my_map, keys)`.
- Run `cargo make fmt-vstd` inside `source/` to format `vstd` using `verusfmt`.

### Tips for testing and verifying your contribution

If you're contributing to the standard library, you should also test the
standalone build of that library by running the following from the repository
root:

```
cargo build --manifest-path source/vstd/Cargo.toml
```

Don't run `cargo build` from inside `source/vstd`: Cargo would then pick up
`source/.cargo/config.toml`, which sets `--cfg verus_keep_ghost` and makes
`rustc` try to compile the ghost code, which only Verus can do.

A common error you'll find at this stage is that imports of specific
identifiers with `use` (as opposed to blanket imports using `*`) don't work
when building the standalone exec-only version of `vstd`. To rectify this error,
make sure every such import is prefixed by `#[cfg(verus_keep_ghost)]`, as
in the following example:

```rust
#[cfg(verus_keep_ghost)]
use crate::arithmetic::internals::general_internals::is_le;
```

You may sometimes want to verify `vstd` outside of the usual build process. To do so,
build Verus first following the instructions above (with `cargo build --release`) and then
run, from inside `source/`:

```sh
cargo verus verify --manifest-path vstd/Cargo.toml --features std,alloc
```

## Best practices for publishing Verus-verified code on crates.io

[Publishing](https://doc.rust-lang.org/cargo/reference/publishing.html)
your Verus-verified crate on [crates.io](https://crates.io) is a great
way to enable more people to build on your hard work. If you do so, we encourage
you to follow these best practices.

1. If your crate is primarily for specification and proof purposes (i.e., a normal Rust developer
   is unlikely to benefit from it), then please make this clear in your preamble (i.e., in the README.md
   file that appears on the crates.io landing page. For example, you might say:
   "This crate contains formal specifications and proofs about Widgets,
   primarily for use with [Verus](https://github.com/verus-lang/verus), a tool
   for verifying the correctness of Rust code."
2. If your crate contains verified executable Rust code that could be used by both unverified
   and verified projects, you might instead say something like: "This crate
   implements Widgets with the following fun features: [Feature list]. The
   code has been formally verified using [Verus](https://github.com/verus-lang/verus),
   which means [list of properties you proved, with suitable caveats for what
   properties have not been proven]." It's important to convey the limitations
   of your proof (e.g., what you may have assumed about other libraries), so that
   consumers of your crate are not disappointed when something breaks. Err on the
   side of under-promising and over-delivering.
3. If your crate contains verified executable Rust code that uses any of
   Verus's unsafe primitives ([raw
   pointers](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html),
   [PPtr](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PPtr.html),
   or
   [PCell](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PCell.html))
   or uses explicit `unsafe` blocks, then we encourage you to run the [safe API
   checker](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html),
   which can detect places where your external interface relies on
   Verus-checked preconditions to ensure safety. It's important to remember
   that unverified consumers are not subject to these checks, so providing such
   an interface may lead to undefined behavior. The
   [guide](https://verus-lang.github.io/verus/guide/calling-verified-from-unverified.html)
   offers some tips on how to improve such an interface.
4. We encourage you to apply [verusdoc](https://verus-lang.github.io/verus/guide/verusdoc.html)
   to your crate. Like `rustdoc`, `verusdoc` will automatically generate nice
   HTML documentation, and it will also include Verus-related specifications.
   Ideally, you should host this documentation online and provide a link to it
   in the preamble of your package on crates.io. In addition, adding a CI job
   to your repository to automatically update your documentation site will
   help keep it in sync as your package evolves.

## Other tips

If you modify the syntax parsing inside of the `dependencies/syn/src` directory,
be sure to regenerate the auto-generated files in the `dependencies/syn/src/gen` directory.
See `dependencies/syn/README.md` for details.

### Cheat Sheet: Vargo to Cargo

The following section assumes that `cargo-make` has been installed via `cargo install cargo-make`.

**IMPORTANT**: The `cargo-make` tasks that need to run `cargo-verus`, `verus`, or `rust_verify`,
install them automatically _only if they are missing_. You **must** re-run `cargo make install` for
any changes to those tools to take effect.

| Vargo                                  | Cargo                                     |
| -------------------------------------- | ----------------------------------------- |
| `source ../tools/activate`             | `cargo make install`                      |
| `vargo build`                          | `cargo make build`                        |
| `vargo build --exclude vstd`           | `cargo make build-exclude-vstd`           |
| `vargo build -p vstd`                  | `cargo make build-vstd`                   |
| `vargo fmt` [`--check`]                | `cargo make fmt` [`--check`]              |
| `vargo fmt --exclude vstd` [`--check`] | `cargo make fmt-exclude-vstd` [`--check`] |
| `vargo fmt -p vstd` [`--check`]        | `cargo make fmt-vstd` [`--check`]         |

For more detail on the exact commands each `cargo-make` task runs, refer to their definitions in
`source/Makefile.toml`.