Installing Dafny

Follow the instructions below to install the command line version of Dafny. These instructions have been tested for Mac OS, but should also work for Linux and Windows.

Windows

1. Download and unzip the Boogie distribution from the Boogie project webpage. The Boogie distribution also includes Dafny.
2. Download latest version of the Z3 Theorem Prover.
3. Create a Dafny test file and call it test.dfy.
4. While in the Boogie directory, check whether Dafny is working by executing:
   Dafny.exe /compile:0 test.dfy

Linux and Mac OS

1. Download and unzip the Boogie distribution from the Boogie project webpage. The Boogie distribution also includes Dafny.
2. Download latest version of the Z3 Theorem Prover. Build it following the instructions in the README file.
3. Copy the Z3 executable to the Boogie directory and rename it z3.exe.
4. Install Mono. You will need version 2.8 or higher.
5. Create a Dafny test file and call it test.dfy.
6. While in the Boogie directory, check whether Dafny is working by executing:
   mono --runtime=v4.0.30319 Dafny.exe /compile:0 test.dfy