Slides: Chapter 1 (Dafny mechanics)
Slides: Chapter 2 (Specification)
Slides: Chapter 1 & 2 Epilogue
Slides: Chapter 3 (State machines and behaviors)
Slides: Review of Day 3 solutions
Slides: Chapter 4 (Proving properties)
Slides: Leader Election invariant discovery demo
Slides: Chapter 5 (Modeling distributed and asynchronous systems)
Slides: Midterm project (Distributed lock)
Slides: Midterm review and Chapter 6 exercise preview
Slides: Chapter 6 (Refinement)
Slides: Chapter 7 (Asynchronous specs)
Slides: Chapter 8 (Application correspondence)
Slides: Chapter 9 (Multi-level refinement)
Slides: Chapter 10 (Modules and automation)