Kani Visual Studio Code Extension

A Visual Studio Code extension that allows users to run and debug their Kani Rust Verifier harnesses in VS Code.

Usage

Kani Usage

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.

Features

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.

Requirements

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.

Extension Settings

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`

Installation

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.

Troubleshooting

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.

Security

See SECURITY for more information.

License

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.

Code of conduct

This project has adopted the Rust Code Of Conduct. See CODE OF CONDUCT for details.

Kani

Model Checking