Kind 2 Extension for VS Code

September 10, 2026 ยท View on GitHub

This extension provides basic support for the Lustre programming language with Kind 2 Model Checker annotations.

Requirements

Java 11+ run-time.

  • Debian-based Linux: sudo apt install openjdk-17-jdk
  • RHEL-based Linux: sudo yum install java-17-openjdk
  • MacOS: brew install --cask temurin
  • Windows: install a JDK from Adoptium, or run winget install EclipseAdoptium.Temurin.17.JDK.

Windows is supported natively; running the extension through WSL2 is no longer required.

Windows through WSL2 (Advanced)

Running the extension inside WSL2 remains supported, and uses the Linux build. WSL1 is not supported. Follow these steps to run the extension on WSL2 (Windows 10 version 1903+ or Windows 11):

  1. Install WSL
    • Windows 10 version 2004+ and Windows 11: Run wsl --install in PowerShell or Windows Command Prompt and restart your machine.
    • Windows 10 version 1903+: follow the manual steps in this page.
  2. Follow the instructions on this page to finish setting up your WSL2 Linux environment.
  3. Install the Remote - WSL extension for VS Code.
  4. Click on the green rectangle in the bottom-left corner of the VS Code window. A prompt will appear on the top. click on new WSL window. WSL window
  5. Press Ctrl+Shift+` to open a Linux terminal on the new VS Code window. Use the terminal to install the Java run-time.
  6. In the same VS Code window, go to the extension view in the activity bar to the left and lookup the Kind 2 extension. Click Install in WSL: <distro name>. Install extension Refer to this page to learn more about using WSL with VS Code.

Options

The extension supports modular and compositional analysis modes of Kind 2. Those modes are disabled by default. Follow the steps below to enable them (and other Kind 2 configurations):

  1. Go to VS Code settings. GUI settings
  2. Click on Kind 2 under the Extensions section. Kind 2 settings
  3. Enable modular, compositional, and/or other options. GUI Options
  4. If you prefer an editor interface, click on go-to-file icon at the top-right corner of the settings page to switch the JSON view: JSON settings
  5. Type kind2. VS Code will provide an autocompletion menu with available Kind 2 options. Select the options you want to configure and save your changes. JSON options

You can also enable/disable modular and compositional analysis modes from Kind's view. Click on their icons to enable them. Analysis modes icons

Main Features

  • Syntax highlighting for Lustre and Kind 2 constructs.
  • Go-to-definition for top level declarations.
  • Document symbol outline. Outline
  • Syntax and type error reports. Error reports
  • Model checking. Check
  • Simulations. Simulations
  • Counter-examples for falsified properties. Counter-examples
  • Raw output of calling Kind 2 through the terminal. Raw output