Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Coding agents can produce hundreds or thousands of pull requests a week. Checking that output creates a different bottleneck: an LLM judge gives a probabilistic assessment, tests exercise selected inputs, and human review struggles to keep pace. Varun Pant, who builds AI products and leads formal-verification teams at AWS, introduces formal verification as a way to prove that an implementation satisfies a specified property across every input covered by that property. 0:12

The first engineering task is to write what “correct” means. In the spec-driven workflow Pant introduces with Kiro, a human can write a formal specification directly in Lean or write natural-language requirements that an AI formalizes. The specification then needs validation: someone reviews it, or tests whether it describes the expected behavior on concrete inputs. A proof establishes agreement with the specification; a mistaken specification can therefore produce a proved implementation of the wrong requirement.

That order matters because the specification sits upstream of both implementation and verification. It remains a “living, breathing artifact” that the builder works with as requirements develop. Once its meaning is settled, the coding agent implements it and the verification tool proves the implementation matches it. Pant’s division of labor is compact: “humans own the specification, and machines own the code and proof.”

Lean is both a programming language and a proof assistant. Definitions and proofs use the same language, so a Lean implementation does not need a separate translation into a proof language. Pant also emphasizes extensibility—Lean is implemented in Lean—and a small trusted kernel that checks proofs. Proofs can be exported for independent checking.

List reversal supplies the first concrete example. Reversing [1, 2, 3] produces [3, 2, 1]. The accompanying theorem describes how reversal interacts with concatenation: reversing A followed by B gives the reverse of B followed by the reverse of A. Here, the talk’s “plus” means joining lists, rather than adding their elements.

To see the change, split that same list into A = [1, 2] and B = [3]. Concatenation places the A block before the B block. Reversing the combined list moves the B block to the front and reverses the order inside A, yielding [3, 2, 1]. Reversing the blocks separately and joining them in the opposite order produces the same result: [3] ++ [2, 1]. This instance makes the property visible; the theorem expresses it for every pair of lists, rather than only these three elements.

Tactics construct the proof, and the kernel checks it. This separation provides a way to accept machine-generated proofs: the machine searches for an argument, while a much smaller component checks whether that argument establishes the theorem.

Pant’s analogy is chess. The theorem is the goal, like checkmate; tactics are the moves used to reach it. Proof construction is interactive and branches into a search tree. A tactic may advance the proof, but a branch can also leave a goal unresolved. The prover then backtracks and tries another route. A plausible sequence of moves alone does not finish the job: the resulting proof must pass the kernel.

The kernel rejects an incorrect proof in Pant’s example. Confidence in the generator therefore does not substitute for checking its output. Pant describes open-source kernel implementations in C++, Rust, and Lean, and the possibility of writing an independent checker yourself. The trusted component remains the checker, even when proof search becomes large or complicated. 4:03

The next example puts both specification and implementation in Lean. Pant describes an open-source project in which AI converted zlib, the C compression library, to Lean over about a week. Its natural-language requirement is easy to understand: decompressing compressed data should return the original data. Written as an intended property, the round trip is decompress(compress(data)) = data. The Lean theorem in Leo de Moura’s separate May 6, 2026 NFM presentation proves that round trip across compression levels for inputs satisfying data.size < 1024 * 1024 * 1024: strictly below 1 GiB. The proved claim therefore includes an input-size precondition that the plain-language requirement leaves unstated. 4:41

The AI first turns that requirement into a formal specification. After the specification is checked, it writes the Lean code and breaks the proof into helper lemmas—smaller claims that serve as subgoals. Tactics prove those claims, the claims assemble into the final theorem, and the independent kernel checks the result. Pant reports 32,000 lines of proof for this example. That quantity describes the proof artifact, rather than a count of test cases.

How does one readable requirement lead to such a large proof? The flow below separates the initial decision about meaning from the generated implementation and proof. Specification validation comes first. The AI then expands the problem into code and lemmas, and the kernel checks the assembled argument. The checker’s position at the end explains why validating the requirement cannot be delegated to proof checking.

Production code can stay in Rust while Lean supplies its functional specification. Cedar, an open-source authorization policy language, illustrates this arrangement: its specification is written in Lean and its production implementation runs in Rust. The critical example is “forbid trumps permit.” Whenever a forbid policy is satisfied, the request must be denied, even when permission would otherwise be available. 5:58

The connection between the two implementations uses differential random testing. Each generated input goes to both the Rust production code and the Lean model, and their outputs are compared. Pant reports about 100 million such tests nightly and says no version ships until the agreement requirement is satisfied. This checks the Rust implementation against the formal model on sampled inputs; it does not establish a deductive proof that the Rust code agrees with the model for every input.

The practical choice is to keep a shipping implementation in Rust and use a Lean model as the reference for its behavior. For the forbid example, agreement means both paths return denial for the same request and policies. A difference exposes a disagreement that must be resolved before release. The model gives testing a precise expected result, rather than requiring each test author to invent one.

Deductive verification offers another way to work with Rust. Before introducing the tools, Pant distinguishes a solver from Lean’s interactive proof search. Lean resembles a chessboard on which tactics advance a goal. A solver resembles a powerful calculator: it receives a formula and answers whether that formula is satisfiable or unsatisfiable—whether its constraints can hold together. 6:59

• Verus: specifications alongside code. Verus uses Z3 to verify Rust code with annotations expressing preconditions and postconditions. A precondition states what must hold before the operation; a postcondition states what must hold afterward. These specifications are checked statically by the verifier and erased at runtime, so they do not become runtime assertions.

• Aeneas: translate Rust into Lean. Aeneas starts from Rust’s mid-level intermediate representation and translates it into a functional form in Lean. The translated program can then use the theorem-proving approach introduced earlier: goals, tactics, and checked proofs.

These paths place the specification in different working environments. Verus keeps it close to the Rust code and uses a solver; Aeneas brings a functional translation into Lean for theorem proving. Both differ from Cedar’s differential-testing arrangement, where the production program and model are run on matching inputs and their outputs compared.

The final technical proposal extends the compiler idea beyond Rust. Pant describes Strata, an open-source AWS tool. A language-specific dialect represents a program at a high level, then lowers it into Strata Core, a common low-level representation written in Lean. The intended architecture lets that representation feed different verification engines: Lean proofs, SMT solvers, or model checkers. The architecture documentation describes the implemented analysis as a verification-condition generator with an SMT interface; broader Lean reasoning and other engine integrations remain architectural goals. Support for arbitrary languages is likewise the intention of this work in progress, rather than a claim that every language is already supported. 8:26

What does a shared core buy? The diagram shows where language-specific work ends and analysis begins, distinguishing the implemented SMT route from proposed engine choices. Each language needs a dialect and lowering path, but the resulting program reaches the same core. That common representation allows an analysis to be reused across languages, with additional engines intended to extend the choice of verification method.

The closing recommendation starts smaller than that infrastructure: pick your most critical code and write what correct means. Pant points to using Lean in a browser, then having a coding agent implement the specification and a verification tool prove the result. A useful first target is a property whose meaning you can inspect and care about—a compression round trip or a denial rule—before asking a machine to expand it into a proof. That is the route toward the ending’s ambition of software that is “provably correct.” 9:17