We Have Proof Automation Now

Adam Langley built a Zstandard decompressor in Lean to test a specific claim: that LLMs have removed the thing that kept dependently-typed languages out of ordinary software. His conclusion is narrow and supported. Proofs of nontrivial universal properties about real decoder code are now cheap. Verified assembly, the other thing he tried, is not.

The cost that made dependent types niche

The promise of a dependent type system is that invariants which normally survive as comments — and stop being true as the team grows — can be written formally and checked by a machine. The price has always been proof effort. Langley's reference point is the seL4 retrospective: the team spent roughly ten times as long proving as they did designing and implementing, and ended with more than twenty times as many lines of proof as lines of C. He adds the failure mode that does not show up in ratios, which is spending hours on a proof and discovering the goal was false.

The established escape hatch is automation by SMT solver, as in F*. It works on easy obligations and then stops working in a way that is hard to reason about: it is easy to write something that sends the solver off for hours with no way to tell whether it will ever return. People who use these systems daily develop a feel for what keeps the solver happy and shape their code around it. Langley's verdict on that is the best line in the post — it "converts the problem into mysticism: you end up serving a complex and fickle god."

What makes LLMs a different kind of automation is proof irrelevance. Once a statement is correct, only the existence of a proof matters, not its contents. Two things complicate that in practice. The seL4 group's "proof engineering" is the work of structuring proofs so they can be repaired cheaply after the code changes, and sufficiently complicated proofs can blow up the type checker's memory. If a machine regenerates proofs on demand, the first problem mostly stops being a problem. The second does not, though Langley found LLMs avoided it in his tests.

What got proved

The concrete result is about FSE table construction. Langley implemented the algorithm from RFC 8878, put the RFC's three test vectors into unit tests, and then stated a theorem about all inputs:

