← Back to feed

For forty years, formal verification of production software has been a niche discipline. The seL4 microkernel project — the canonical example — required more than 20 times as many lines of proof code as C code, and the team spent roughly 10 times more effort on proofs than on design and implementation. That overhead made formal verification economically viable only for aerospace, cryptography, and other domains where a single bug justified years of proof engineering.

Adam Langley published a post on July 26 describing what he built: a formally verified Zstandard decompressor in Lean 4, with LLMs handling most of the proof burden. His conclusion is direct: “We have proof automation now.”

What Changed

The key insight is proof irrelevance. In formal systems, once a statement is proven correct, the contents of the proof do not matter — only its existence. A human proof engineer has to structure proofs carefully so they survive code changes (what the seL4 group called “proof engineering”). LLMs do not need to. They can generate proofs that are ugly, verbose, or non-reusable, and as long as the type checker accepts them, they are mathematically valid.

This collapses the human time cost. The proof still exists. The machine still checks it. But the 10x overhead that blocked production adoption becomes an automated background task.

Langley picked Zstandard because it is winning the compression utility race as gzip’s successor — RFC 8878 standardizes it — and because it is complex enough to be a real test. zstd uses FSE (Finite State Entropy), a state machine entropy coder that Langley describes as more intricate than Huffman trees. Getting a formally verified implementation of FSE correct is not trivial.

The Practical Implication

The immediate beneficiary is security-critical software. Libraries like zstd, TLS implementations, cryptographic primitives, and protocol parsers are exactly the code where a single correctness bug causes widespread harm. They are also the code where the 10x proof overhead was most painful to justify, because the libraries themselves are not that large — the proof code would dwarf the implementation.

LLM-assisted proof automation changes the calculus. A security engineer can now write the implementation, describe the correctness properties they want to enforce, and let an LLM generate the proofs. The type checker verifies the proofs. The human reviews the properties, not the proof machinery.

Langley’s observation that LLMs can avoid blowing up the type checker (a second failure mode of automated proof systems, alongside SMT solvers that “go off into space”) matters here. Earlier attempts at proof automation through SMT solving required engineers to develop “a sixth sense for what is going to make the solver happy.” LLMs appear more robust in practice.

Context

This is a different category of AI-assisted software development than code generation. Code generation produces unverified output. Formal verification produces mathematically proven guarantees about output behavior. The combination — LLMs generating code and proofs together, checked by a type system — is a qualitatively different reliability proposition than either in isolation.

The timing lands as the industry is measuring how often AI coding agents ship insecure code. Independent audits have found that agentic coding tools produce insecure output 87% of the time even when tests pass. Formal verification is the one approach that can close that gap without relying on testing to catch what tests miss. Langley’s result suggests the tooling to apply it at production scale has arrived.

The Lean 4 ecosystem, which has seen rapid growth since the Lean Copilot and ProofNet work in 2024-2025, is the most LLM-compatible formal verification environment available. Its tactic-based proof system maps well to LLM-generated sequences of steps. The zstd verification is a production-grade demonstration that the combination works outside of academic settings.