Velvet
Velvet is an extensible program verifier for executable imperative programs in Lean 4. Implement algorithms in a natural style, specify their behaviour, and formally prove their correctness with Lean's state-of-the-art automation, mathematical libraries, and your favourite AI system.
Why Velvet
Ideal for Teaching Program Correctness
Velvet is designed to be intuitive and easy to use. It lets you write executable code with loops, mutation, and non-determinism. Its proofs automate away mundane obligations, so one can focus on the interesting bits of algorithmic reasoning.
Multi-Modal Verification
Programs in Velvet can be run, tested, and verified for correctness with respect to ascribed specifications in a variety of modes: using automated methods (SMT solvers, Lean's grind) and interactive proofs driven by a human or AI.
Lightweight and Foundational
Velvet is implemented as a library in Lean, so it can use any Lean definitions, including the entirety of Mathlib, the world's largest mathematical library. Velvet is foundational: its correctness does not rely on any non-standard axioms and is checked by Lean's kernel.
Feature-Rich Programming Model
Beyond "does it return the right answer", Velvet lets you track proof-only data (ghost state), reason about choices made either in your favour or against you (angelic and demonic nondeterminism), and prove programs correct whether or not they terminate. More exciting features are on the way.
See It in Action
Insertion sort, specified and verified. Automation discharges most of the proof; the remainder is left as an ordinary Lean goal, labelled with the invariant name.
import Velvet
-- Ordinary Lean definitions
@[grind] def cnt (a : Array Int) (x : Int) : Nat := a.toList.count x
@[grind] def sameElems (a b : Array Int) : Prop := ∀ x, cnt a x = cnt b x
@[grind] def SortedUpTo (a : Array Int) (n : Nat) : Prop :=
∀ i j, i ≤ j → j < n → a[i]! ≤ a[j]!
method insertionSort (arr : Array Int) returns (res : Array Int)
requires size_pos: arr.size > 0
ensures sorted: SortedUpTo res res.size
ensures elems_same: sameElems res arr
do
let mut res := arr
let mut n : Nat := 1
while loop_cond: n ≠ res.size
invariant sz_inv: res.size = arr.size
invariant n_le: n ≤ res.size
invariant sorted_prefix: SortedUpTo res n
invariant elems_inv: sameElems res arr
decreasing by_size: res.size - n
do
let mut mind := n
while inner_cond: mind ≠ 0
invariant inner_sorted:
∀ i j, i ≤ j → j < n + 1 → j ≠ mind → res[i]! ≤ res[j]!
decreasing by_mind: mind
do
if res[mind]! < res[mind - 1]! then
let tmp := res[mind]!
res := res.set! mind res[mind - 1]!
res := res.set! (mind - 1) tmp
mind := mind - 1
n := n + 1
return res
prove_correct insertionSort by
velvet_vcgen [insertionSort] with try finish
case inner_sorted =>
intro i j hij hj_bound hj
by_cases hj_m : j = mind
· subst hj_m
rcases Nat.lt_or_eq_of_le hij with hi | rfl
· exact Int.le_trans
(inner_sorted i (j - 1) (by omega) (by omega) (by omega)) (by omega)
· grind
· exact inner_sorted i j hij hj_bound hj_mGet Started in Minutes
Add Velvet to your Lean 4 project and write your first verified method.
In your lakefile.toml:
[[require]]
name = "velvet"
git = "https://github.com/verse-lab/velvet.git"
rev = "main"Give an algorithm a contract:
import Velvet
method max (a b : Nat)
returns (r : Nat)
requires True
ensures r ≥ a ∧ r ≥ b ∧
(r = a ∨ r = b)
do if a ≥ b then return a
else return bDischarge the verification conditions:
prove_correct max by
velvet_vcgen [max] with finishFrom the same lab
A multi-modal verifier for distributed protocols, also built in Lean. Veil specifies, tests, and proves safety properties of state transition systems in the style of TLA+.