Enhancing Proof Stability
summary
Claim: simple, low-automation proofs break less often. Implements a coding style called Dafny64 that makes invariants opaque, moves postconditions into explicit lemmas, and reveals function bodies only when needed. Uses Z3’s resource count and 5 random seeds to measure brittleness via coefficient of variation (threshold 0.2). On a 177,000-line Dafny codebase the string module drops Z3 resource use by ~100× and wall time by ~100×, eliminating all VCs above the 0.2 threshold at the cost of more lemma code.
AI-written summary · about
chapters (19)
- 0:00Proof stability challenges
- 1:03DNE at AWS scale
- 2:26Proof brittleness impact
- 4:35Proof brittleness causes
- 5:39Proof hardness and DNE 64
- 6:00Measuring proof complexity
- 7:24DNE 64 simplification
- 7:44Opaque invariants in loops
- 9:09Removing postconditions
- 10:14DNE 64 proof simplicity
- 10:35Proof simplification results
- 11:38Brittleness with random seeds
- 13:04Reducing brittleness with DNE 64
- 14:07Code size impact of DNE 64
- 15:12Conclusion and future work
- 16:14Q&A: Automating DNE 64
- 17:39Q&A: Impact on clients
- 18:44Q&A: Postconditions in methods
- 19:47Q&A: Default DNE 64 style
related talks
15mOn the Impact of Formal Verification on Software Development
24mTooling Infrastructure for Zero Knowledge Proofs
01h 10mMedium-scale automation for proof assistants
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
21mLive Verification in an Interactive Proof Assistant
15mAdaptable Traces for Program Explanations
19mQED in Context: An Observation Study of Proof Assistant Users
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...