LLMs Bring Proof Automation to Dependent Types in Lean

Adam Langley has long admired dependently-typed languages like Coq and Lean. These languages offer type systems that can encode and enforce very subtle invariants. In regular programming languages, those invariants end up as comments at best. They get lost as teams grow, leading to misunderstandings and components that do not fit together. By the time the problem is noticed, the components have grown large enough that aligning them becomes a wearying prospect. Dependent types promise a way to write those invariants formally and have a machine check them.

Coq recently changed its name. Langley recalled a conference in Princeton years ago where he suggested that having a programming language called Coq was an impediment in the English-speaking world. The audience did not agree at the time. He also joked that many talks sounded like a speech by Tyrion Lannister, with so many Coqs and Hoares. The joke fell flat, coming before the final season of that show and its collective memory-holing.

The problem has always been that great type-system power requires great proof effort. Langley can attest to entire days spent proving simple things. Doing proofs is challenging, interactive, and has a clear goal. But it takes a lot of time, especially if you do not know what you are doing. There is also the galling experience of realizing after hours of effort that the goal you are trying to prove is false. The seL4 effort found that engineers spent about 10 times as much time proving as they did designing and implementing. They ended up with more than 20 times as many lines of proof code as C code.

That overhead has made programming in dependently-typed languages extremely niche. It has spurred people to try to automate it away. Langley is passingly familiar with F*, where an SMT solver automatically discharges obligations. That works for simple cases, but it is easy to craft something that causes the SMT solver to run for hours. People who use these languages a lot develop a sixth sense for what makes the solver happy and craft everything around that. It converts the problem into mysticism, serving a complex and fickle god.

A critical fact is that, at least in theory, once the statement is correct, the contents of its proof are irrelevant. Only its existence matters. This is not entirely true because of two complicating factors. First, what the seL4 group called proof engineering: the need to structure proofs so that realigning them after code changes is reduced. Second, sufficiently complicated proofs can cause type checkers to blow up and consume vast amounts of memory.

LLMs now exist, and combined with proof irrelevance, they promise to be an extremely capable form of proof automation. With sufficient automation, you may not need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker, but in Langley's limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical. Langley wanted to play around with this, so he built a Zstandard decompressor in Lean, mostly because he was also curious about Zstandard.

Zstandard and Entropy Coding

Zstandard seems to be winning the competition to replace gzip as the canonical compression utility. It is another LZ77-style compressor, but it offers better entropy coding and a careful design that allows very impressive decompression speeds. It will never be as beautiful as bzip2, but the elegance of the Burrows-Wheeler transform does not count for much in the face of significant practical advantages.

A chart shows compression tradeoffs on 64 MiB of Lean/mathlib source. Space saved is measured farther right for more compression. Decompression throughput is measured in MiB per second on a log scale, with higher being faster. Measurements were taken on the standard reference computer, the author's machine. Note the log scale on the y-axis: gzip and Zstandard are in their own speed class. This is an Apple machine and Apple's gzip is especially optimized; expect gzip to be slower elsewhere.

Zstandard, by Yann Collet building on the seminal ANS work by Jarek Duda, has an RFC, but it is quite terse. It contains all the information needed to implement a decompressor, but unless you are already familiar with compression, you will need to re-read it several times. Langley had to read section 4.1 half a dozen times before he felt he had a decent grasp. Too late, he discovered that his colleague Nigel Tao has written a better write-up of Zstandard. If you want to understand Zstandard, you should read that. Langley will give an explanation of the most interesting bit, the entropy encoder, mixed with some evangelism about Lean.

The job of an entropy encoder is, given a set of symbols with non-uniform probabilities, to encode a sequence using the fewest number of bits. The classic entropy coder is a Huffman encoder. Huffman encoders build a binary tree with symbols at the leaf nodes. Huffman showed that a simple algorithm produces an optimal prefix-tree: take the list of symbols, find the two with the least probability, and form a tree node with them as children. That tree node then has a probability that is the sum of its two children, and you repeat the algorithm with two fewer symbols, now with a tree node in the mix. Each step reduces the size of the set by one, so it terminates, and it produces an optimal tree. Huffman trees are very fast because you can build a table indexed by the next n bits, where n is the length of the longest code. The table entry tells you what symbol you have decoded and how many bits to unread. The drawback is that Huffman trees can only use a whole number of bits for each symbol. If -log2(p) = 2.3, you ideally want to use 2.3 bits. But Huffman forces you to round up to 3 bits or round down, forcing other symbols to consume more bits.

