v3.9.1 documentation snapshot
In addition to a verification engine to check implementation against specifications, the Dafny ecosystem includes several compilers, plugins for common software development IDEs, a LSP-based Language Server, a code formatter, a reference manual, tutorials, power user tips, books, the experiences of professors teaching Dafny, and the accumulating expertise of industrial projects using Dafny. Example Dafny code in a Visual Studio IDE is shown to the right.
Dafny has support for common programming concepts such as
Dafny also offers an extensive toolbox for mathematical proofs about software, including