🎤 Verification Talk & Demo: Interactive Proof Mode for Dafny

We’re excited to welcome Ștefan Ciobâcă for a special guest talk on his work “The Design of an Interactive Proof Mode for Dafny.”
Dafny is well known for its powerful automated verification, but anyone who has worked on non-trivial proofs knows that automation alone isn’t always enough. In this session, Ștefan will present a new interactive proof mode for Dafny, designed to give users more control and insight when automation falls short.
In this talk, we’ll cover:

• The motivation behind adding an interactive proof mode to Dafny
• Key design decisions and challenges in integrating interactivity with Dafny’s verifier
• How interactive proofs complement automated verification
• A live demo showing the interactive proof mode in action
• Discussion of use cases, limitations, and future directions

Why attend:
If you’ve ever struggled to guide Dafny through a tricky proof, wondered how interactive proof assistants compare to automated tools, or are curious about the future of proof engineering in Dafny, this session will be highly relevant.
There will be time for questions and discussion after the talk.
All experience levels welcome — familiarity with Dafny is helpful but not required.
We hope you can join us for this deep dive into the evolving verification tooling ecosystem!