Adam Langley, a security engineer who writes the blog Imperial Violet, spent part of July building a Zstandard decompressor in the proof language Lean and using large language models to write its formal proofs. The experiment targets a problem that kept an entire class of programming languages on the margins: proving code correct has always been too slow for most teams to bother. Langley’s results suggest that constraint may finally be loosening, at least for some kinds of proofs.
Lean is a dependently typed language, meaning its type system can encode specific facts about a value, such as an array’s exact length, not just what kind of data the value holds. A proof checker verifies those facts before the program ever runs, a form of formal verification: mathematically demonstrating that code meets a specification rather than testing it against a handful of examples. That approach is best known from seL4, a verified microkernel, and from Lean’s growing use inside mathematics research.
Langley points to the retrospective published by the seL4 team as the concrete case for why this stayed rare. Its engineers, despite years of practice, needed roughly ten times longer to prove their code correct than to design and build it, and their finished proofs ran to more than twenty times the line count of the C they were verifying. That overhead, not any missing feature, is why Lean, Coq (recently renamed Rocq), and F* remained tools for compiler researchers and mathematicians rather than working programmers.
Automating proofs is not a new ambition. F*, a related dependently typed language, leans on an SMT solver to close obligations without a person writing each step. Langley says that approach works only for simple cases; a solver can just as easily churn for hours without terminating, so users develop an instinct for what keeps it satisfied and write code around that instinct instead of around the actual problem.
For the Zstandard decoder, Langley had LLMs prove correctness properties of FSE, or finite state entropy, the table-based encoder that gives the format its compression edge over gzip. That is the kind of invariant that normally survives only as a code comment. He reports the resulting proofs type-checked with no “sorry” placeholders, Lean’s marker for a step left unproved, after roughly 20 minutes of model time and a sliver of a $20 monthly subscription’s quota. The models did need him to rewrite the table-generating code first, since an imperative shortcut he had used made the proof harder to automate.
A second experiment fared worse. Langley tried a tool called LNSym, an AArch64 chip-semantics simulator that AWS built, to prove that hand-optimized assembly matched the behavior of equivalent Lean functions, a technique already common in verified cryptography code. A small popcount example from LNSym’s own repository required more memory than his machine had. Tiny functions could be proven equivalent and then called from Lean at run time, but neither Langley nor the several LLMs he tried could push the approach further.
Langley does not claim the method generalizes. His toy decoder runs about ten times slower than the reference zstd tool on the command line, and he has not published the code, saying an LLM would likely produce a cleaner version than his own. He also warns that strong dependent types force a change in one part of a program to ripple through every type derived from it, and that proof effort may scale worse in larger codebases than current automation can keep up with. It is a genuine limit, not a caveat for show.
For teams weighing whether formally verified components belong on a 2026 roadmap, the operative question is no longer whether the proof burden is affordable. It is whether an LLM subscription can absorb it instead of a specialist engineer, and Langley’s evidence, one file format, one experiment, only starts to answer that.
Adam Langley described the experiment in a July 26, 2026 post titled “We have proof automation now” on his blog, Imperial Violet.
