Velvet: A Multi-Modal Verifier for Effectful Programs
summary
Velvet is a Dafny-style verifier implemented as a Lean library that verifies imperative programs with mutable state, loops, and nondeterminism by generating Lean goals and discharging them via SMT and interactive proofs. It uses CVC5 for automated VCs, supports partial/total correctness modes and demonic choice vs existential semantics for nondeterminism, and plugs to LLMs to fill hard proofs (demo: 15 initial goals for a prime checker, CVC5 solves most, LLM closes the remaining proof; a memory-allocator left 7 goals and AI constructs a small theory to finish them). Property-based testing finds counterexamples (example: repeated -8) and termination annotations are required for total proofs.
AI-written summary · about
chapters (10)
- 0:00Velvet introduction
- 1:38Imperative programs in Lean
- 3:27Multi-modal semantics
- 5:57Property-based testing
- 7:22Partial vs total correctness
- 9:11Combining proofs
- 10:36AI for interactive verification
- 13:30AI-assisted verification
- 15:00Forward pointers
- 15:45Q&A
related talks
01h 01mMulti-Modal Verification of Distributed Systems in Lean
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
21mVerified VCG and Verified Compiler for Dafny
19mAutomated Verification of Fundamental Algebraic Laws
01h 02mLanguage Design meets Verifying Compilers
46mRefinement Types from Light to Deep Verification
23mVellvm: Formalizing the Informal