Adam Langley, who writes the imperialviolet blog and works on security at Google, published a piece on July 26 called "We have proof automation now." The title is not hype. He built a Zstandard decompressor in the dependently-typed language Lean, and then had several LLMs automatically prove nontrivial universal properties of the entropy decoder in about 20 minutes each, using a fraction of a $20/month API subscription. The thing that used to make formally verified software impractical was that the proof effort cost roughly 10 times as much engineer time as writing the code in the first place. That 10x was the wall. The wall has a crack in it now.
What dependent types actually buy you
Most type systems check shapes. A function takes a string and returns an int. Lean, like Rocq (formerly Coq) and Agda, goes further. The return type can carry a proof that the int is prime, or that a byte array is exactly 256 bytes long, or that an index is in bounds. The type system can encode arbitrarily subtle invariants and check them at compile time. What you trade for that power is proof obligation. Every claim baked into a type needs to be discharged, and discharging it by hand is slow.
Langley's post quotes the seL4 retrospective, which is the canonical data point on this. The seL4 team, who verified a production microkernel in Isabelle/HOL, found that even after they got experienced at it, they spent about 10 times longer proving than designing and implementing. The proof artifacts were more than 20 times larger than the C code they verified. That ratio is why almost nobody outside specialized niches writes verified software. The code is fine. The proofs will eat your project.
The honest version is that doing proofs is also kind of fun. Langley says so himself. It is interactive, there is a clear goal, and you know when you are done. But "fun" does not scale to shipping software, and the periodic experience of proving something for hours only to realize the statement was false is a specific kind of misery that tends to cure people of the hobby.
What the LLMs actually proved
The specific example is the FSE entropy coder at the heart of Zstandard. FSE is a finite state machine where each state maps to a symbol, a number of bits to read, and a baseline. The RFC gives an algorithm for building the state table from a list of symbol probabilities, but the correctness conditions are not spelled out as theorems. They are the assumptions an optimized decoding loop silently depends on. In a C implementation they live as comments, or as nothing.
Langley wrote the table construction in Lean and then asked several LLMs to prove four properties, which he states formally. Stripped of the Lean syntax, they are: the table has the correct size for the configured accuracy; each symbol gets the right number of states given its probability; for every state, reading nbBits and adding the baseline yields a valid next state; and for every symbol with nonzero probability and every target state, exactly one state of that symbol can reach the target. That last one is the real condition. It is what makes the decoder total: you never get stuck, every path through the state machine is covered.
This is not a unit test. A unit test checks three example inputs. This proves the property holds for all possible probability distributions and all possible table sizes. Several LLMs discharged it in roughly 20 minutes, using only part of a $20/month quota. Langley confirmed the proofs type-check and contain no sorry axioms, which means no holes were quietly admitted. He did note they needed him to refactor the code first because his heavy use of Id.run (Lean's imperative escape hatch) made the proof machinery harder to work with. So it is not fully hands-off, but it is close.
Why this is different from "LLMs write code"
LLM-generated code has a trust problem. You cannot tell by reading it whether it is correct, and the model cannot tell you either. People have shipped subtle bugs this way because the code looked right, compiled, and passed surface checks. The standard mitigation is tests, but tests are a sample. They prove the code works on the cases you remembered to check.
LLM-generated proofs have the opposite property. The proof either type-checks or it does not, and the type checker is a small, trusted kernel you can audit independently. If the LLM produces an invalid proof, Lean rejects it. There is no "looks correct but is not" failure mode for the proof itself, only for the theorem statement. So the human job shifts from "verify the LLM's reasoning" to "verify the LLM's statement is the statement you actually wanted proved." Statements are shorter and easier to read than proofs. The trust bottleneck moves to the place where human review is cheap.
This is the structural reason the combination is powerful. LLMs are unreliable at correctness but fast at generation. Proof assistants are slow at generation but perfect at checking. Put them together and the failure modes cancel in the direction you want. The LLM proposes, the kernel disposes.
What does not work yet
Langley is careful about the limits and I want to be too. His toy Zstandard decoder is about 10 times slower than the stock zstd binary. Lean is a high-level language and the verified artifact is the Lean code, not optimized assembly. For crypto and compression you often want the latter. He also tried extending the idea to verified assembly via AWS's LNSym project, which gives Lean a semantics and simulator for AArch64. He and several LLMs could prove equivalence between tiny Lean functions and their assembly counterparts, but could not get it to scale. A small popcount example already exhausted system memory because the SAT-backed bv_decide tactic blew up.
There is also the question of proof engineering. Proofs need to be structured so that re-proving them after a code change does not cost the whole effort again. Langley suggests that if LLMs can regenerate proofs cheaply, the proof engineering tax drops, because you stop caring about proof reusability when regenerating is nearly free. That is plausible for small modules. Whether it holds for a system with hundreds of interdependent theorems is an open question, and probably the one that determines whether this scales past toys.
Then there is the statement-correctness caveat I raised earlier. An LLM that can prove anything you ask it to is only useful if you ask it the right thing. "Prove this function returns a byte array of length n" is easy to state and hard to mess up. "Prove this parsing routine never accepts a malicious input" is the actual security property, and it is much harder to express precisely. The LLM cannot help you figure out the right theorem if you do not already know it. The automation widens the bottleneck at the proof step but leaves the specification step as a human task.
Why this landed at this particular moment
Proof automation has been a research goal for as long as proof assistants have existed. The dominant prior approach was SMT-backed tactics, like F* uses. Langley's description of that approach is unflattering and worth quoting indirectly: it works for simple cases, but it is easy to write something that sends the solver into space for hours, and experienced users end up developing a sixth sense for what keeps the solver happy, which converts the problem into a kind of mysticism. You serve a complex and fickle god. SMT tactics reduce proof effort, but they do not eliminate it, and the cases where they fail are exactly the cases that are hard to debug.
LLMs fail differently. They do not get stuck in the same way. They might produce a wrong proof, but a wrong proof is rejected. They might need a code refactor first, but a refactor is local. The failure modes are ones you can actually see and act on, rather than a solver silently chewing on CPU for three hours. That is not a rigorous advantage, but it is a practical one. Before LLMs, the realistic options for proof automation had a ceiling that kept formal methods in the niche. After LLMs, the ceiling is somewhere we have not found yet, and the early returns are surprisingly good.
What I think this is worth
Langley ends with "this is exciting" and he is right, but I want to be specific about what kind of exciting. It is not that verified software is about to become default. The performance gap is real, the specification problem is unsolved at scale, and the assembly verification path is not ready. What changed is the cost structure of the proof step specifically. That step was the dominant cost in verified software projects, by a factor of 10. If LLMs bring it down by an order of magnitude, the economics of formal methods shift from "we can only afford this for a microkernel or a crypto primitive" to "we can afford this for a parser, an encoder, a state machine, a protocol implementation." The set of things worth verifying just got bigger.
The part I am not yet sold on is the fully autonomous version. Langley's LLMs needed him to refactor the code first. They needed him to pick the right theorem statements. They needed him to confirm no sorry leaked in. That is a human in the loop who knows Lean and knows compression. The skill floor for proving just dropped sharply. The skill floor for specifying the right thing to prove did not move. The people who will get value from this first are the ones who already knew which invariants mattered and just could not afford the time to prove them. For everyone else, the bottleneck is now "do you know what you should be proving," which is a harder question than it sounds.
Still. A decade ago, proving a universal property of a real entropy coder took a formal methods specialist days. Now it takes an LLM and a prompt, and a $20 subscription you probably already have. Langley calls this "a new type of programming language available to us," and that framing is not wrong. It is just earlier than he admits. The infrastructure is not built. The tooling around statement validation, proof regeneration at scale, and integration with real build systems does not exist yet. Someone has to build it. But the core thing, the LLM-can-discharge-the-proof, works now. That is the part people should be paying attention to, because it is the part that was supposed to take another five years.