Pant frames formal verificationFormal verification uses mathematical logic and machine-checked proofs to establish that a system satisfies a precisely stated specification. 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 proofA machine-checked proof is a formal proof whose logical steps are represented in a form that a small verification program can independently validate. 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 statementA formal specification is a precise mathematical description of a system's required behavior, inputs, outputs and constraints., 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 languageLean is a proof assistant and functional programming language used to define mathematical objects, write programs and create machine-checked proofs., backed by a small trusted kernelA trusted kernel is the small core of a proof system that independently checks whether formal proof terms are valid under the system's logical rules. 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
