The gap between dependent type theory and practical software engineering has always been one of effort, not expressiveness. The type systems of Coq (now Rocq) and Lean can encode essentially arbitrary mathematical invariants. The problem is that encoding them costs time at a rate that, historically, made the approach economically indefensible for most software projects. The seL4 retrospective, frequently cited in this space, found a roughly 10x ratio of proof effort to design and implementation effort, yielding more than 20 lines of proof code per line of C. That is a steep price for correctness guarantees that, in principle, eliminate entire categories of bugs.
A post from Adam Langley at ImperialViolet makes a concrete, empirically grounded claim: that claim is now obsolete. LLMs, applied to Lean proof obligations, can discharge non-trivial theorems about real algorithms in roughly 20 minutes of interaction, consuming a small fraction of a standard API subscription. If that holds up at scale, it is a structural change to the cost-benefit calculus of formal verification.
The Proof Burden Problem and Why SMT Solvers Were Not Enough
Prior attempts at automating proof obligations concentrated on SMT solvers. F* is the canonical example: it routes verification conditions through Z3 or similar backends, which works well for simple arithmetic and memory safety properties. The failure mode is well-known to anyone who has used these systems seriously. SMT solvers are sensitive to the precise form of the query. A slight change in how a lemma is stated can turn a sub-second discharge into an hours-long divergence, with no clear signal about which direction to push. Practitioners develop intuitions about what the solver will accept, but those intuitions are hard to transfer and fragile under refactoring.
The deeper issue is that SMT-based automation is fundamentally brittle at the boundary between decidable fragments. Linear arithmetic is fine. Nonlinear arithmetic is not. The moment your proof obligation crosses that boundary, the solver becomes unreliable. Lean's tactic system, by contrast, is a programmable proof search environment. Tactics like omega, simp, and bv_decide are composable and inspectable. An LLM generating tactic scripts is operating in a richer, more compositional space than one generating SMT queries.
FSE Table Construction as a Verification Target
The choice of Zstandard's FSE (Finite State Entropy) table construction as the primary verification target is well-motivated. FSE is an ANS-based entropy coder developed by Yann Collet, building on Jarek Duda's asymmetric numeral systems work. The decoder's inner loop relies on a set of invariants about the state table that are subtle enough to be non-obvious but structured enough to be formally stateable.
The theorem proven in the post captures four properties of a correctly constructed FSE table:
- The table has exactly
2^accuracyLogentries, matching the accuracy parameter. - The number of states assigned to each symbol matches its quantised probability, i.e.
probCells probs[s]for symbols. - For every state, reading
nbBitsbits and adding the baseline produces a valid state index within bounds. - For every symbol with non-zero probability and every target state, there is exactly one source state for that symbol that transitions to the target. This is the surjectivity/injectivity property that makes the state machine well-defined as a reversible code.
The fourth property is the most interesting. It is essentially a bijectivity condition on the state transition structure, and it is precisely the kind of thing that gets silently assumed in optimised decoding loops. In C or Rust, this assumption lives in a comment, if anywhere. In Lean with this proof, it is a machine-checked guarantee. The fact that an LLM could produce the proof tactics for this, without the programmer having to manually construct the argument, is the substantive claim.
One detail worth noting: the LLM-assisted proof process required refactoring the table-generation code away from Id.run blocks, which drop into an imperative monadic context that the proof machinery handles less gracefully. This is a real cost. Proof-friendly code is not always the same as performance-friendly or readability-friendly code. The tension between these is not new; it is precisely what the seL4 team called proof engineering. The question is whether LLMs reduce the cost of that engineering sufficiently to make it tractable.
Lean as a Systems Programming Language
The post touches on Lean's practical properties as a programming language, which deserve some analysis independent of the verification angle. Lean is strict rather than lazy, which removes the performance unpredictability that makes Haskell difficult to use in latency-sensitive contexts. Its monadic do notation supports imperative-style control flow including loops and early returns, which substantially reduces the syntactic overhead of writing procedural algorithms.
The reference-counting optimisation that enables in-place mutation is significant. Lean's compiler will perform destructive updates on arrays when the reference count is exactly one at the mutation site. This is semantically equivalent to a purely functional update but has the performance of a mutable one. The catch is that Lean lacks linear types, so there is no static guarantee that a reference count will be one at any given point. A stray reference held in a closure or a data structure can silently revert the operation to a copying update, with a substantial performance penalty. This is a known sharp edge in the language design, and it limits the degree to which performance can be reasoned about statically.
The toy Zstandard decoder described in the post runs about 10x slower than the reference zstd implementation. That gap is not surprising for a high-level functional implementation without careful attention to low-level optimisation, but it does illustrate that Lean is not yet a drop-in replacement for systems languages in performance-critical paths.
Verified Assembly and the Limits of Current Tooling
The aside on AWS's LNSym, an AArch64 semantics and simulator, points toward a more ambitious vision: proving equivalence between a Lean specification and an optimised assembly implementation, then running the assembly at runtime while relying on the Lean proof for correctness. This is the approach used in verified cryptography, most prominently in projects like HACL* and the Fiat Cryptography work that ships in production TLS stacks.
The practical results here are sobering. The bv_decide tactic, which uses a certifying SAT solver to discharge bitvector arithmetic goals, exceeded available memory on the author's machine for even the small popcountextern mechanism for calling verified assembly from Lean does work. But scaling beyond trivial examples proved intractable for the combination of the author and several LLMs. This is an honest and important data point. The memory and time costs of bit-precise reasoning about machine code remain high, and LLMs do not yet help much with the combinatorial explosion that occurs as function size grows.
What This Actually Changes
The honest assessment is that LLM-assisted proof automation is real and useful now for bounded, well-defined algorithmic components. The FSE table construction proof is a genuine result: it covers a non-trivial algorithm, it captures properties that matter for correctness, and it was produced at a cost that is plausibly within the budget of a careful software project. That is new.
What remains unclear is how the approach scales. Dependent types amplify the scope of changes: modifying a core data structure requires propagating type changes and re-proving theorems throughout the dependency graph. In a large codebase, that graph can be extensive. The post acknowledges this directly, noting that proof effort may scale poorly in larger systems even with LLM assistance. The seL4 project was large enough to develop institutional expertise; a typical software team is not. Whether LLMs can substitute for that expertise at scale is an open empirical question.
The more conservative claim, that LLM-assisted Lean proofs are now practical for self-contained algorithmic modules with clear formal specifications, is well-supported by this work. Entropy coders, cryptographic primitives, protocol state machines: these are natural targets. The broader vision of dependent types as a routine tool in production systems software is still some distance away, but the distance has measurably shortened. For researchers and engineers working at the intersection of formal methods and systems programming, that is worth paying attention to.