Home

Welcome to the Dafny wiki!

This Wiki contains specific and in-depth information on working with Dafny, specifically for those developing Dafny.

User information about Dafny (tutorials, FAQs, reference materials, etc.) are at dafny.org.

Make sure to check out the Dafny tutorial for a more general introduction to Dafny.

Using Dafny

Setup

• INSTALL
• Disabling underlining of info messages

Best practices

• Style Guide - (maintained in the Dafny repo, not in this wiki)
• Cautionary Tales

How-tos

• FAQ
• Proving termination by decreasing Repr
• Modeling External State Correctly
• Investigating slow verification performance
• Proving properties about integers and bit vectors together

Developing the Dafny tool

• Setting up a development copy of Dafny
• Running Dafny's test suite
• Writing and previewing user-facing web pages
• Issuing a new Dafny release
• JetBrains Rider FAQ
• Building against a custom Boogie
• Contributing FAQ