This page has instructions for installing Dafny for developers.

User installation instructions are in the project's repository. Those instructions are a necessary precursor to these.

If you want access to the very latest Dafny developments or you want to extend Dafny yourself, install the source code, as explained here.

Note that the Dafny integration tests are mainly written using the syntax defined by the LLVM Integrated Tester (LIT) tool, but are actually run using a custom xUnit adaptor in the IntegrationTests package. The configuration files for LIT are still temporarily present in the Test directory and therefore LIT is still likely to work, but its use is deprecated and will not be supported in the future. See here for more details.

First, install the following external dependencies:

• Visual Studio 2017 or newer, or the free Visual Studio Community Edition
• Visual Studio SDK extension
• Code contract extension
• NUnit test adapter
• Python 3 which should come bundled with pip, or manually install pip.

To install pre-commit checks to verify the style of C# files, run:

pip install pre-commit
pre-commit install

If you had any pre-commit scripts before, follow these steps to keep them.

Second, clone the Dafny source code.

git clone https://github.com/dafny-lang/dafny --recurse-submodules

Third, build the Dafny project, either on the command line: dotnet build dafny\Source\Dafny.sln or open Visual Studio, and open dafny/Source/Dafny.sln, and click on Build > Build solution while the project Dafny Runtime is still the startup project (in bold)

To run Dafny on a particular file, or to run the tests, you'll have to install a prover such as CVC4 or z3. For z3, do the following:

1. Go to the release of version 4.12.1, download the zip according to your system
2. Unzip the content of the Z3 folder into dafny\Binaries\z3 so that dafny\Binaries\z3\bin\z3.exe exists.
3. (optional, depending on configuration) Make sure the dafny\Binaries\z3\bin folder is accessible from the command line by updating the PATH environment variable.

To run Dafny on a particular file:

• Right-click the project DafnyDriver, and set as startup project
• Click Debug > DafnyDriver Debug properties...
• In the text area "Application arguments", write the path to the file you would like to run Dafny on, e.g. "..\..\Test.dfy" with the double quotes, if the file Test.dfy is next to the dafny folder, and save
• Now, press F5 to compile Dafny and run it on the specified file.

To run the integration tests, go to dafny/Source/IntegrationTests and run dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them.

0. Dependencies:

   • Install .NET 6.0 as described above
   • Install python3: e.g., sudo apt install python3 python3-pip
   • If you intend to compile to Java, install Java and gradle

1. Download and build Dafny:

   git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
   cd dafny
   make exe
   

To install pre-commit checks to verify the style of the source code, perform

   pip3 install pre-commit
   pre-commit install

If you had any pre-commit scripts before, follow these steps to keep them.

2. Install Z3 version 4.12.1 (not the most recent version of Z3)

   make z3-ubuntu
   

   OR

   cd dafny/Binaries
   wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
   unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
   mv z3-4.12.1 z3
   

3. Install the compiler dependences as described here.

4. Run Dafny using the dafny shell script in the Scripts directory: dafny/Scripts/dafny You can run a quick test of the installation by executing dafny/Scripts/quicktest.sh

5. To execute the integration tests: cd dafny/Source/IntegrationTests; dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them. The tests take a while, depending on your machine, but emit progress output.

0. Dependencies:

   • Install .NET (6.0): brew install dotnet-sdk
   • [python3 and pip3 are needed but they are likely already part of the Mac installation]
   • (Optional) Install java (possibly use brew install openjdk@8)
   • (Optional) Install gradle (possibly use brew install gradle)

1. Download and build Dafny:

   git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
   cd dafny
   make exe
   

To install pre-commit checks to verify the style of the source code, perform

   brew install pre-commit
   pre-commit install

If you had any pre-commit scripts before, follow these steps to keep them.

3. Download and unpack Z3 (Dafny looks for z3 in Binaries/z3/bin/) version 4.12.1 (note, this is not the latest version of Z3). You can use

   brew install wget
   make z3-mac
   

or

   cd dafny/Binaries
   wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
   unzip z3-4.12.1-x64-macos-11-bin.zip
   mv z3-4.12.1 z3

4. Install the compiler dependences as described here.

5. Install backend-dependencies as needed.

6. To compile to JavaScript, make sure you have Node.js installed and run

   npm install bignumber.js
   

7. Run Dafny using the dafny shell script in the Scripts directory: dafny/Scripts/dafny You can run a quick test of the installation by executing dafny/Scripts/quicktest.sh

8. To execute the integration tests: cd dafny/Source/IntegrationTests; dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them. The tests take a while, depending on your machine, but emit progress output.

If you install pre-commit, it will rename any existing pre-commit hook (./git/hooks/pre-commit) to a file namepre-commit.legacy, and put a python script named pre-commit instead. To keep any previous pre-commit hooks along with the new hook:

• Rename pre-commit to pre-commit-python
• Make pre-commit-python executable
• Rename pre-commit.legacy to pre-commit
• Add the line ./.git/hooks/pre-commit-python to the file pre-commit.

The reference manual is only buildable on Linux or Mac and requires some tools to be installed

On Mac:

• brew install --cask basictex
• brew install pandoc
• eval "$(/usr/libexec/path_helper)"
• sudo tlmgr update --self
• sudo tlmgr install framed tcolorbox environ trimspaces

Then, in the top-level directory of the source distribution: make refman

Dafny is tightly integrated with Boogie. Sometimes we want to make Boogie changes and test those changes against Dafny. To do that, you must replace the Boogie NuGet package reference with project references to a locally checked out Boogie. We've added the git patch customBoogie.patch to the Dafny repository to make this easier. The patch requires that a Boogie repository with directory boogie is a sibling of the Dafny repository.

Steps to use:

• git clone git@github.com:dafny-lang/dafny.git --recurse-submodules
• cd dafny
• git clone -b v<Boogie version> git@github.com:boogie-org/boogie.git
  • The required version of Boogie shows up as the version attached to the Boogie.ExecutionEngine dependency in this file: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/DafnyCore.csproj#L34
• git apply customBoogie.patch
• dotnet build Source/Dafny.sln

You can then use git checkout Source/Dafny.sln Source/Directory.Build.props to return to the version of Boogie that Dafny regularly builds with.

Alternatively, you can build a local checkout of Boogie separately and copy the binaries into the Dafny Binaries directory with the Scripts/use-local-boogie.sh script:

• ln -s <your checkout of Boogie> Source/boogie (or clone it there directly)
• dotnet build Source/Dafny.sln
• Scripts/use-local-boogie.sh

This can be useful for certain debugging scenarios in which you want to temporarily use a custom Boogie version, because cleaning and rebuilding automatically reverts to the standard version, and because Boogie can then easily be built with different compilation flags than Dafny.