Dafny is a programming language that provides verification-ready support during development. It has an integrated verifier which constantly flags errors and shows counterexamples, ensuring that the code meets the written specifications. Dafny supports common programming concepts such as classes, inheritance, datatypes, lambdas, and more. The language offers an extensive toolbox for mathematical proofs such as quantifiers, termination conditions, loop invariants, and read/write specifications. Dafny can compile code to C#, Go, Python, Java, or JavaScript, reducing the risk of costly bugs during the development process. This github site contains sources, binary downloads for multiple platforms, the issue tracker, and wiki with frequently asked questions. You can learn more about Dafny by visiting their website or reference manual that is available online and in PDF format. Join the Dafny community on Stack Overflow and Gitter or try Dafny out today.
