Your Code Has Bugs. Lean 4 Has Proofs. A Practical Guide to Formal Verification for Engineers

We've spent decades testing code and still ship bugs. Formal verification — mathematically proving your code is correct — has always been the answer nobody could use. Too academic. Too slow. Too hard. That's changed. Lean 4 is a theorem prover that's also a real programming language — with a package manager, an LSP, a REPL, and a growing ecosystem. It's what the Mathlib community uses to formalize mathematics, and it's quietly becoming practical for verifying real software. In this talk, I'll show you how formal code verification works — no PhD required: - Lean 4 as a programming language: it compiles, it has types, it has IO — you can write real programs, not just proofs - Three proof strategies: decide for exhaustive finite-domain checks (one line, kernel-verified), omega for linear arithmetic bounds, and simp for rewriting — these aren't research techniques, they're tactics you'll use daily - Live demo using claude code. - When to verify vs. test: a practical framework for picking which code paths deserve a proof (hint: the ones where a bug is a security incident, a compliance violation, or a lost customer)