Skip to content
Dafny is a verification-aware programming language
C# F# Java Go Python JavaScript Other
Branch: master
Clone or download
RustanLeino Merge pull request #376 from lavaleri/patch-1
Add guidelines for newline use
Latest commit 08bf591 Sep 10, 2019
Type Name Latest commit message Commit time
Failed to load latest commit information.
Binaries Spend less time constructing BigInteger's in compiled code Aug 30, 2019
Source Spend less time constructing BigInteger's in compiled code Aug 30, 2019
Util Added "witness" clauses to newtype and subset-type declarations. Reso… May 19, 2017
third_party/Coco Updated the Coco build and .exe to use VS 2017 and a .NET version 4.5 Feb 8, 2018
.gitattributes Preserve line endings for dafny and dafny-server scripts Feb 15, 2018
.gitignore update .gitignore Aug 23, 2019
.travis.yml time lit tests Aug 16, 2019 Move Emacs install instructions to Wiki Jan 9, 2019
LICENSE.txt Change license to MIT following migration to GitHub Jun 18, 2016
NOTICES.txt add copy of Coco under GPL Jul 5, 2017 Move build status to top, add link to new gitter Jul 2, 2019
dafny-banner.png Remove cursor in banner Jun 18, 2016 Include DafnyRuntime.{js,go} into the release. May 7, 2019

Build Status Gitter


Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors. Dafny is currently spread across 3 sites:


You can ask questions about Dafny on Stack Overflow or participate in general discussion on Dafny's Gitter.

Try Dafny

The easiest way to get started with Dafny is to use rise4fun, where you can write and verify Dafny programs without having install anything. On rise4fun, you will also find the online Dafny tutorial. It is also easy to install Dafny on your own machine in VS Code, which gives you a much better user experience than in the web browser.


See installation instructions on the wiki and instructions for installing the Dafny mode for Emacs.

Read more

Here are some ways to get started with Dafny:

The language itself draws pieces of influence from:

  • Euclid (from the mindset of a designing a language whose programs are to be verified),
  • Eiffel (like the built-in contract features),
  • CLU (like its iterators, and inspiration for the out-parameter syntax),
  • Java, C#, and Scala (like the classes and traits, and syntax for functions),
  • ML (like the module system, and its functions and inductive datatypes), and
  • Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).

External contributions

Code of Conduct

This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact with any additional questions or comments.


Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory third_party contains third party material; see NOTICES.txt for more details.

You can’t perform that action at this time.