Key Takeaways
- Pant's framing of the gap: LLM-as-judge is probabilistic, tests "only check some inputs, not all," and human code review doesn't scale to agent speed — only a proof covers every possible input.
- His proposed division of labor: "humans own the specification and machines own the code and proof."
- Cedar, the open-source authorization policy language, keeps its specification in Lean and its production code in Rust, cross-checked by about 100 million differential random tests nightly — and no version ships until they pass.
- In one open-source example he cited, AI converted zlib (a C compression library) to Lean over roughly a week, producing 32,000 lines of proof that Lean's small kernel then checked.
“Coding agents are generating more code than ever,” Varun Pant opened. “Builders are generating hundreds and thousands of PRs every week. How do you know that this is correct?” His answer: none of the checks we currently reach for can answer that honestly, and formal verification can. Pant builds AI products at AWS, where he leads teams working on formal verification, and his AI Engineer talk argues that Lean belongs inside the agent loop.
The three checks that don’t close the gap
Pant’s setup lands because every team shipping agent-written code has felt it. Using an LLM as a judge for code? “Well, that’s probabilistic.” Tests? “They only check some inputs, not all.” Human code review? It “doesn’t scale to match agent speed.” His conclusion is one sentence: “None of these can say for all inputs the code is correct. Formal verification can.”
That is narrower than it first sounds. He is not saying LLM judges and tests are worthless — only that they cannot make a universal statement. A passing test suite tells you about the inputs you thought of; a model-graded rubric tells you about a sample. Our guide to running evals as a team covers what that sampled confidence buys and where it stops, and Uber’s uReview is a serious attempt at scaling review that is still sampling behavior rather than proving it. Formal verification, in his definition, “provides mathematical proof that code is correct. For all inputs… If the proof passes, it holds for every possible input.”
Humans own the spec, machines own the code
The workflow he describes is spec-driven development, and he names Kiro as one way to do it. You write what correct means — either formally, directly in Lean, or in natural language that the AI auto-formalizes.
Then comes the step he flagged hardest: “Now, this is really important. You then validate the specification.” Either a human reviews it, or you test that it holds on some inputs. The specification sits upstream of everything else — “it’s a living, breathing artifact that the builder interacts with. You want this to be correct. Everything else is downstream from this.”
Only then does the coding agent implement from the specification, and the verification tool prove the implementation matches. He compressed the arrangement into one line: “So, humans own the specification and machines own the code and proof.”
Note what that implies: the review burden does not disappear, it moves. Instead of reading the diff an agent wrote, you read the formal statement of what the code should do — a smaller artifact but a denser one, and if you get it wrong the proof will certify the wrong thing.
What Lean is, and the chess analogy
Lean “is a programming language and a proof assistant. It is the same language for the definitions and proofs. There’s no translation layer.” It is implemented in Lean, which makes it very extensible; it has a small trusted kernel, and proofs can be exported and independently checked.
His demo file shows both halves at once: a function that reverses a list, and below it a theorem proving that the reverse of A appended to B equals the reverse of B appended to the reverse of A, for every possible input.
How that proof gets built is the clearest teaching moment in the talk. In chess your goal is checkmate, and you make a series of moves; in Lean, tactics are the moves and the theorem is checkmate. “You’re kind of going down a tree. So, you’re traversing the tree, you’re trying different tactics. Maybe for some goals, you’re not able to prove it, so you backtrack and then you try another branch of the tree.” Tactics do the work; the kernel checks the work.
That kernel is what makes this trustworthy rather than merely elaborate. An incorrect proof is rejected immediately, and you only need to trust the kernel — not the tactics, not the agent that wrote them. Nor must you trust one implementation: independent kernels exist in C++, Rust, and Lean, all open source, and Pant noted you could write one yourself.
Case one: spec and code both in Lean
His first worked example is a zlib port. An open-source project he cited had AI convert zlib, a C compression library, into Lean — “granted this happened over a week or so.” The natural-language specification: decompressing the output of compress returns the original data. An AI generated the formal spec from that; then, after the spec was checked, it wrote the Lean code, generated helper lemmas as subgoals, and proved the theorem. The result was 32,000 lines of proof, verified by the small independent kernel.
His summary of the pattern is the part to steal: “AI decomposed the problem into lemmas, which are subgoals. It proved each of them using tactics… and it assembled it into a final theorem. Checkmate. And the kernel checked it.” Decompose, prove locally, assemble, then let a small trusted component check the whole thing — a familiar agent architecture with an unusually strong verifier at the end.
Case two: spec in Lean, production code in Rust
Cedar is his second example: an open-source authorization policy language, which he said is used by AWS Verified Permissions and Verified Access. Its specification is written in Lean; its production code runs in Rust.
The property he used to motivate it is one any authorization engineer knows: forbid trumps permit. For any forbid policy that is satisfied, the request must always be denied. To connect the Lean model to the Rust implementation, the team runs differential random testing — same inputs into both, check for the same output. Pant put the volume at about 100 million differential random tests run nightly, and added the rule that gives it teeth: “No version ships until this is satisfied.”
This is the pragmatic middle path: you do not rewrite production in a proof language, you write a Lean model of what it should do and bind that model to the real code with an enormous randomized test loop.
Case three: solvers, pre/postconditions, and any language
For deductive verification of Rust, Pant introduced solvers with a deliberately unglamorous metaphor: a solver is “a calculator, a very powerful one.” Feed in a formula, get back satisfiable or unsatisfiable. Lean is the interactive chessboard; the solver is the calculator.
Verus is his example, an open-source tool that uses the Z3 solver. It reads like annotations: requires and ensures keywords in line with the code, the precondition and postcondition — what must be true before, what must be true after. It is a static check, “enforced by the verifier and erased at runtime. So, almost like ghost code.” Aeneas takes a different route to the same place, consuming Rust’s mid-level intermediate representation and doing a functional translation into Lean, which puts you back on the same chessboard.
For everything else there is Strata, an open-source AWS tool Pant explicitly labeled work in progress. Any language can get a dialect, structured like a compiler: a high-level intermediate representation lowered into a low-level one called Strata Core, itself written in Lean. Once every program speaks Strata Core, you dispatch it to whichever engine fits — the Lean proof assistant, SMT solvers, or model checkers.
What happens next
Pant’s closing ask is deliberately small: open Lean in your browser, pick your most critical code, write what correct means, then let your coding agent implement it and the verification tool prove it. Not your whole codebase — your most critical code.
That scoping is the honest read of the talk. Nothing in it suggests proving an entire product is tractable today: the zlib example took about a week and 32,000 lines of proof for one compression library, and Strata is unfinished by his own admission. What has changed is the cost curve on the machine side of the split — writing those 32,000 lines was the bottleneck, and agents that decompose goals and grind tactics attack exactly that, while the human keeps the part that was always interesting.
The near-term bet worth watching is the Cedar pattern rather than the zlib one: a Lean model of the critical invariant, production code in whatever you already ship, a differential test loop wired into the release gate. Most teams could adopt that without hiring a proof engineer, and it fits how agent-written code is already landing in production — the same tension runs through Stripe’s account of shipping a vibe-coded billing engine, where the question is never whether the agent can write it but what you check it against. Pant’s ending line is the pitch: software that is not probably correct, but provably correct.
Quick poll
Which half of the split would you rather own on your team?
Pant's rule: "humans own the specification and machines own the code and proof" — and he flagged validating the spec as the step everything else depends on.
FAQ
Does formal verification mean I can stop writing tests? Not in the workflow Pant described. Tests are one way to validate the specification itself — he said you either have a human review the spec or “test that it holds on some inputs” — and in Cedar, about 100 million differential random tests nightly tie the Lean model to the Rust code.
What is the difference between Lean and a solver like Z3? Pant’s analogy: Lean is an interactive chessboard where tactics are moves and you backtrack through a tree of goals. A solver is “a calculator, a very powerful one” — feed it a formula, get satisfiable or unsatisfiable. Verus uses Z3; Aeneas instead translates Rust into Lean.
Do I have to trust the whole Lean toolchain? No — that is the point of the small kernel. Tactics do the work and the kernel checks it, so an incorrect proof is rejected immediately. Independent kernels exist in C++, Rust, and Lean, all open source.
Can I apply this to a language that isn’t Lean or Rust? That is the goal of Strata, the open-source AWS project Pant described: define a dialect for your language, lower it into Strata Core, then dispatch to a Lean proof, an SMT solver, or a model checker. He was explicit that it is work in progress.
