The links below connect to annotated examples of Dafny source code, demonstrating various coding techniques or proof capabilities. Each of these verify successfully.

The files for these examples can be found in the examples folder of Dafny’s github project.

• Simple Maximum method
• Tutorial on parser combinators
• A simple compiler
• An example of significant use of induction on a mini-compiler