# Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers Varun Pant, AWS | AI Engineer World's Fair 2026 | 10:07 Source: https://www.youtube.com/watch?v=lRa9sPaMyy4 Channel: AI Engineer (https://www.youtube.com/@aiDotEngineer). Summarised by AIE Talks. Page: https://aietalks.com/talks/your-code-has-bugs-lean4-has-proofs-formal-verification-for-engineers Published: 2026-08-28 Tags: agents, coding-agents, testing ## TL;DR - Formal verification can prove that code satisfies a specification for every possible input. - Humans should validate the specification, while coding agents produce the implementation and its proof. - Lean can verify code directly or check models against production code through tools such as Cedar, Verus, and Strata. ## Summary Varun Pant argues that coding agents have made ordinary software checks insufficient. Model-based grading is probabilistic, tests cover selected inputs, and human review cannot keep pace with agent-generated pull requests. Formal verification starts with a specification of what correct means, then proves that the implementation satisfies it for every input. Pant assigns humans responsibility for validating the specification and machines responsibility for writing code and proof. He explains Lean as a language for both definitions and proofs, with a small kernel that independently checks the result. Examples include an AI rewrite of zlib in Lean with 32,000 lines of proof, Cedar's Lean specification and Rust implementation, and tools that use solvers or translate other languages into a shared core. The approach still depends on getting the specification right, and Pant puts that work before implementation, testing, and proof. ## Key ideas ### Formal verification checks correctness for every input [00:01](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=1s) Pant contrasts formal verification with the checks commonly used on agent-generated code. A language model judging code gives a probabilistic answer. Tests cover only the inputs someone selected, and human review cannot match agents producing hundreds or thousands of pull requests each week. Formal verification begins with a specification that states what correct means, then proves that the implementation satisfies it. When the proof passes, Pant says the claim holds for every possible input. This changes the question from whether selected examples work to whether the code meets a defined property across its full input space. ### Humans validate the specification while machines produce code and proof [01:01](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=61s) Pant describes a workflow in which a person writes the specification directly in Lean or asks an AI to formalize a natural-language version. The specification must then be validated, either through human review or tests on some inputs. He calls it an upstream, living artifact because everything else depends on it. An AI coding agent implements the specification, and a formal verification tool proves that the implementation matches it. His division of responsibility is simple: humans own the specification, while machines own the code and proof. A flawed specification can still produce a formally verified program, so this ordering matters. ### Lean keeps program definitions and proofs in the same language [02:00](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=120s) Lean is both a programming language and a proof assistant. The same language contains the definitions and the proofs, so the workflow does not need a translation layer between them. Pant shows a list-reversal function alongside a theorem stating that reversing the concatenation of two lists equals reversing the second list and then the first. The theorem applies to every possible input. Tactics perform the proof work, while Lean's small kernel checks the resulting proof. Because Lean itself is extensible and proofs can be exported, the verification result can be checked independently. ### Tactics explore proof branches like moves in a chess game [03:01](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=181s) Pant uses chess to explain interactive theorem proving. The theorem is the checkmate goal, and tactics are the moves used to reach it. A proof can branch as different tactics are tried against different goals. If one branch cannot be closed, the process backtracks and tries another branch. Once a tactic sequence appears to prove the theorem, the small kernel checks it rather than trusting the tactic process alone. Pant shows an incorrect proof being rejected immediately. The analogy explains both the interactive nature of Lean and the distinction between generating a proof and independently checking it. ### A small kernel limits what must be trusted [03:58](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=238s) Lean proofs are checked by a small kernel, which Pant presents as the part that needs to be trusted. The kernel catches an incorrect proof, and the proof can be exported for independent checking. Pant says people can write their own kernel because Lean is open source, and he mentions implementations in C++, Rust, and Lean. He also points to Arena Lang, where another kernel can be added. Multiple independently implemented kernels provide a way to reduce dependence on one checker or one implementation of the verification system. ### An AI rewrite of zlib produced a large proof assembled from lemmas [04:52](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=292s) Pant describes an open-source effort by Andreo.AI to convert zlib, a C compression library, into Lean over about a week. The natural-language specification says that decompressing the output of compression returns the original data. After the formal specification is generated and checked, the AI writes the Lean code, creates helper lemmas as subgoals, and proves them with tactics. It then assembles those lemmas into a final theorem, which the independent kernel checks. The example produced 32,000 lines of proof. Pant uses it to show how an agent can decompose a programming task into smaller proof obligations before building the final result. ### Cedar keeps its formal model in Lean while production code runs in Rust [06:44](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=404s) Cedar is an open-source authorization policy language used by AWS Verified Permissions and Access. Its functional specification is written in Lean, while the production implementation runs in Rust. Pant gives a policy example in which a forbid policy must always deny a request when it is satisfied. AWS checks that the Rust implementation and Lean specification produce the same output for the same inputs through differential random testing. About 100 million such tests run nightly, and Pant says no version ships until the two sides agree. This combines a formal model with repeated comparisons against the shipping implementation. ### Solvers and preconditions add static checks that disappear at runtime [07:40](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=460s) Pant describes a solver as a powerful calculator that receives a formula and returns whether it is satisfiable or unsatisfiable. Verus is an open-source tool that uses the Z3 solver and lets developers annotate Rust code with specifications. Its requires and ensure declarations express preconditions and postconditions, meaning what must be true before and after the code runs. The verifier enforces these conditions statically, and the annotations are erased at runtime. Pant compares them to ghost code. He also mentions Eneus, which translates Rust's mid-level intermediate representation functionally into Lean before applying the same theorem-proving workflow. ### Strata can bring different programming languages to a shared verification core [08:37](https://www.youtube.com/watch?v=lRa9sPaMyy4&t=517s) AWS is working on Strata, an open-source tool that is still in progress. Its proposed model lets each programming language define a dialect, similar to a compiler frontend. Programs are lowered from a high-level intermediate representation into a low-level representation called Strata core, which is written in Lean. Once programs share that core language, they can be sent to different verification engines. Pant names Lean proofs, SMT solvers, and model checkers as possible destinations. The goal is to make the verification machinery reusable even when the original application code is written in another programming language. ## Notable quotes - "None of these can say for all inputs the code is correct. Formal verification can." (00:01) - "Humans own the specification and machines own the code and proof." (01:47) - "The kernel catches the mistake." (04:00) - "This particular example had 32,000 lines of proof." (05:32) - "No version ships until this is satisfied." (06:39) ## Tools & references mentioned - Lean - Kiro - Andreo.AI - zlib - Cedar - AWS Verified Permissions - AWS Access - Verus - Z3 - Eneus - Strata - Arena Lang - SMT solvers - model checkers ## Who should watch - You are using coding agents to generate more pull requests than your existing review and testing process can handle. - You need to define correctness precisely before asking an agent to implement critical code. - You are evaluating Lean, deductive verification, solver-backed checking, or a formal model paired with production code in another language. ## Editor's note From the pack [Coding agents on real codebases](https://aietalks.com/packs/coding-agents-on-real-codebases): Horthy says read the plan. Blum says fund verification before you fund adoption. Both assume you can see what the agent did. That is easy in Claude Code and much harder when you built the agent and shipped it to other people. Kitaru records those runs so you can replay one and find the step where it went wrong. It is also why this site exists. Written by the AIE Talks editors (the Kitaru team), not by the speaker.