This extension supports Dafny version 3 and beyond. If you require Dafny 2 support, consider using the legacy extension.

• Compile and Run .dfy files.
• Verification as one types.
• Syntax highlighting thanks to sublime-dafny. See file LICENSE_sublime-dafny.rst for license.
• Display the verification trace for failing assertions.
• IntelliSense to suggest symbols.
• Go to definition to quickly navigate.
• Hover Information for symbols.

You can find examples below.

The plugin requires at least .NET Core 5.0 (the ASP.NET Core 5.0 or 6.0 runtimes to be more specific) to run the Dafny Language Server. Please download a distribution from Microsoft. When you first open a Dafny file, the extension will prompt you to install .NET Core manually. The language server gets installed automatically.

Here are a few impressions of the features.

On the first start, the plugin will install the Dafny language server automatically.

Whenever a syntax, semantic, or verification error is present, the plugin will inform the user.

Press F5 to compile and run the program.

Press F7 to show the verification trace.

Press F8 to hide the verification trace.

Additionally the context menu helps you show/hide the verification trace, as well as copy it to the clipboard with the assume keyword to insert it into the code if needed.

Hover a symbol to get information about that symbol.

Type a dot to get a list of possible members of the accessed symbol.

If VSCode appears unresponsive, you may lower the verification frequency or disable it entirely.

Under certain circumstances, the extension appears to be stuck at Verifying.... Until now, this has only been observed for Mac OSX and occurs due to a stack overflow in the language server. To overcome this issue, set the environment variable COMPlus_DefaultStackSize to a sufficiently large value before starting VSCode. For example:

# Increase the stack size
export COMPlus_DefaultStackSize=100000
# Launch VSCode
code

Dafny for Visual Studio Code is an MIT licensed open-source project that lives from code contributions.

We welcome your help! For a description of how you can contribute, as well as a list of issues you can work on, please visit the Dafny-VSCode GitHub repository.

To build Dafny VSCode locally, first clone this repository.

git clone https://github.com/dafny-lang/ide-vscode.git

Change into the root directory of the previously cloned repository and install the node modules.

npm install

To build and debug using Visual Studio Code, install the TypeScript + Webpack Problem Matchers extension. After the installation, open the root folder within VSCode and hit F5 to debug the Dafny extension.

To debug the extension from source, with a custom version of Dafny, you can use the launch configuration "Run with $DAFNY_DEV_SERVER", which looks at the environment variable DAFNY_DEV_SERVER to determine which Dafny CLI to use to run the language server. For example, if you have a local checkout of Dafny at location /my/path/to/dafny, you can set DAFNY_DEV_SERVER to /my/path/to/dafny/Binaries/Dafny.dll.

To create a VSIX package of the previously built sources, create the package through the CLI:

npx vsce package

We use ESLint with the TypeScript plugin to ensure code consistency across the whole source. Install the ESLint extension in VSCode to have live feedback. Alternatively, you can check your code from the command line by running npm run lint.