Lessons from Building an Auto-Active Verifier in Lean
summary
Veil is an auto‑active verifier implemented as a Lean library that does concrete and symbolic model checking, bounded searches, and inductive‑invariant discovery with SMT proofs reconstructed via CVC5. The team rewrites Veil into a VC manager architecture to separate elaboration, asynchronous discharge, and the UI, fixing maintainability problems from heavy meta‑programming. Performance currently sits around ≈10× slower than IV due to higher‑order→first‑order translation but aims for 2–3× with engineering; the code is open and runnable at try.veil.dev.
AI-written summary · about
chapters (9)
- 0:00Auto-active verification intro
- 1:29Tooling trade-offs for protocols
- 5:03Problems with verifier architectures
- 7:11Veil and its Lean foundation
- 11:28Lessons building Veil in Lean
- 13:55Complexity of front-end tools
- 16:28Model-view-controller for verifiers
- 17:53Performance challenges and future work
- 18:14Q&A