This page has instructions for installing Dafny by typical users:

System Requirements

The dafny tool is a .NET 6.0 artifact, but it compiles to native executables on supported platforms. That and the Z3 tool are all that is needed to use dafny for verification; additional tools are need for compilation, as described below.

Operating Systems

In addition to running dafny, the host OS must also be able to run the Z3 executable that is bundled with dafny. (The Dafny tools are tested using github runners, which limits the set of platforms that can be tested.)

Compilers

The Dafny compiler performs two tasks:

In addition, the Dafny toolkit supplies runtime libraries, either in source form or compiled for the target programming language.

C#

Java

Javascript

Python

Go

C++

C++ has only rudimentary special purpose support at present.

Using an IDE

The easiest way to get started with Dafny is using the Dafny IDEs, since they continuously run the verifier in the background. Be sure to check out the Dafny tutorial!

For most users, we recommend using Dafny with VS Code, which has an easy installation, as explained next:

Visual Studio Code

  1. Install Visual Studio Code
  2. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below.
  3. In Visual Studio Code, press Ctrl+P (or P on a Mac), and enter ext install dafny-lang.ide-vscode.
  4. If you open a .dfy file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: vs-code-dafny-2 0 1-install

Emacs

The README at https://github.com/boogie-org/boogie-friends has plenty of information on how to set-up Emacs to work with Dafny. In short, it boils down to running [M-x package-install RET boogie-friends RET] and adding the following to your .emacs:

(setq flycheck-dafny-executable "[path to dafny]/dafny/Scripts/dafny")

Do look at the README, though! It’s full of useful tips.

Install the binaries from the github releases

The following instructions tell you how to install Dafny so that you can run it from various operating systems as a command-line tool.

If you wish to compile to target languages, see the instructions in a subsequent section to install the correct dependencies for the desired language.

Windows (Binary)

To install Dafny on your own machine,

Then:

Linux (Binary)

To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following:

Within the unzipped Linux distribution, the dafny executable is dafny/dafny

If you intend to use the Dafny compiler, install the appropriate tools as described here

After the compiler dependencies are installed, you can run a quick test of the installation by running the script $INSTALL/dafny/quicktest.sh

Mac (Binary)

To install a binary installation of Dafny on macOS, do one of the following:

Either

or

If you intend to use the Dafny compiler, install the appropriate tools as described here.

After the compiler dependencies are installed, you can run a quick test of the installation by running the script $INSTALL/dafny/quicktest.sh

NuGet (Binary)

The .NET NuGet repository collects .NET libraries and tools for easy installation. Dafny is available on NuGet, and can be installed as follows:

Compiling Dafny

The instructions here describe the dependencies needed to have the tools to compile to various languages and the procedure to use for simple programs.

Note that a pure Dafny program (say A.dfy) can be compiled and run in one step using dafny run A.dfy and can be run for a particular programming language with the --target option (the default target is C#). Additional instructions are found in the Dafny User Guide.

C# (.Net)

Install .NET 6.0:

To separately compile and run your program for .NET:

Javascript

To set up Dafny to compile to JavaScript (node.js):

To separately compile and run your program for JavaScript:

Go

To set up Dafny to compile to Go:

To separately compile and run your program for Go:

Java

To set up Dafny to compile to Java:

To separately compile and run your program for Java:

Python

To setup Dafny to compile to python3:

To separately compile and run your program for Python: