Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
Formal verification with Lean4 can mathematically prove AI-generated code correct for all inputs.
“Humans own the specification and machines own the code and proof.”
AWS engineer Varun Pant argues that as coding agents generate code at scale, traditional verification methods—LLM judges, tests, human review—all fail to guarantee correctness across all inputs. He proposes formal verification using Lean4, where humans write specifications and AI agents implement and prove correctness mathematically. The talk introduces a spec-driven workflow (referencing AWS's Kiro) where the division of labor is humans own specs, machines own code and proofs.