verus-analyzer

This extension provides support for the Verus programming language. It is derived from rust-analyzer

This extension is experimental and subject to change; some features are likely broken. At present, it works best on small, self-contained Verus projects. Anything more complex will likely fail.

WARNING: verus-analyzer expects you to "Open Folder..." on a directory containing a standard Rust project layout and metadata (Cargo.toml) file. verus-analyzer scans the project root (src/lib.rs or src/main.rs) and all files that are reachable from the root. If the file you are working on is not reachable from the project root, most of the IDE features like "Go to Definition" will not work.

Verus-specific Features

• Support for Verus syntax
• Each time you save a file in your project, Verus runs and reports proof failures and warnings
• Proof actions are an experimental feature to assist developers when debugging proof failures. They show up as light bulb icons in the IDE when you hover over a failed proof.

Features Extended from Rust Analyzer

• 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. Ensure you have rustup installed.
2. Install the verus-analyzer extension.

Configuration

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

See the Rust analyzer manual for more information on VSCode-specific configurations.

Communication

For usage and troubleshooting requests, please use the Verus Zulip.

Documentation

See rust-analyzer.github.io for more information about the original Rust analyzer.