The Design of an Interactive Proof Mode for Dafny

on YouTube ↗18m

" summary

Prototype interactive proof mode for Dafny that back-translates SMT-LIB VCs (generated via Boogie and Z3) into Dafny-like goals using injected protect_ helper functions, parsing hacks, and a single compilation run. Demonstrates a six-step proof of the xx+1 divisible-by-2 lemma using tactic primitives check, case, and assert*; tactics run offline against the parsed VC so no repeated recompiles. Works on a restricted Dafny subset, outputs copyable Dafny proof code, on GitHub, and needs broader language support and empirical validation.

AI-written summary · about

" chapters (8)

1. 0:00Interactive proof mode intro
2. 2:09Dafny verification limits
3. 5:24Benefits of theorem provers
4. 6:06User perspective
5. 8:57Proof mode design
6. 12:31System architecture
7. 13:56Limitations and future
8. 15:03Q&A