Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
summary
Extracts execution paths from Dafny into a tiny Boogie-like language, embeds a fragment of Dafny semantics into Lean, and implements a verified weakest-precondition generator that spits out Lean proof obligations for each path. Prototype handles non-heap fragments (primitive ints, chars, lists), demonstrates on a string-split case study, and finds that interactive proofs are tractable but require many boilerplate lemmas; the approach uses straight-line micro-Boogie extraction and relies on Lean for semi-manual discharge.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:04Dafny’s automation limits
- 2:05Lean for program verification
- 3:52String splitting example
- 5:56Debugging Dafny errors
- 8:04Extracting straight-line programs
- 11:15Proof paths in microBoogie
- 13:21Prototype tool results
- 14:25Improving Dafny UX
- 15:49References and conclusion
- 16:34Q&A
related talks
01h 02mLanguage Design meets Verifying Compilers
21mVerified VCG and Verified Compiler for Dafny
19mVelvet: A Multi-Modal Verifier for Effectful Programs
14mEmbedding Quantum Program Verification into Dafny
01h 01mMulti-Modal Verification of Distributed Systems in Lean
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
18mDeferring the Details and Deriving Programs
03mAttempts to design hardware using dafny