--- schema: 1 type: video title: >- 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 --- Watch along with the corrected transcript, summary, timestamps and resources on this talk's official AIE page: https://ai.engineer/talks/lRa9sPaMyy4-youtube-a4fdf8b98776965fc286 Join our upcoming AI Engineer conferences (see https://ai.engineer landing page): - AIEi Shanghai, November 5–6 — the first for meeting top Chinese labs and engineers - AIE CODE in SF, November 10–12 — the top AI Coding conference returns - AIEi Sydney, December 7–8 — the first AIEi run alongside NeurIPS 2026 in Sydney --- canonical: 'https://liquidgold.cc/watch/lRa9sPaMyy4' markdown: 'https://liquidgold.cc/watch/lRa9sPaMyy4.md' llms: 'https://liquidgold.cc/watch/lRa9sPaMyy4/llms.txt' parent: 'https://liquidgold.cc/channel/aidotengineer.md' channel: aidotengineer updated: '2026-10-24T04:23:03.005Z' language: null children: [] videoId: lRa9sPaMyy4 durationSeconds: 607 publishedAt: '2026-08-28T18:00:17.000Z' searchChunks: - ordinal: 0 text: null startSeconds: 12 endSeconds: 24 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=12' heldReason: rights - ordinal: 1 text: null startSeconds: 24 endSeconds: 68 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=24' heldReason: rights - ordinal: 2 text: null startSeconds: 24 endSeconds: 68 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=24' heldReason: rights - ordinal: 3 text: null startSeconds: 79 endSeconds: 124 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=79' heldReason: rights - ordinal: 4 text: null startSeconds: 79 endSeconds: 124 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=79' heldReason: rights - ordinal: 5 text: null startSeconds: 124 endSeconds: 136 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=124' heldReason: rights - ordinal: 6 text: null startSeconds: 136 endSeconds: 191 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=136' heldReason: rights - ordinal: 7 text: null startSeconds: 202 endSeconds: 247 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=202' heldReason: rights - ordinal: 8 text: null startSeconds: 247 endSeconds: 259 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=247' heldReason: rights - ordinal: 9 text: null startSeconds: 259 endSeconds: 292 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=259' heldReason: rights - ordinal: 10 text: null startSeconds: 302 endSeconds: 414 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=302' heldReason: rights - ordinal: 11 text: null startSeconds: 302 endSeconds: 414 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=302' heldReason: rights - ordinal: 12 text: null startSeconds: 427 endSeconds: 462 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=427' heldReason: rights - ordinal: 13 text: null startSeconds: 462 endSeconds: 474 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=462' heldReason: rights - ordinal: 14 text: null startSeconds: 474 endSeconds: 520 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=474' heldReason: rights - ordinal: 15 text: null startSeconds: 520 endSeconds: 531 watch: 'https://liquidgold.cc/watch/lRa9sPaMyy4?t=520' heldReason: rights --- # Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS 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 --- Watch along with the corrected transcript, summary, timestamps and resources on this talk's official AIE page: https://ai.engineer/talks/lRa9sPaMyy4-youtube-a4fdf8b98776965fc286 Join our upcoming AI Engineer conferences (see https://ai.engineer landing page): - AIEi Shanghai, November 5–6 — the first for meeting top Chinese labs and engineers - AIE CODE in SF, November 10–12 — the top AI Coding conference returns - AIEi Sydney, December 7–8 — the first AIEi run alongside NeurIPS 2026 in Sydney --- Canonical: https://liquidgold.cc/watch/lRa9sPaMyy4 · Channel: [AI Engineer](https://liquidgold.cc/channel/aidotengineer.md) > Search chunk text is held until public-source provenance is verified. ## Document chunks --- #### Chunk 0: Document excerpt (0:12 to 1:19) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 1: Document excerpt (1:19 to 2:16) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 2: Document excerpt (2:16 to 3:22) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 3: Document excerpt (3:22 to 4:19) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 4: Document excerpt (4:19 to 5:02) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 5: Document excerpt (5:02 to 7:07) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 6: Document excerpt (7:07 to 8:40) > Held: transcript rights do not permit this chunk's text. --- #### Chunk 7: Document excerpt (8:40 to 10:07) > Held: transcript rights do not permit this chunk's text.