A Visual Studio Code extension that allows users to run and debug their Kani Rust Verifier harnesses in VS Code.
- Open a Rust package in Visual Studio Code.
- Navigate to the testing panel and expand on the Kani harness tree view where the harnesses are shown.
- Click on the play button beside the harness or the filename or the crate to run Kani on the respective test case.
Check user guide for more detailed information.
- Automatically indexes and shows Kani harnesses in a tree view.
- One-click button for verifying Kani harnesses.
- Generate counterexamples as Rust unit tests.
- Debug counterexamples using a standard debugger.
- View coverage information inline using VS Code source highlighting.
- Visual Studio Code 1.50 or newer
- Kani 0.34 or newer
NOTE: The extension only works on Cargo packages. For standalone Rust files, Kani is only available on the command line.
| Setting | Description | Default |
|---|---|---|
kani.enable-codelens |
Enable Codelens actions for Run Test (Kani) & Debug Test (Kani). |
true |
kani.show-output-window |
Toggle to show the output terminal window containing the full output from Kani. | false |
kani.highlight-coverage |
Toggle to enable the codelens button for Generage Coverage by default. |
false |
The Kani VSCode Extension is available as a VSCode plugin. You can install the Kani VSCode Extension from the Visual Studio Marketplace.
If you want to build and package from source directly, see dev-documentation for more information.
Check troubleshooting for frequently asked questions and potential fixes.
If you have a question that is not answered there, please file an issue with your question.
See SECURITY for more information.
This code is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See LICENSE-APACHE and LICENSE-MIT for details.
This project has adopted the Rust Code Of Conduct. See CODE OF CONDUCT for details.