In this post, we will show how to specify and verify imperative programs in Lean 4 using Velvet—an embedded verifier, which relies on a combination of automated symbolic and AI-assisted theorem proving techniques.
Disclaimer: At the time of writing, Velvet is distributed as part of the Loom framework. Velvet is currently under active development by VERSE Lab, as we are working to improve its expressivity and performance. It’s likely that its codebase will soon be moved to a separate repository. Nevertheless, the code linked in this post will remain accessible.
Formal program verification is about telling what a program should do without telling how it should do it and then mathematically proving that the program indeed does exactly that. The what is given by a program specification—a logical statement that describes the assumptions on the program’s input and the properties that should hold true about its outcomes.1
Getting Started: Specifying and Verifying Functional Programs
The Lean 4 theorem prover allows one to write a program and also to state its specification in the form of a mathematical theorem. For instance, the following code fragment shows a function append that concatenates two lists of integers and a theorem append_assoc that states and proves the function’s associativity (meaning that the result of concatenating three lists does not depend on the order in which we perform concatenation—only on the position of the arguments).
def append (xs ys : List Int) : List Int :=
match xs with
| [] => ys
| x :: xs => x :: append xs ys
theorem append_assoc (xs ys zs : List Int) :
append (append xs ys) zs = append xs (append ys zs) := by
induction xs with
| nil => rfl
| cons x xs ih => simp [append, ih]
The proof of append_assoc is done by induction on the shape of the first argument of the append function (i.e., the list “on the left side” of the concatenation), and its details are not that important for now: it suffices to say that it closely mimics the paper-and-pencil argument that argues for the validity of the theorem’s statement by considering two different ways lists can be constructed.