Pant frames formal verification as the missing correctness layer for software produced at agent speed. Tests exercise selected examples, human review does not scale, and an LLM judge is probabilistic, while a machine-checked proof can establish that an implementation meets its specification for all possible inputs.
The proposed workflow keeps humans responsible for the specification and delegates implementation and proof construction to machines. Teams can write a specification directly in Lean or translate natural language into a formal statement, but Pant stresses that reviewing and testing that upstream specification remains essential because every later artifact depends on it.
Lean combines definitions, programs and proofs in one language, backed by a small trusted kernel that independently checks generated proof terms. Pant illustrates this with list reversal and a large AI-assisted conversion of zlib to Lean, where the system decomposed a theorem into lemmas, searched through tactics and assembled tens of thousands of proof lines for kernel verification.
He also shows ways to verify production code outside Lean. AWS Cedar keeps its formal model in Lean and compares it against Rust with extensive differential testing, Verus adds preconditions and postconditions to Rust for SMT checking, and the experimental Strata project aims to translate multiple programming languages into a common verified representation.
Watch on YouTube
