This Visual Studio Code extension provides interactive IDE features for verifying Rusti programs with the Prusti verifier.
To verify a Rust program, open the command palette (View -> Command Palette, or Shift+Ctrl+P on Ubuntu) and run the command
To automatically run Prusti when a Rust file is opened or saved, enable the corresponding flag in the settings (Preferences -> Settings -> type "Prusti" -> enable "Verify On Open" and "Verify On Save").
To update Prusti run the command
Inline Code Diagnostics
This extension automatically provides inline diagnostics for Rust by running Prusti and parsing its output.
This extension provides the following commands:
Basic code-completion snippets are provided for Prusti annotations.
In order to use this extension, please install the following components: