A short tutorial for Velvet, a Dafny-style verifier for imperative programs embedded in Lean.
Open the chapters in VS Code and read them in order. Each one is a Lean file you can step through, with explanations in comments.
| Chapter | Covers |
|---|---|
| Tut01Intro | Methods and contracts, prove_correct, verifyOnDefinition, while/for loops, arrays, assert, method calls, finding bugs by testing vs. proving their absence |
| Tut02Termination | Total vs. partial correctness, loops without a termination measure, break, recursion by induction and by fixpoint induction |
| Tut03EffectsAndNonDet | Stateful programs (StateT), exceptions (signals), composing stateful methods, demonic and angelic choice |
| Tut04InteractiveProofs | When finish fails: the VC report, with try finish and case <label>, teaching grind a lemma with grind_pattern |
| Tut05GhostState | Ghost state: a StateT (Ghost Nat) step counter proving binary search takes at most log₂ n + 1 steps |
lake buildThe tutorial pins Velvet at tag v2.0 (Lean v4.34.0).