Multi-Modal Verification of Distributed Systems in Lean
summary
Framework called Veil (Lean library) encodes transition systems as shallow Lean programs, generates verification conditions sent to SMT solvers and falls back to interactive proofs inside Lean when automation times out. It performs SMT-powered symbolic model checking (finite-depth, can produce concrete traces), proves equivalence between weakest-precondition and big-step semantics, and finds inductive invariants (it even exposed a porting typo in a prior IV+Isabelle formalization). Automation is usable but currently slower than Ivy/IV by about an order of magnitude.
AI-written summary · about
chapters (9)
- 0:00Multi-modal verification intro
- 1:27Distributed protocol motivation
- 16:35Whale framework intro
- 20:24Leader election demo
- 36:18Invariants and induction
- 46:37Implementation details
- 51:49Case studies and performance
- 55:24Conclusion and future work
- 56:57Q&A
related talks
19mVelvet: A Multi-Modal Verifier for Effectful Programs
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
19mAutomated Verification of Fundamental Algebraic Laws
46mRefinement Types from Light to Deep Verification
13mInteractive Bit Vector Reasoning using Verified Bitblasting
01h 02mLanguage Design meets Verifying Compilers
21mVerifying term graph optimizations using Isabelle/HOL