LLMs Automate Formal Proofs in Lean: Zstd Decompressor Case Study
Original: We have proof automation now
Why This Matters
LLM-driven proof automation could unlock formal verification for mainstream software engineering workflows.
Engineer Adam Langley built a Zstandard decompressor in Lean 4 to test whether LLMs can automate formal proof generation. Results suggest LLMs may dramatically reduce the historically prohibitive proof-writing overhead that has made dependently-typed languages impractical.
Adam Langley (imperialviolet.org) published findings from an experiment building a Zstandard decompressor in Lean 4, using LLMs to automate formal proof obligations. Dependently-typed languages like Lean and Rocq (formerly Coq) allow encoding of arbitrarily precise invariants verified by the type system, but have historically required enormous proof effort—the seL4 project famously spent roughly 10x more time on proofs than on design and implementation, with over 20x more lines of proof code than C code.
Previous automation attempts such as F* used SMT solvers, which work for simple cases but can run indefinitely on complex inputs, requiring developers to develop an intuitive sense for what the solver will accept.
Langley argues that a key theoretical property—proof irrelevance, meaning only a proof's existence matters, not its content—makes LLMs an ideal fit for proof automation. His experiments indicate LLMs can generate valid proofs without triggering type-checker memory blowups, a known failure mode for complex proofs. He concludes that LLMs could make dependent type systems significantly more practical for real-world software development, reducing the "proof engineering" burden that has kept the paradigm niche.