Zstandard uses Huffman trees, but it also has a higher-compression entropy encoder called FSE. FSE is a state machine. There are more states than symbols, and each symbol gets a fraction of the states that mirrors its probability of occurrence. If a symbol is expected to appear 50% of the time, it gets about 50% of the states. Each state has three values: the symbol for that state, a number of bits to read from the bitstream when in that state, and a baseline state number that is added to those bits to get the next state. The problem with Huffman trees was that they could only use a whole number of bits, and these states also read a whole number of bits. The trick is that if you are aiming to read one and a half bits for a given symbol, then half of its states will read one bit and half will read two bits. You hit your target on average. The table of states is never transmitted. The RFC prescribes an algorithm for building the table from a list of symbol probabilities, so only the probabilities need to be transmitted.

Let us do an example. Say we have four symbols and we are going to use 16 states. We have to approximate the symbol probabilities in terms of 16ths. If you want a more accurate approximation, you can use a larger number of states. Zstd actually never uses fewer than 32 states.

Any symbol may follow any other symbol, and a symbol might only have a single state. Every symbol must be able to reach every state. Consider state three, which is the only state for symbol D. Because it is the only one, it has to read four bits, which is sufficient to encode any other state. For symbol B, its states only demand that you read one or two bits. However, the set of 16 possible next states is exactly partitioned between those states for symbol B. For any particular state, there is exactly one state for symbol B that can reach it.

A table shows states 0 through 15 with symbols A, B, C, D. State 0 is A, state 1 is A, state 2 is B, state 3 is D, state 4 is A, state 5 is B, state 6 is C, state 7 is A, state 8 is B, state 9 is C, state 10 is A, state 11 is B, state 12 is C, state 13 is A, state 14 is A, state 15 is B. Another table shows the number of bits read for each state: states 0-1 read 1 bit, states 2-3 read 1 bit, states 4-7 read 2 bits, states 8-11 read 2 bits, states 12-15 read 2 bits.

Consider symbol B, which has a probability of 5/16. The ideal number of bits to encode that symbol is -log2(5/16) = 1.68. There are three symbol B states that read two bits and two that read one bit. The states are not used equally often, and weighted by how often they are used, the average comes out to almost exactly the right value for the quantized probabilities. If you want to capture the true symbol probabilities with more accuracy, use a bigger table.

The central trick is that by giving multiple states to more common symbols, the encoder does not just pick a symbol. It also picks which of that symbol's states to land in, and that choice carries information forward to the next symbol. That is where the fractional bits of information go. This entropy encoder is still table based, so it runs very quickly.

The wrinkle is that you cannot work forwards. Assume you want to encode C, D. Which C state do you start in? D only has one state, so it has to be the C state which can reach that one. If D had multiple states, you would need to worry about what came after D to know which of those you needed. FSE forces you to start at the end of the sequence and work backwards. That is not too bad because you usually need to know the whole sequence to calculate the symbol probabilities anyway. A Zstandard compressor thus encodes symbols back-to-front, but writes output incrementally, so the decompressor has to seek to the end of a block and read the bits backwards to straighten it out. That is getting into broader details of the format that Langley will not cover. See Nigel's piece.

Basic entropy encoders do not care about inter-symbol probabilities. They cannot use the fact that the letter Q is disproportionately followed by the letter U in English. There has to be some other encoding that exploits those redundancies. In Zstandard, that is a traditional Lempel-Ziv structure where it encodes either literal bytes or back references to previously decoded data. FSE is primarily used for efficiently encoding these back reference offsets and lengths.

Lean and Dependent Types

Let us talk about Lean. Langley said it is a dependently-typed language, and that concept is better articulated in examples than in a complicated definition. Here is the type of a function that reads n bytes from a stream and, if it does not throw, returns a byte array that the type system knows is n bytes long:

