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

Coding agents increase the amount of code engineers must assess. Varun Pant, who builds AI products and leads teams in formal verification at AWS, opens with builders generating hundreds and thousands of pull requests each week. A language model judging that code gives a probabilistic assessment. Tests check selected inputs. Human review struggles to match agent throughput. These checks do not establish that an implementation behaves correctly for every possible input.

Formal verification changes the question into a mathematical claim. First, write a specification that defines what correct means. Then prove that the implementation satisfies it. The resulting guarantee concerns the property expressed by that specification across its input domain. The specification is therefore part of the claim: proving that code satisfies a stated requirement does not independently establish that the requirement captures everything its users need.

Pant describes a development workflow centered on the specification, mentioning Kiro as an example. Engineers can write the specification formally, directly in Lean, or express it in natural language and ask an AI to formalize it. Either route produces the artifact that defines what the implementation must do.

The next step is to validate that artifact before building downstream from it. Pant proposes human review or checking that the specification holds on some inputs. Those checks help assess whether the specification expresses the intended behavior. This is why he calls it a living artifact that the builder interacts with: an error here can direct the entire implementation toward the wrong objective.

Once that definition is validated, the coding agent implements it and the verification tool proves that the implementation matches it. Pant assigns responsibility accordingly: humans own the specification; machines own the code and proof. Automation takes on implementation and proof construction while people remain responsible for deciding what behavior should count as correct.

Lean is both a programming language and a proof assistant. Its definitions and proofs use the same language, so this arrangement needs no separate translation layer between the program and its proof. Pant also emphasizes extensibility through Lean’s implementation in Lean, alongside a small trusted kernel. Proofs can be exported and checked independently.

His example is a function that reverses a list: reversing [1, 2, 3] produces [3, 2, 1]. The accompanying theorem states a general relationship: reversing the concatenation of lists A and B gives the reverse of B followed by the reverse of A. Written illustratively, reverse(A ++ B) = reverse(B) ++ reverse(A), where ++ means list concatenation. The concrete list demonstrates the function; the theorem establishes the stated relationship for every pair of lists in its domain.

Two mechanisms divide the work. Tactics help construct the proof, and the kernel checks the result. This distinction separates finding a way to establish a theorem from deciding whether the proposed proof actually establishes it.

Pant uses chess to explain interactive proof construction. The theorem is the goal, analogous to checkmate, and tactics are the moves available to reach it. Trying tactics takes the prover through a tree of possibilities. If one branch leaves a goal that cannot be proved through that approach, the prover can backtrack and try another branch. The analogy captures why proof construction involves exploration rather than a single predetermined sequence.

A successful search still ends with a separate check by the small kernel. Pant describes an incorrect proof being rejected immediately: a proof-producing process cannot make its answer valid simply by presenting it confidently. Trust is concentrated in the checker. He points to independent kernel implementations in C++, Rust, and Lean, and notes that the open-source design allows someone to write another checker themselves.

The first larger example keeps both specification and implementation in Lean. Pant reports that an AI converted zlib, a C compression library, to Lean over roughly a week. The requirement he presents is a round trip: decompressing the output of compression must return the original data. Illustratively, decompress(compress(data)) = data. That is the specific property at the center of this example; the presentation does not establish the scope of every other property of the converted library.

The workflow begins with that natural-language requirement, which an AI turns into a formal specification. Pant again stresses checking the specification before proceeding. The AI then writes the Lean implementation and generates helper lemmas: smaller claims that break the overall proof into manageable subgoals.

Each lemma is proved using tactics, and those results are assembled into the final theorem. The independent kernel checks the completed proof. Pant reports 32,000 lines of proof for this example, illustrating how a compact requirement can require a substantial body of supporting reasoning. The reported achievement is the construction and checking of that proof; its size alone does not tell us how broad the specification is.

A second arrangement keeps production code in Rust and expresses its functional specification, or model, in Lean. Pant uses Cedar, an open-source authorization policy language, as the example. Its specification is written in Lean while its production implementation runs in Rust. The security property he highlights is that forbid takes precedence over permit: if any forbid policy is satisfied, the request must be denied.

Differential random testing connects these two implementations of the behavior. The same inputs are passed to the Rust production code and the Lean functional specification, and their outputs are compared. Pant says approximately 100 million such tests run nightly, with agreement required before a version ships. This allows the team to retain Rust in production while checking it against the Lean model. The connection described here is still testing over sampled inputs, so it does not constitute a proof that Rust and Lean agree for all inputs.

Pant next considers deductive verification of Rust using Lean or solvers. He distinguishes the interactive chessboard of Lean from a solver, which he compares to a powerful calculator: feed it a formula and it returns a satisfiable or unsatisfiable result. This introduces another way to handle verification obligations, with the solver performing the formula-solving work.

Verus is his concrete example of an open-source tool using the Z3 solver. Specifications appear alongside the code as preconditions and postconditions. A precondition states what must be true before the operation; a postcondition states what must be true afterward. This makes the assumptions part of the contract: the promised outcome is tied to the conditions under which the operation is verified.

These checks happen statically. The verifier enforces the specifications, and the specification code is erased at runtime—what Pant likens to ghost code. Its purpose is to support verification before execution rather than to remain as an executing runtime check.

He also describes a translation-based route from Rust to Lean. It takes Rust’s mid-level intermediate representation and produces a functional translation in Lean. Once that translation exists, the same Lean theorem prover can be used to reason about it. The mechanism provides a path into Lean’s proof environment, although the talk does not detail which Rust constructs the translation supports.

The final architectural question is how to extend verification to other programming languages. Pant introduces Strata, an open-source tool under development at AWS. Its intended design lets developers create a language-specific dialect and lower a high-level intermediate representation into Strata core, a lower-level intermediate representation written in Lean. The compiler analogy explains the role of this step: different source languages converge on a common representation.

Once programs are represented in Strata core, they can be dispatched to different verification engines: Lean proofs, SMT solvers, or model checkers. This design separates the work of representing a source language from the choice of verification engine. Pant explicitly describes Strata as work in progress, so support for arbitrary languages is the architectural ambition rather than a demonstrated claim of universal coverage.

Pant closes with a bounded starting point: try Lean in the browser, choose the most critical code, and write down what correct means. Then let a coding agent implement that specification and a formal verification tool prove it. The practical sequence begins with deciding which behavior matters enough to specify precisely; implementation and proof follow from that decision.