theorem ofDistribution_wellFormed (h : ofDistribution accuracyLog probs = some t) :
    t.entries.size = 2 ^ accuracyLog ∧
    (∀ s : Fin probs.size,
      t.entries.toList.countP (fun e => e.symbol == s.val) = probCells probs[s]) ∧
    (∀ (i : Nat) (hi : i < t.entries.size) (v : Nat), v < 2 ^ (t.entries[i]'hi).nbBits →
      (t.entries[i]'hi).baseline + v < 2 ^ accuracyLog) ∧
    (∀ (s : Fin probs.size), 0 < probCells probs[s] → ∀ x < 2 ^ accuracyLog,
      ∃! i : Nat, ∃ hi : i < t.entries.size,
        (t.entries[i]'hi).symbol = s.val ∧ (t.entries[i]'hi).baseline ≤ x ∧
          x < (t.entries[i]'hi).baseline + 2 ^ (t.entries[i]'hi).nbBits) := …

In words: if the constructor produces a table at all, then the table has the right size for the accuracy parameter; each symbol gets exactly as many states as its probability calls for; reading nbBits bits and adding the baseline always lands on a valid state number; and for every symbol with nonzero probability and every target state, exactly one state of that symbol reaches it. Those four facts are precisely the assumptions an optimised decoding inner loop relies on and that no mainstream type system can express.

Several LLMs produced that proof automatically in about twenty minutes, using a fraction of a $20/month subscription quota. Langley confirmed it type-checks with no sorrys. One caveat he is explicit about: the models needed the table-generating code changed first, because he had used too much Id.run to drop into imperative style, and that is harder for the proof machinery to work with. Lean's mvcgen work is aimed at that gap.

The smaller example in the post is the same idea at everyday scale. A block of type rle has a content size of one byte, so indexing blockBytes.val[0] is safe — and in Lean you discharge that at the index site rather than trusting it:

let b := blockBytes.val[0]'(by
  rw [blockBytes.property, blockHeader.contentSize_rle hty]; omega)

blockBytes.property comes from readExact's return type, IO {ba : ByteArray // ba.size = n}, which carries the length as part of the type. C gives undefined behavior here, and a modern language gives you a runtime throw or an option; Lean gives a third option, which is proving the case cannot arise.

Why FSE is the interesting target

Zstandard is winning the succession to gzip because it decompresses fast — Langley's chart over 64 MiB of Lean/mathlib source puts zstd and gzip in a decompression-speed class of their own, on a log scale, while bzip2 and LZMA sit orders of magnitude slower in exchange for compression. (His measurements are from an Apple machine, where gzip is unusually well optimised.) Its entropy coder is where the design earns that.

A Huffman code can only spend a whole number of bits per symbol, so a symbol whose ideal cost is 2.3 bits has to round, and the rounding is paid for elsewhere in the alphabet. FSE is a state machine that gets around this. There are more states than symbols, and each symbol holds a share of the states proportional to its probability. Each state stores three things: its symbol, how many bits to read from the stream while in it, and a baseline that is added to those bits to get the next state. States still read whole bits, but a symbol whose ideal cost is one and a half bits can have half its states read one bit and half read two, hitting the target on average. In the post's 16-state example, symbol B occupies five states for a probability of 5/16, ideal cost 1.68 bits; three of its states read two bits and two read one, and weighted by how often each is used the average comes out about right. The table itself is never transmitted — the RFC gives an algorithm for rebuilding it from the probabilities alone, which is exactly why the construction function is the piece worth proving correct.

Two structural consequences follow. Any symbol can follow any other, so every symbol must be able to reach every state; symbol D with a single state therefore has to read four bits, enough to name any of the sixteen, while symbol B's five states partition the state space between them so that exactly one B-state reaches any given target. That partition property is clause four of the theorem above. And because the choice of which state to land in carries information forward, encoding cannot run forwards: the encoder starts at the end of the sequence and works backwards, writes output incrementally anyway, and so the decompressor has to seek to the end of a block and read its bits backwards. FSE carries no inter-symbol structure; that job belongs to the surrounding LZ77 layer, and FSE mostly encodes its back-reference offsets and lengths, with Huffman still used elsewhere in the format.

Lean as a programming language

Langley's case for Lean is not only about proofs. It is strict rather than lazy, so unlike Haskell you can reason about when work happens. Its monadic do notation has for, return, and break, so imperative-shaped code reads as imperative code. And it will mutate objects in place when their reference count is one, which makes array updates as cheap as in an imperative language. That last one is a sharp edge, because Lean has no linear types to help you keep the count at one: an inconspicuous extra reference to a large array can crater performance with no type error to warn you.

What did not work

The second half of the experiment was verified assembly. AWS's LNSym gives Lean a semantics and simulator for AArch64, which suggests a workflow where you prove an optimised assembly routine equivalent to its Lean counterpart, call it through extern at run time, and let LLMs optimise freely without being able to introduce functional bugs — cheap verified assembly, where today it is only economic for cryptography. It did not scale. LNSym's own 32-bit popcount example uses bv_decide, a certifying SAT solver, and needs more memory than Langley's machine has. Tiny functions do work end to end, including the extern call. Neither he nor several LLMs got past that.

He lists the open questions honestly. Proof effort may scale badly in large systems in a way that outruns the models. Very strong types amplify the blast radius of a change, since every derived type has to be updated. Lean is high-level and not right for everything; his own decoder runs about ten times slower than the zstd command line. He did not publish the code, on the grounds that for a task this well-defined an LLM would probably do a better job than he did, and he points at lean-zip, which goes further and proves round-tripping.

Where this sits

The claim is bounded and testable, which is what makes it worth keeping. It is not that formal verification is solved; it is that one specific line item — the proof of a nontrivial universal property about working decoder code — moved from days of expert effort to twenty minutes of inference. That is the same shape of argument if-ai-writes-your-code-why-use-python makes about language choice, where the human cost that made a language impractical is the thing the models removed, and it inherits the same weakness: the cost that disappeared is the one being measured, not necessarily the one that dominates a real project. llm-mathematical-research is the neighboring case where models produce formal or research-level mathematical content rather than repair proofs about code. Shriram Krishnamurthi, in pl-education-in-the-age-of-ai, is optimistic about the same shift and wary of the path this post barely exercised: when the model finds no proof, a non-expert gets no counterexample and nothing to act on.

Dependent types are the far end of the static axis in type-system-axes — checks done entirely before the program runs, on properties arbitrary enough to include primality and unique reachability. Everything the vault has on coverage-guided-fuzzing and differential-fuzzing is the pragmatic alternative for exactly this workload: a format decoder with a reference implementation to compare against is the canonical differential-fuzzing target, and fuzzing finds counterexamples where a proof establishes their absence. The trade between them is now priced differently than it was.