def IO.FS.Stream.readExact (st : Stream) (n : Nat) : IO {ba : ByteArray // ba.size = n} := ...

Here is a function that returns two numbers and a byte array such that the first number is prime, the sum of the two numbers is divisible by six, and the byte array is at least as long as the smaller of those two numbers:

def getResult : IO (Σ a b : Nat, { bytes : ByteArray // Nat.Prime a ∧ 6 ∣ a + b ∧ Nat.min a b ≤ bytes.size }) := ...

That is not a type that anyone will ever need. It just demonstrates that you can go as wild as you want. Dependently-typed languages are sufficient to encode even very complicated mathematical structures. Lean's dominant use at the moment is as a formal language for stating and proving mathematics. The recent book, The Proof in the Code, is a short, well-written articulation of the story of how Lean came to be. The author does completely butcher constructive mathematics for a few paragraphs, but other than that, Langley enjoyed it.

Lean is a purely functional language like Haskell, although it has a few properties that make it potentially more convenient as a programming language. First, Lean is strict, while Haskell is lazy. Strictness means that arguments to functions are evaluated before the call happens, whereas in Haskell the evaluation of arguments is deferred until the value is actually required. In Haskell it is free to write expensive expressions and pass them into functions, because they will only be computed if they end up being used. But it also means that computation can happen in very surprising places in the program. This is a contentious topic, but while Langley appreciates the elegance of laziness, it can make the performance of programs hard to reason about.

Next, Lean has some nice helpings of sugar. Its monadic do notation contains for loops and return statements and break statements. If you want to program in an imperative style, you can do so pretty reasonably.

Lastly, Lean has an optimization where it will make mutating updates to objects as long as their reference count is equal to one. You can mutate an array in place as efficiently as in an imperative language, as long as you are careful not to have a reference to it someplace else. Unfortunately, Lean does not have any aspects of a linear type system that Langley is aware of, so it does not help you in ensuring that there is only a single reference to a value. It is a bit of a sharp edge that a seemingly minor tweak to the code can completely crater its performance by holding on to a reference to a large array somewhere inconspicuous. But it does mean that if you are trying to optimize the performance of something, you have a lot more tools at your disposal.

Here is an example of some of this, from the zstd decoder Langley sketched:

while true do let some blockHeaderBytes ← input.readExactOrEof 3 | break let some blockHeader := BlockHeader.fromBytes blockHeaderBytes frameHeader | throw ( .userError "invalid block header" ) let blockBytes ← input.readExact blockHeader.contentSize

match hty : blockHeader.type with | .rle => let b := blockBytes.val[0]'( by rw [blockBytes.property, blockHeader.contentSize_rle hty]; omega )

Focus on line 9. There is an array index there, which is exactly the sort of place that implicit invariants live. blockBytes had better not be empty. C-like languages will give you undefined behavior in that case. Modern languages will throw at run-time, or only give you an optional value to avoid that. Lean has another option: prove that it is not empty. That is what line 10 does. blockBytes.property is the fact that it is as long as the requested read, exactly blockHeader.contentSize bytes long. blockHeader.contentSize_rle is this:

theorem BlockHeader.contentSize_rle (h : BlockHeader) (hty : h.type = .rle ) : h.contentSize = 1 := by simp [contentSize, hty]

That is a proof that, when the type is rle, the contentSize is always one. With those facts, Lean can figure out the rest.

It is a really short proof and probably Langley could have figured that out himself, but we can aim much higher. He wrote an implementation of the FSE table construction algorithm from the RFC. The RFC contains test vectors for it: three sample outputs from given probabilities. Those go into unit tests. But in Lean, we can also prove universal properties of the function:

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) := ...

Repeating that in words: Assuming that the table construction function, when given the accuracy constant and a list of symbol probabilities, produces a value, then the table has the right size, each symbol appears the right number of times, each state can only lead to valid states, and each state can be reached from exactly one state for each symbol.

These are the subtle assumptions that an optimized decoding inner-loop requires, and things that can only ever be implicit or mere comments in weaker type systems. Proving strong statements like that is part of the 10x effort that the seL4 retrospective described, and a major barrier to the adoption of dependent types in regular software. Several LLMs can do it automatically now in about 20 minutes, using only a fraction of a $20/month subscription quota. It will probably be table-stakes next year. Langley admitted that they needed to change the table-generating code when doing so. He had used too much Id.run, dropping into imperative mode, and that is harder for the proof machinery to work with. But Lean are working on it. He confirmed that the proofs type-check and that there are no sorries.

The Future of Proof Automation

Combining dependent types and LLMs is not a new idea, but not much has been done on applying the combination to quotidian software engineering. Lots more experience would be needed. Very strong types can amplify the scope of changes as they have to be propagated out through all the derived types. Perhaps the proof effort scales poorly in larger systems, such that even modern LLMs cannot keep up. Lean is a high-level language, and that is not suited to everything. Langley's toy Zstandard decoder is 10x slower than zstd on the command line. Still, proof automation is here now and we, practically speaking, have a new type of programming language available to us. That is exciting.

Langley is not publishing the code because, for a small, well-defined case such as this, the LLMs can probably do a better job than he did. He did this to learn Lean a little and does not hold his explorations up as an exemplar. This was inspired by lean-zip which does much more, includes a compressor, and proves round-tripping.

AWS made LNSym: a semantics and simulator for AArch64. That is cool. Perhaps we could use it to show equivalence between an optimized assembly implementation of some functions and their Lean counterparts, and then use the assembly code at run-time. Then we could let LLMs rip at optimization and they could not introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap.

Langley put some, mostly LLM, time into trying this. The small popcount example from the repo uses bv_decide, which is a certifying SAT solver, and that example requires more memory than his system has, which does not bode well. Tiny functions do work, and it is possible to get an equivalence proof to tiny Lean functions, and then to use extern to call them at run-time. But he, and a few LLMs, could not get it to scale any further.

Related on Neura Market

• AI Tools Directory, Explore AI-powered development tools and automation platforms.
• Automation Marketplace, Discover solutions for automating software engineering workflows.
• Developer Tools, Browse tools for formal verification and type-safe programming.