These are the assignments for COMP SCI 839 (Protocol Verification), taught at UW-Madison in Fall 2023 by Tej Chajed.
The exercises in each chapter are surrounded by // FIXME and // END; you're
not supposed to modify text outside these markers. When you're done we suggest
you change FIXME to DONE, but this isn't required.
- Chapter 0: Making sure your IDE is set up for Dafny (see installation instructions below).
- Chapter 1: Learn some fundamental Dafny syntax and concepts.
These assignments will have you defining and verifying protocols in Dafny, a verification-aware programming language.
We highly recommend using VS Code. Dafny is an interactive tool, and the VS Code extension makes it easy to use it interactively. If you're used to vim keybindings, the vim extension is quite good.
Install the Dafny
extension.
From within VS Code you can do this by clicking on the Extensions icon in the
left side bar and searching for dafny-lang.ide-vscode. If you're more
familiar with the command line, code --install-extension dafny-lang.ide-vscode will also work.
You'll need to install .NET 6 and the ASP.NET Core Runtime to run Dafny (you won't need to interact with these tools except for installing them). If you don't have them, the Dafny extension will tell you. The simplest way to do this is to install the SDK from https://dotnet.microsoft.com/en-us/download/dotnet/6.0.
On macOS, you can instead use brew install dotnet@6 and then in VS Code set
the option "Dafny: Dotnet Executable Path" to the output of echo $(brew --prefix dotnet@6)/bin/dotnet.
If you get stuck on something Dafny related, you might find what you need in a syntax tutorial I wrote, or you can check out the Dafny getting started guide.
I recorded a Dafny debugging video of the "toy consensus" example (code here) that illustrates how to come up with an inductive invariant and debug an inductiveness proof.