On the Impact of Formal Verification on Software Development
summary
Auto-active verifier Dafny is studied via 14 interviews using grounded theory and the paper reports concrete pain points: SMT queries balloon to 5 GB of SMT queries in one project, error messages routinely fail to explain simple math, and users debug by inserting assertions as breakpoints and building a mental model of the verifier state. Proofs are brittle to trivial edits, so developers adopt disciplined refactorings and propose tooling like a verifier-focused linter and visualizing verifier context to make proofs robust and reviewable.
AI-written summary · about
chapters (10)
- 0:00Formal verification impact
- 1:04Why verification remains niche
- 2:27User-centric verification tools
- 4:37Proof debugging without debug
- 6:21Debugging with assertions
- 8:28Brittle proofs robustness
- 10:30Code reviews overload
- 12:36Summary and future directions
- 13:17Q&A verification linter
- 14:41Q&A adoption by devs
related talks
01h 02mLanguage Design meets Verifying Compilers
19mVerifying Dafny Contract Integrity
21mEnhancing Proof Stability
46mKeynote: Formal Verification? No, Formal Reasoning!
19mLearn 'em Dafny
16mIncremental Proof Development in Dafny with Module-Based Induction
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination