Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean

Explore a 19-minute conference talk that examines the integration of Lean interactive theorem proving with Dafny automated verification. The presentation, delivered at the Dafny 2025 workshop by researchers from University College London and Amazon Web Services, introduces a methodology for handling complex program verification challenges. Learn how the team extracts straight-line programs for execution paths, embeds Dafny's semantics into Lean, and provides a verified weakest-precondition generator. Discover why Lean's semi-manual interactive proving approach can be valuable when dealing with difficult Dafny proofs, particularly for programs with non-local control flow where automated SMT solvers might struggle to provide visibility into proof states.