Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
summary
Proposes a proof system that breaks a single complex inductive invariant into incremental steps and proves each rule sound, implemented as a checker in myvy and applied to 12 Paxos variants plus Raft with reusable artifacts. Uses forward-backward proof rules to reduce Boolean structure and prophecy witnesses to replace quantifier alternations by explicit witnesses whose soundness is discharged by a small safety subproof (monitor relation). Shows any incremental proof yields a single inductive invariant (usually more complex) and reports successful manual proofs in the case study.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:06Traditional safety verification
- 3:13Forward-backward reasoning
- 8:07Prophecy for quantifiers
- 11:35Proof system rules
- 12:40Case study results
- 14:30Future research
- 15:15Q&A
related talks
19mAutomated Verification of Fundamental Algebraic Laws
30mProof Logging for Constraint Programming
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
46mRefinement Types from Light to Deep Verification
30mRelatively Complete Verification of Probabilistic Programs
15mA systematic approach to "Well-founded recursion done right"
01h 34mFormal Logic Undressed
15mProducts of Recursive Programs for Hypersafety Verification