Summary
Varun Pant, an AWS engineer leading formal verification teams, makes the case that as AI coding agents generate hundreds of thousands of pull requests per week, probabilistic checks — LLM-as-judge, unit tests, human review — are fundamentally insufficient. Only formal verification can guarantee correctness for all possible inputs, not just tested ones.
The talk centers on Lean4, a programming language and proof assistant where code and mathematical proofs live in the same file with no translation layer. Pant walks through a practical workflow he calls spec-driven development: humans write or approve a formal specification, an AI coding agent (such as Kiro) implements from that spec, and a proof assistant verifies the implementation matches. A small, independently auditable kernel checks all proofs. He illustrates with the open-source conversion of zlib — a C compression library — into verified Lean code spanning 32,000 lines of proof, and with AWS Cedar, an authorization policy language whose Lean specification is differential-tested against Rust production code via 100 million nightly randomized runs.
Pant also introduces solver-based verification as a complement to interactive tactics, and closes with a clear division of labor: humans own specifications, machines own code and proofs. For teams building on AI-generated codebases, the talk offers a concrete architectural pattern for making correctness guarantees that scale with agent velocity.
📺 Source: AI Engineer · Published August 28, 2026
🏷️ Format: Deep Dive
