Why AI-generated code needs mathematical proof, not just tests

Varun Pant presents formal verification as a complement to AI-generated code, not a replacement for testing. The key insight is that Lean provides mathematical proofs for all inputs, unlike the probabilistic nature of LLM-as-judge or the limited coverage of unit tests.

The methodology centers on back-driven development: humans write specifications (manually or via AI auto-formalization), then AI agents implement code while Lean proves correctness. The specification becomes the critical artifact that must be validated upstream—everything else flows from it.

Practical examples include AWS's Cedar policy language, where Lean specifications run 100 million differential random tests nightly against Rust production code, and AI-assisted conversion of zlib (32,000 lines of proof). No version ships until verification passes.

The tradeoff is upfront investment: teams must write precise specifications and learn Lean's interactive theorem-proving approach. This is not yet mainstream, but for critical systems, it offers certainty that testing and code review cannot provide.