← back
Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
Takeaway
Use carefully reviewed specifications and machine-checked proofs for critical properties, while distinguishing proved models from implementations tested against them.
Summary
- Formal verification proves implementation properties relative to a specification, making human validation of that specification the critical upstream responsibility.
- Lean combines code, theorems, and tactics in one language, with proofs checked by a small trusted kernel; the talk cites an AI-built zlib port with about 32,000 lines of proof.
- Cedar pairs a Lean specification with Rust production code and approximately 100 million nightly differential tests, which check agreement on sampled inputs rather than proving the Rust implementation equivalent.
- Verus uses Z3 to verify annotated Rust, Aeneas translates Rust representations into Lean, and AWS's work-in-progress Strata aims to route language-specific dialects through a shared verification representation.
lean4formal-verificationspecifications
Original 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_ / 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