⏱️ Lectura: 13 min
The team behind seL4, the formally verified microkernel, documented something brutal in their retrospective: writing the formal proofs took them about 10 times longer than designing and implementing the system, and they ended up with more than 20 lines of proof for every line of C. That cost explains why dependently typed languages like Lean or Coq (recently renamed Rocq) remained reserved for projects with nearly unlimited budgets.
📑 En este artículo
An engineer who works on cryptography at Google and writes the ImperialViolet blog decided to test whether language models bring that cost down. He built, end to end, a Zstandard decompressor in Lean, with the proofs generated by an LLM instead of by hand.
TL;DR
- The seL4 project documented that formally verifying it took 10 times longer than designing and coding it.
- seL4’s proof code ended up more than 20 times longer than its C code.
- An ImperialViolet engineer implemented a complete Zstandard decompressor in Lean with proofs generated by an LLM.
- Zstandard, created by Yann Collet, uses Jarek Duda’s ANS entropy coding instead of gzip’s Huffman coding.
- F* delegates proofs to an SMT solver that sometimes takes hours without converging on complex cases.
- Proof irrelevance means that once a theorem type-checks, the content of the proof stops mattering.
- Coq changed its name to Rocq, a detail mentioned in passing in the original post about the experiment.
- Zstandard has its formal specification in RFC 8878, used as the reference for building the decoder.
What happened
The ImperialViolet author published the experiment on July 26, 2026: he implemented a complete decoder for the Zstandard (zstd) format in Lean, delegating the generation of formal proofs to an LLM. The goal wasn’t just to have a working decoder, but for Lean’s type checker to mathematically certify that certain properties of the code, for example that it never reads outside a buffer’s bounds, always hold, without relying on tests.
The choice of Zstandard isn’t arbitrary. It’s the compressor created by Yann Collet that relies on ANS (Asymmetric Numeral Systems) entropy coding, developed by Jarek Duda, and it has been displacing gzip as the de facto standard in Linux distributions, container formats, and network protocols. It has a specification in RFC 8878, dense but complete, which the author used as a line-by-line reference to write the decoder.
Context and history: the old problem with dependent types
Dependently typed languages let you express invariants in the type system itself: not just “this function takes an array”, but “this function takes an array of exactly N elements where N is even”. In theory, that turns errors discovered today in production into compile-time errors. In practice, writing those proofs by hand is extremely expensive.
The reference case is seL4, the microkernel formally verified in Isabelle/HOL. Its retrospective gets cited over and over in the community because it quantifies the problem: despite the team having built up considerable expertise, they spent about 10 times more time proving than designing and implementing, and ended up with more than 20 times more lines of proof than lines of C. That ratio is what makes applying formal verification to most software impractical.
F* emerged to bring that cost down, a language that delegates a large part of the burden to an SMT (Satisfiability Modulo Theories) solver, which tries to automatically prove each obligation. It works well for simple cases, but it’s easy to write a proof that makes the solver hang for hours without converging. Anyone who uses F* regularly ends up developing intuition about which formulations the solver “likes”, a form of technical superstition rather than predictable engineering.
⚠️ Heads up: delegating proofs to an SMT solver doesn’t eliminate the cost, it shifts it. Instead of writing the proof by hand, you have to learn how to formulate the problem in a way the solver can resolve in reasonable time, and that isn’t always cheaper.
There’s a technical detail that makes combining this with LLMs promising: proof irrelevance. Once a statement is proven correct, the specific content of that proof stops mattering: only its existence does. This isn’t absolute, there are two caveats. First, what the seL4 team called “proof engineering”: structuring proofs so that, when the code changes, they don’t need to be rebuilt from scratch. Second, a sufficiently tangled proof can make the type checker itself consume enormous amounts of memory and time, even if it’s correct.
Why Zstandard is a good testbed
Zstandard, like gzip and bzip2, is a compressor from the LZ77 family: it replaces repeated sequences with references to earlier occurrences. The difference lies in the entropy coding used after that stage. Gzip uses Huffman coding; Zstandard uses ANS, which achieves tighter compression at the cost of a more intricate design. That added complexity is precisely what makes it interesting to try to formally verify: there’s more surface area where a mismatch between the specification and the implementation can hide a bug.
The author himself measured, over 64 MiB of the Lean/mathlib source code, the tradeoff between space saved and decompression speed for the four most common compressors. The table summarizes the qualitative differences he documented:
| Compressor | Algorithm family | Strength | Limitation |
|---|---|---|---|
| zstd | LZ77 + ANS | Very fast decompression while maintaining a good compression ratio | Doesn’t reach lzma’s maximum ratio on large corpora |
| gzip | LZ77 + Huffman (DEFLATE) | Ubiquitous, with highly optimized implementations (for example, Apple’s) | Worse compression ratio than zstd or lzma |
| bzip2 | Burrows-Wheeler Transform | Good ratio on highly repetitive text | Noticeably slower decompression than zstd |
| lzma (XZ/LZMA2) | LZ77 + range modeling | The best compression in the group | The slowest to decompress |
The author himself notes that his measurements come from the machine he was using at the time (a Mac), and that on that platform gzip is especially optimized, so the absolute numbers aren’t comparable across different setups. What’s reproducible is the order of magnitude: on a logarithmic scale, zstd and gzip sit in their own speed category compared to bzip2 and lzma.
Formal proofs with LLM help: how the cycle works
The mechanics are simpler than they sound. You write the theorem statement in Lean, for example “the buffer’s read index never exceeds its size”. An LLM proposes a tactic script that, in theory, proves that statement. Lean’s type checker evaluates it: if it compiles, the proof is accepted forever, no matter how clumsy or long it is. If it fails, the error is sent back to the model along with the compiler’s exact message, and the cycle repeats.
flowchart TD
A["Theorem statement in Lean"] --> B["The LLM proposes a tactic script"]
B --> C["Lean's type checker evaluates the proof"]
C -->|"Type error"| D["The LLM receives the error message"]
D --> B
C -->|"Compiles"| E["Proof accepted: the content no longer matters"]This cycle works thanks to the proof irrelevance mentioned earlier: the proof doesn’t need to be elegant or short, only existent. It’s the same reason a human can write an ugly proof and the compiler accepts it just the same. The difference from F* is that here there’s no generic solver trying to guess the strategy: the LLM already knows idiomatic Lean patterns (induction, simp, case analysis) because it saw them during training, and applies them more purposefully than a blind search.
A minimal example, the kind anyone can try right after installing Lean, illustrates the syntax:
theorem add_comm (a b : Nat) : a + b = b + a := by
induction a with
| zero => simp
| succ n ih => simp [Nat.succ_add, ih]
That theorem is trivial, but the pattern scales. In a compression decoder, the kind of invariant that matters is different: that a read pointer never goes outside the buffer. In Lean this can be modeled with Fin, a type that represents “a natural number less than N” directly in its definition:
structure DecompressionWindow where
data : Array UInt8
pos : Fin data.size
def nextByte (v : DecompressionWindow) : UInt8 :=
v.data.get v.pos
With pos : Fin data.size, it’s impossible to construct a DecompressionWindow with an out-of-range pointer: the type itself forbids it. nextByte doesn’t need any runtime check and can’t fail from an invalid access, because the compiler already ruled out that possibility before generating the binary. That’s exactly the kind of error, an out-of-bounds read in a compression decoder, that produced real vulnerabilities in libraries like zlib over the years.
💡 Tip: proof irrelevance is what makes it viable to delegate the proof to an LLM. Since the content of the proof doesn’t affect the final binary, it doesn’t matter if the model takes 40 attempts to find the right script: only the outcome matters.
Getting started: installing Lean and compiling your first proof
Lean 4 is installed with elan, its version manager (the equivalent of what rustup is for Rust). The commands vary by operating system:
# macOS / Linux
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Windows (PowerShell)
irm https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | iex
With elan installed, you create a new project with Lake, Lean’s build manager, and compile it:
lake new my_proof math
cd my_proof
lake build
lake env lean --version
If lake env lean --version returns a version number with no errors, the environment is working. From there, pasting the add_comm example above into a .lean file and running lake build is the fastest way to confirm that the type checker actually rejects incorrect proofs: just delete a line from the tactic script to see the error.
To experiment with LLMs integrated into the proof workflow without writing the infrastructure from scratch, two open source projects serve as a starting point: LeanDojo, which exposes Lean’s proof state as an environment a model can query, and LeanCopilot, which integrates model-generated tactic suggestions directly into the editor.
Impact and analysis
The concrete result, a working Zstandard decoder that Lean certified against certain properties, matters less than the question it answers: if proof irrelevance makes it indifferent how ugly a proof is, then the cost human engineers used to pay (writing and debugging each proof) is exactly the kind of repetitive task, with immediate compiler feedback, that an LLM can iterate on thousands of times without fatigue.
That doesn’t resolve the two caveats that already complicated proof irrelevance before LLMs existed. Proof engineering, structuring proofs so they survive code changes, remains a design problem: an LLM can regenerate the entire proof every time the code changes, but that can become costly as the project grows. And a proof that blows up the type checker’s memory usage is still a problem, no matter who generated it.
There’s also a risk of replacing one kind of mysticism with another. With F*, the community developed intuition about which formulations the SMT solver could resolve. With LLMs generating proofs in Lean there’s a similar risk: the process might work better with certain statement styles and worse with others, without it being clear why, simply because it matches patterns seen during the model’s training.
What’s next
The ImperialViolet author himself frames this as a proof of concept, not as a product ready for use in production compression libraries. The logical next step is to replicate the experiment on code with a real history of vulnerabilities, such as binary format parsers or network protocol implementations, to measure whether the approach scales beyond a decoder written to test the idea.
The bottleneck that remains isn’t generating the proof once, but keeping it alive as the code changes week to week. If an LLM can regenerate the complete proof at a low marginal cost every time there’s a commit, the proof engineering that cost seL4 so much time could stop being an exclusively human problem. That’s the implicit bet behind the experiment.
📖 Summary on Telegram: View summary
Try it yourself: install elan with the command above, paste the add_comm theorem into a .lean file, and run lake build to see Lean’s type checker in action in under five minutes.
Frequently Asked Questions
What is a dependently typed language?
It’s a language where types can depend on values, not just on other types. This allows expressing invariants like “an array of exactly N elements” or “an index always less than the buffer’s size” directly in a function’s signature, with the compiler verifying them.
Why did Coq change its name to Rocq?
The name generated confusion and recurring jokes in an English-speaking context. The project adopted Rocq as its new name, though the language’s technical foundation remains the same.
What does “proof irrelevance” mean?
It’s the property by which, once a theorem type-checks correctly, the specific content of that proof stops being relevant to the program: only the fact that the proof exists and is valid matters, not how it’s written.
Why did seL4 take so long to formally verify?
Because writing manual proofs for each property of the microkernel turned out to be far more laborious than writing the original code: the team reported spending about 10 times more time proving than designing and implementing, with more than 20 times more lines of proof than lines of C.
Can this approach already be used in production?
Not as a packaged solution. ImperialViolet’s experiment is a proof of concept around a Zstandard decoder, not a ready-made library to replace existing implementations in critical systems.
How does it differ from F*?
F* delegates proofs to a generic SMT solver, which can hang searching for a proof with no guarantee of finding it in time. The LLM-based approach in Lean uses a model trained on the language’s idiomatic patterns, which iterates on the type checker’s errors instead of depending on a general-purpose solver.
References
- ImperialViolet, “We have proof automation now”: the original post documenting the Zstandard-in-Lean experiment.
- RFC 8878: the official specification for the Zstandard compression format.
- sel4.systems: official site for the seL4 microkernel and its formal verification retrospective.
- leanprover.github.io: official documentation for the Lean 4 language.
- github.com/lean-dojo/LeanDojo: open source environment for connecting LLMs to Lean’s theorem prover.
📱 Enjoying this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day. @programacion
Imagen destacada: Foto de Brett Jordan en Unsplash
0 Comments