Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
Varun Pant introduces formal verification as the solution to reliably validate AI-generated code, proposing a division where humans define specifications and machines handle code and proof. He details Lean's role as a unified language for code and proof, exemplified by an AI rewriting zlib with 32,000 lines of proof, and AWS's Cedar using Lean specs with Rust production code reconciled by 100 million nightly tests. The talk also covers deductive verification with solvers and future cross-language verification with Strata, aiming for "provably correct" software.
Formal verification offers a definitive solution to the problem of ensuring correctness for the vast amount of code generated by AI agents, a challenge that current methods like probabilistic LLM judgments, partial test coverage, and unscalable human review fail to address. Varun Pant, leading AI product and formal verification teams at AWS, highlights that formal verification provides mathematical proof that code is correct for all inputs, contingent on a well-defined specification. The proposed methodology establishes a clear division of labor: humans own the specification, while machines own the code and the proof. This process begins with specification-driven development, where specifications are either formally written (e.g., in Lean) or auto-formalized by AI from natural language. A critical step is the validation of the specification, either through human review or testing against real inputs, because as the upstream “living, breathing artifact,” its correctness is paramount to everything downstream. The AI coding agent then implements the code from this validated specification, and a formal verification tool proves the implementation matches the specification. Lean serves as a powerful core tool, functioning as both a programming language and a proof assistant. It uniquely uses the same language for definitions and proofs, eliminating translation layers and offering extensibility due to being implemented in Lean itself. A key feature is its small, trusted kernel, which independently checks proofs. The process of proof generation in Lean is likened to chess: tactics are “moves” used to navigate an interactive “chessboard” (the proof goal), attempting to reach “checkmate” (proving a theorem). If a branch of tactics fails, backtracking is employed until a successful proof is found, which is then confirmed by the independent kernel. This kernel, which can be rebuilt and is open-source, is the only component that needs to be trusted. Several practical applications demonstrate this approach: * Zlib Rewrite in Lean: Andreo.AI’s effort to convert the C compression library zlib into Lean resulted in an AI decomposing the problem into lemmas, proving each with tactics, and assembling them into a final theorem. This single endeavor generated an astonishing 32,000 lines of proof, all checked by the Lean kernel. * Cedar (Lean Semantics, Rust Production): AWS uses Lean to define the functional specification of Cedar, an open-source authorization policy language. While the production code runs in Rust, rigorous differential random testing (100 million tests nightly) ensures that the Rust implementation consistently aligns with the Lean specification for all inputs before any version is shipped. * Deductive Verification with Solvers: For Rust code, Lean can be used with powerful “calculators” called solvers (e.g., Z3, utilized by Verus). This involves adding specifications as annotations like requires (pre-conditions) and ensures (post-conditions) to the code. These are static checks enforced by a verifier and erased at runtime, acting like “ghost code.” Tools like Eneus also translate Rust’s intermediate representation to Lean for theorem proving. Looking ahead, AWS is developing Strata, an open-source tool aiming to standardize formal verification across any programming language. Strata introduces a “dialect” (compiler-like) approach, translating high-level code into a low-level intermediate representation called Strata Core, which is written in Lean. This universal core allows programs to be dispatched to various verification engines, including the Lean proof assistant, SMT solvers, or model checkers. The ultimate vision is a future where software and systems are not merely “probably correct,” but “provably correct.”