Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
Description
An AI spent about a week rewriting zlib in Lean and emitted 32,000 lines of proof. Not tests, proof. It decomposed the job into lemmas, closed each one with tactics, assembled them into a single theorem, and a small independent kernel checked the result. Varun Pant opens on the gap that makes this worth caring about now. Coding agents are producing hundreds or thousands of pull requests a week, and none of the usual checks actually clear them. A model grading code is probabilistic, tests cover the inputs someone thought of, and human review does not scale to agent throughput. None of the three can say the code is correct for every input. His division of labor is the memorable part: humans own the specification, machines own the code and the proof. That puts all the weight on the spec being right, which is why he insists on validating it before anything downstream runs, whether a person reviews it or it gets tested against real inputs. The chess analogy carries the rest, with tactics as moves, a theorem as checkmate, and backtracking when a branch will not close. AWS runs this in production on Cedar, whose authorization semantics live in Lean while the shipping code is Rust, reconciled by roughly 100 million differential tests nightly. Nothing ships until they agree. Speaker info: - https://x.com/varun_pant_ - https://www.linkedin.com/in/varunp1/ Timestamps: 0:00 - Why none of the usual checks clear agent output 1:06 - Specifications humans own, proofs machines own 2:00 - Lean as one language for code and proof 3:01 - Tactics, theorems, and the chess analogy 3:58 - A small kernel you can independently rebuild 4:52 - Rewriting zlib into Lean, and 32,000 lines of proof 6:44 - Cedar: Lean semantics, Rust in production 7:40 - Solvers, preconditions, and code erased at runtime 8:37 - Bringing any language into the same core
Summary
Generated by gpt-5.6-terraAt-a-Glance
- Verdict: Watch fully
- Core thesis: As coding agents accelerate code production beyond the capacity of review and tests, formal verification can make agent-generated software trustworthy by proving an implementation satisfies a human-approved specification for all inputs.
- Why it matters: This presents a practical control-plane pattern for AI coding: move human oversight upstream to specifications, let machines generate code and proofs, and use independently checkable proof artifacts rather than probabilistic evaluation alone.
- Best use: Use it to frame a pilot for formally verifying a narrow set of high-consequence invariants, especially authorization, policy evaluation, cryptographic, or core workflow logic produced or modified by coding agents.
Executive Summary
Varun Pant argues that conventional safeguards do not scale to the volume of code generated by AI agents. LLM-as-judge is probabilistic, tests cover only selected inputs, and human review cannot keep pace with hundreds or thousands of agent-created pull requests. Formal verification addresses a different and stronger question: whether code satisfies a defined specification for every possible input.
The operating model is specification-driven development. Humans write or approve the definition of correct behavior—either directly in Lean or initially in natural language and then AI-formalized—while an agent writes the implementation and generates a machine-checkable proof. Pant stresses that specification validation is the critical human responsibility: a flawless proof of the wrong specification is still the wrong system.
Lean is positioned as a useful foundation because it combines a programming language and proof assistant, allowing definitions and proofs to live in one language with no translation layer. Its small trusted kernel checks proof results, and proofs can be exported and independently checked, narrowing the trusted computing base relative to trusting a generative model or a large verification workflow.
The talk gives a maturity ladder rather than claiming every codebase must be rewritten: implement and prove directly in Lean; keep production code in Rust but maintain a Lean functional model and differential-test them; or use Rust-oriented deductive verification tools such as Verus and Aeneas. AWS's work-in-progress Strata/"Starter" concept aims to lower multiple languages into a Lean-based core representation and route verification to Lean, SMT solvers, or model checkers.
Key Takeaways
- Claim: Formal verification is the appropriate complement to agentic coding when the requirement is correctness over all inputs, not merely confidence from sampled tests or reviews. | Evidence: Pant contrasts formal proof with LLM judging, conventional tests, and human code review, arguing that none of those can establish that code is correct for every possible input; a verifier proves that an implementation satisfies its formal specification. | Implication: For high-impact agent-generated changes, Ken should distinguish test-based confidence from proof-backed guarantees and reserve formal methods for explicit invariants where the added assurance changes the risk posture. | Caveat: A proof establishes conformance to the specification, not that the specification captures the real business, security, or user requirement.
- Claim: The key governance boundary is 'humans own the specification; machines own the code and proof.' | Evidence: The proposed workflow is: write a specification of correct behavior; optionally use AI to formalize a natural-language version; validate that specification through human review or sample testing; then have the coding agent implement it and the verifier prove compliance. | Implication: An AI engineering process should require explicit, reviewable invariants before autonomous implementation in sensitive areas, rather than treating generated code and post hoc tests as the primary review object. | Caveat: Pant explicitly calls the specification a living upstream artifact that must be validated; testing it on some inputs is only a validation aid, not proof that the intended requirement was specified completely.
- Claim: Lean's small trusted kernel makes proof results independently auditable and reduces the amount of tooling that must be trusted. | Evidence: Lean uses the same language for program definitions and proofs; tactics construct proof steps, while the kernel checks them and rejects incorrect proofs. Pant says proofs can be exported and independently checked, with open-source kernels available in C++, Rust, and Lean. | Implication: For a control plane that must justify safety decisions, retain proof artifacts and independent checking rather than trusting an agent's explanation, a verifier's opaque verdict, or a single vendor runtime.
- Claim: Formal methods can be introduced without requiring all production software to be written in Lean. | Evidence: AWS Cedar keeps its formal functional specification in Lean while production code runs in Rust; Pant also cites Verus, which verifies annotated Rust using Z3, and Aeneas, which functionally translates Rust's mid-level IR to Lean for theorem proving. | Implication: A practical adoption path is to model and check the most critical behavior around an existing Rust or systems codebase before considering direct proof-oriented implementation. | Caveat: These approaches differ materially: a Lean model plus differential testing provides strong consistency checking over sampled executions, whereas deductive verification seeks a proof of annotated properties.
- Claim: Authorization engines are a compelling early target because policy semantics can be expressed as non-negotiable safety properties. | Evidence: Cedar, AWS's open-source authorization policy language used by AWS Verified Permissions and Access, has a Lean specification and Rust production implementation. Pant says approximately 100 million differential random tests run nightly and no version ships until the implementation and model agree on those tests. | Implication: Treat policy evaluation, permission boundaries, and denial/allow invariants as priority candidates for a proof/model-based assurance layer in agent systems. | Caveat: Differential random testing, even at 100 million cases, is not itself a universal proof; it checks agreement between the production implementation and the model on generated inputs.
- Claim: AI can participate in proof construction by decomposing a target theorem into helper lemmas, proving subgoals with tactics, and assembling a kernel-checked result. | Evidence: Pant describes an Andreal AI conversion of the C compression library Zlib to Lean: from the intended property that decompress(compress(data)) returns the original data, AI generated a formal specification, Lean code, helper lemmas, and a final proof checked by the kernel. The cited proof was roughly 32,000 lines. | Implication: Use agents to lower the labor of formalization and lemma discovery, but budget for specification review, proof maintenance, and decomposition work when scoping a pilot. | Caveat: The Zlib effort reportedly took over a week and produced a large proof artifact, illustrating that formalization remains an engineering investment rather than a free byproduct of code generation.
- Claim: A language-neutral verification layer could route programs to different proof engines after lowering them into a common representation. | Evidence: Pant describes AWS's work-in-progress open-source tool called "Starter" in the transcript, with a Lean-written "Strata core" low-level intermediate representation; users would create language dialects, lower programs into that core, and dispatch them to Lean proofs, SMT solvers, or model checkers. | Implication: Do not anchor an architecture decision on this AWS project yet, but monitor common-IR approaches as a possible way to avoid committing every verified component to one source language or proof engine. | Caveat: The project is explicitly work in progress, and the transcript uses both "Starter" and "Strata core," so its current product name, scope, and readiness should be independently verified.
Detailed Brief
How the verification mechanisms differ
- Claims: Lean is presented as an interactive theorem-proving environment: users or agents apply tactics, explore branches, backtrack from failed approaches, and close a theorem when the kernel accepts the constructed proof.; SMT solvers are presented as a complementary automation engine rather than an interactive proof environment: a formula is supplied and the solver returns whether it is satisfiable or unsatisfiable.; Verus expresses obligations inline through preconditions and postconditions; these annotations are statically enforced by the verifier and erased at runtime.
- Evidence: Pant uses chess as an analogy for Lean: tactics are moves, theorem goals are checkmate, and proof search traverses a tree of possible moves.; The Lean list-reversal example proves that reversing concatenated lists produces reverse(B) concatenated with reverse(A), for all list inputs.; Verus uses Z3 and annotations represented with keywords such as requires and ensures.
- Caveats: The talk is an architectural overview rather than a hands-on implementation guide; it does not quantify proof-authoring cost, developer training requirements, CI performance, or the maintenance burden caused by changing specifications.
- Implications: Verification-engine selection should follow the type of claim: use interactive theorem proving for rich mathematical or semantic properties, and solver-backed tools for properties that fit automated constraints and contracts.; A rollout should measure not just defect prevention but proof turnaround time, verification flakiness, and the cost of updating proofs when production behavior changes.
Notable Concepts & Terms
- Specification-driven development: Correctness is defined first as an explicit artifact; implementation and proof are downstream, making the specification the central human-governed control point.
- Lean: A programming language and theorem prover used here to express both executable definitions and formal proofs, with a kernel that validates proofs.
- Small trusted kernel: The minimal checker that validates proof terms; its small scope and independent implementations support stronger trust and auditability.
- Tactics: Proof-construction operations in Lean that solve or reduce theorem goals, analogous in the talk to moves in chess.
- Differential random testing: Running a production implementation and formal model on the same generated inputs and checking that outputs agree; Cedar uses this as a release gate.
- SMT solver / Z3: An automated constraint-solving engine used by tools such as Verus to check whether formal formulas and annotated program obligations hold.
- Preconditions and postconditions: Contracts describing what must be true before and after a function executes; in Verus, they become static verification obligations rather than runtime behavior.
- Strata core / "Starter": AWS work-in-progress described as a Lean-based common intermediate representation intended to let multiple source languages access multiple verification backends.
Operator Notes / Why Ken Should Care
- Select one narrow, high-consequence invariant in Ken's systems—such as authorization deny-by-default behavior, tenant isolation, tool-call permissioning, idempotency, or money/state-transition conservation—and write a reviewable specification before assigning implementation to an agent.
- Add a release policy for that component that preserves the specification, generated proof or model-check result, verifier version, and independent checker result as build artifacts.
- For existing Rust services, evaluate a two-step pilot: first build a Lean reference model with differential testing; then assess Verus or Aeneas only if sampled equivalence does not meet the required assurance level.
- Require a separate specification-review owner from the coding-agent operator; do not let a passing proof substitute for product, security, or policy validation.
- Monitor AWS's common-IR verification project, but verify its current naming, repository status, supported languages, and production readiness before adopting it.
Source/Metadata
- Title: Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
- Transcript words: 3234
- Duration seconds: 606
- Timestamp note: No timestamps or chapters were present in the supplied transcript. The transcript contains a substantial repeated segment and trailing non-substantive repetition.
Transcript
Coding agents are generating more code than ever. Builders are generating hundreds and thousands of PRs every week. How do you know that this is correct? Using LLM as a judge for the code? Well, that's probabilistic. Tests? They only check some inputs, not all. Human code review? Doesn't scale to match agent speed. None of these can say, for all inputs, the code is correct. Formal verification can. Hi, I'm Varun Pant. I build AI products at AWS, leading teams in formal verification. Formal verification provides mathematical proof that code is correct. For all inputs, you write what correct means, which is the specification, and a formal verification tool proves that your code satisfies it. If the proof passes, it holds for every possible input. How do you use this? One way is spec-driven development, for example, with Kero. You write what the specification is, which is what correct means. Either you write it formally, for example, directly in Lean, or you write it in natural language and let the AI auto-formalize it. Now, this is really important. You then validate the specification. So either the human reviews it or you test that it holds on some inputs. And this is important because the specification is upstream. It's a living, breathing artifact that the builder interacts with. You want this to be correct. Everything else is downstream from this. The AI coding agent then goes and implements from this specification. And the formal verification tool proves that the implementation matches the specification. So humans own the specification, and machines own the code and proof. 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 means it's very extensible. And this is important. It has a small trusted kernel. Proofs can be exported and independently checked. So here's an example of a Lean file, which has both the code and proof in the same language. At the top, you'll see the code, which is a function that reverses a list in Lean. So reverse of 1, 2, and 3 gives 3, 2, and 1. And right in the middle, you'll see a theorem. This is the proof. And this theorem prover proves a property which says that reverse of A plus B is, in fact, reverse of B plus reverse of A. And this holds for every possible input. How do you do this? You have something called tactics, which do the work, which we'll get to in a second. And the kernel, remember the small trusted kernel, checks the work. A good analogy to understand the Lean proof assistant is that of chess. So in chess, your goal is to checkmate the opponent. And you make a bunch of moves. You move the knight, you move the bishop. Similarly, in Lean, you have a bunch of tactics, which are your moves. And it's the same chessboard. It's interactive. You want to prove the goal, the theorem, checkmate. And you're 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. Very similar to chess. And finally, you get a goal that hopefully proves the theorem. And then that small independent kernel confirms and checks it. The kernel catches the mistake. So here's an example at the top, where an incorrect proof is rejected immediately. And you only need to trust the small kernel. The good thing is that you can have multiple independent kernels. You yourself can actually go write one. It's completely open source. You have kernels in C++, Rust, Lean. That's a link to the ArenaLang where you can go and add a kernel. So let's look at some examples where you can put this to practice. The first one is having the specification and code both be in Lean. Now, this is open source. Andreal AI converted Zlib, which is a C compression library, to Lean. Now, granted, this happened over a week or so. But going back to our specification methodology that we mentioned, where you had specification at the top and then verification for the code, we will see the same thing here. So the natural language specification says that you decompress the output of compress, returning the original data. And then you have an AI that generates the formal spec. Now, remember, this is important. Checking the specification is key. After you do that, the AI goes and writes your code in Lean and then generates these helper lemma subgoals and proves the theorem. And at the bottom, you can see that it's verified with that small independent kernel. So what you just saw was that AI decomposed the problem into lemmas, which are subgoals. It proved each of them using tactics. Remember the chess moves that we were making? And it assembled it into final theorem, checkmate, and the kernel checked it. And this particular example had 32,000 lines of proof. So it was pretty big. Let's take another example. What if you have code in Rust? Well, you can write the functional specification of it, or the model, in Lean. An example of that is Cedar. Cedar is an open source authorization policy language, which is used by AWS Verified Permissions and Access. The specification of Cedar is written in Lean. The production code runs in Rust. Why is this important? Because let's take an example. You have 4-bit trumps permit. You want to make sure that, for any 4-bit policy being satisfied, the request is always denied. This is key. Here you can see the example of what I was talking about, which is you have the Rust production code and you have the functional specification in Lean, and you run differential random testing to check that both of those, for the same inputs, give the same output. And there's about 100 million differential random tests run nightly. No version ships until this is satisfied. Let's take another example. What if you have code in Rust and you want to deductively verify with Lean or solvers? Before we go there, let's quickly talk about this new term, solvers. Remember, we spoke of Lean being this chessboard, interactive, where you're making a bunch of moves, trying to checkmate. A solver is a calculator, a very powerful one. You feed in a formula and it returns an output, in this case, satisfiable or unsatisfiable. So an example of this is Verus, also an open source tool. It uses this solver, this very powerful calculator, Z3. And if folks are familiar with adding annotations, it's similar to that, where you can add specifications in the form of that. And the code is in line. So you see these two require and ensure keywords. That's what we call a pre- and post-condition: what must be true before and what must be true after. And this is a static check. It's enforced by the verifier and erased at runtime, almost like ghost code. Another example of this is Aeneas, which uses the mid-level intermediate representation for Rust and does a functional translation to Lean. And right after that, you use the same theorem prover, the same chessboard that we spoke of. Now, you may be asking, well, what if I have any programming language? We at AWS have been working on an open source tool called Starter. This is work in progress. But the idea is that you can have any programming language, and you yourself can create what we call a dialect. Think of this like a compiler. You have a high-level intermediate representation and you lower it down to a low-level intermediate representation, which is what Strata core is. Now, this is written in Lean. After you have all of these programs talking in the same language, which is the Strata core, you can dispatch it to any of the engines. For example, the Lean proof, remember the chessboard, or the very powerful calculator, SMT solvers, or model checkers. So, you can get started with this today. You can go to Lean in your browser with the link I pasted, and you can pick your most critical code, write what correct means, which is the specification, which is very important. And then you can let your coding agent implement it and your formal verification tool prove it. So, hopefully, in this brave new world, we have software and systems that are not probably correct, but probably correct. Thank you. That yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay You specification. So humans own the specification and machines own the code and proof. 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 means it's very extensible. And this is important. It has a small trusted kernel. Proofs can be exported and independently checked. So here's an example of a Lean file, which has both the code and proof in the same language. At the top, you'll see the code, which is a function that reverses a list in Lean. So reverse of 1, 2, and 3 gives 3, 2, and 1. And right in the middle, you'll see a theorem. This is the proof. And this theorem prover proves a property which says that reverse of A plus B is in fact reverse of B plus reverse of A. And this holds for every possible input. How do you do this? You have something called as tactics, which do the work, which we'll get to in a second. And the kernel, remember the small trusted kernel, that checks the work. A good analogy to understand the Lean proof assistant is that of chess. So in chess, your goal is to checkmate the opponent. And you make a bunch of moves. You move the knight, you move the bishop. Similarly, in Lean, you have a bunch of tactics, which are your moves. And it's the same chess board. It's interactive. You want to prove the goal, the theorem, checkmate. And 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. Very similar to chess. And finally, you get a goal that hopefully proves the theorem. And then that small independent kernel confirms and checks it. The kernel catches the mistake. So here's an example at the top, where an incorrect proof is rejected immediately. And you only need to trust the small kernel. The good thing is that you can have multiple independent kernels. You yourself can actually go write one. It's completely open source. You have kernels in C++, Rust, Lean. That's a link to the ArenaLang where you can go and add a kernel. So let's look at some examples where you can put this to practice. The first one is having the specification and code both being in Lean. Now, this is open source. Andreal AI converted Zlib, which is a C compression library to Lean. Now, granted, this happened over a week or so. But kind of going back to our specification methodology that we mentioned, where you had specification at the top and then verification for the code, we will kind of see the same thing here. So the natural language specification says that you decompress the output of compress returning the original data. And then you have an AI that generates the formal spec. Now, remember, this is important. Checking the specification is key. After you do that, the AI goes and writes your code in Lean and then generates these helper lemma subgoals and proves the theorem. And at the bottom, you can see that it's verified with that small independent kernel. So what you just saw was that AI decomposed the problem into lemmas, which are subgoals. It proved each of them using tactics. Remember the chess moves that we were making? And it assembled it into final theorem, checkmate, and the kernel checked it. And this particular example had 32,000 lines of proof. So it was pretty big. Let's take another example. What if you have code in Rust? Well, you can write the functional specification of it or the model in Lean. An example of that is Cedar. Cedar is an open source authorization policy language, which is used by AWS verified permissions and access. The specification of Cedar is written in Lean. The production code runs in Rust. Why is this important? Because let's take an example. You have 4-bit trumps permit. You want to make sure that for any 4-bit policy being satisfied, the request is always denied. This is key. Here you can see the example of what I was talking about, which is you have the Rust production code and you have the functional specification in Lean and you run differential random testing to check that both of those for the same inputs give the same output. And there's about 100 million differential random tests run nightly. No version ships until this is satisfied. Let's take another example. What if you have code in Rust and you want to deductively verify with Lean or solvers? Before we go there, let's quickly talk about this new term solvers. Remember, we spoke of Lean being this chess board interactive where you're making a bunch of moves, trying to checkmate. A solver is a calculator, a very powerful one. You feed in a formula and it returns an output. In this case, satisfiable or unsatisfiable. So an example of this is Verus, also an open source tool. It uses this solver, this very powerful calculator, Z3. And if folks are familiar with adding annotations, it's kind of similar to that, where you can add specifications in the form of that. And the code is in line. So you see these two requires and ensure keywords. That's what we call a pre and post condition. What must be true before and what must be true after. And this is a static check. It's enforced by the verifier and erased at runtime. So almost like ghost code. Another example of this is Aeneas, which uses the mid-level intermediate representation for Rust and does a functional translation to Lean. And right after that, you use the same theorem prover, the same chessboard that we spoke of. Now, you may be asking, well, what if I have any programming language? We at AWS have been working on an open source tool called Starter. This is work in progress. But the idea is that you can have any programming language and you yourself can create what we call a dialect. Think of this like a compiler. You have a high level intermediate representation and you lower it down to a low level intermediate representation, which is what Strata core is. Now, this is written in Lean. After you have all of these programs talking in the same language, which is the Strata core, you can dispatch it to any of the engines. For example, the Lean proof, remember the chessboard, or the very powerful calculator, SMT solvers or model checkers. So, you can get started with this today. You can go to Lean in your browser with the link I pasted, and you can pick your most critical code, write what correct means, which is the specification, which is very important. And then you can let your coding agent implement it and your formal verification tool prove it. So, hopefully in this brave new world, we have software and systems that are not probably correct, but probably correct. Thank you. That yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay yay You