CS 477 - Formal Software Development Methods (Fall 2016)

Information on Dafny

DAFNY is a programming language that allows specifications and comes equipped with a program verifier. See the Dafny page for various resources, including quick references, tutorials, videos, etc.

You can use Dafny in different ways: you can try it online at Rise4Fun/Dafny or you can install it on your machine. We encourage you to install it on your machine for this course.

Windows machines

Go to

You can use Dafny in different ways: you can try it online at Rise4Fun/Dafny or you can install it on your machine. We encourage you to install it on your machine for this course.

Windows machines

Go to this page on the Dafny Github site and follow instructions to install the binary directly (Z3 will automtically get installe).

Executing Dafny
./Dafny.exe /compile:0 filename.dfy

Linux or Mac machines

Follow the instructions below to install the command line version of Dafny. These instructions have been tested for macOS 10.12 (should also work for 10.11), and Linux (Ubuntu 14.04).

First install mono:
Installation Guides for macOS, Linux and Windows are provided in the following website: http://www.mono-project.com/docs/getting-started/install/.

Then install Dafny:
Download and unzip the latest release of Dafny corresponding to your OS from the Dafny project website: https://github.com/Microsoft/dafny/releases/tag/v1.9.8

Executing Dafny
mono Dafny.exe /compile:0 filename.dfy