verus-analyzer

This extension provides IDE support for the Verus verification language. It is derived from rust-analyzer and remains compatible with ordinary Rust syntax.

Verus Features

• Verus syntax parsing and highlighting
• Verification on save with editor diagnostics
• Automatic installation of the latest Verus release
• Experimental proof actions for debugging failed proofs

Inherited Rust Features

• code completion with imports insertion
• go to definition, implementation, type definition
• find all references, workspace symbol search, symbol renaming
• types and documentation on hover
• inlay hints for types and parameter names
• semantic syntax highlighting
• a lot of assists (code actions)
• apply suggestions from errors
• ... and many more, check out the manual to see them all

Quick start

1. Install rustup and a Rust toolchain compatible with your Verus project.
2. Install the verus-analyzer extension.
3. Open a Cargo project containing Verus code.

The extension downloads Verus automatically on supported platforms. Configure verus-analyzer.verus.binary to use an existing Verus build, or disable verification with verus-analyzer.verus.enable.

Configuration

This extension provides configurations through VSCode's configuration settings. All configurations are under verus-analyzer.*.

See the verus-analyzer repository for Verus settings and the rust-analyzer manual for inherited VS Code settings.

Communication

For usage and troubleshooting, use the Verus Zulip.