Notes ·
LLMs May Finally Make Formally Verified Software Practical
Adam Langley writes at ImperialViolet about using LLMs and the Lean theorem prover to implement part of a Zstandard decompressor and formally prove important properties of the code.
Dependently typed languages such as Lean can encode detailed software requirements directly into their type systems. Instead of merely testing a few examples, developers can prove that an implementation satisfies an invariant for every valid input.
The problem has always been the cost. Langley points to the formally verified seL4 project, where engineers reportedly spent around ten times longer proving the software than designing and implementing it, producing more than twenty times as much proof code as C code.
LLMs may change that tradeoff.
For the Zstandard experiment, several models were able to generate proofs for subtle properties of an entropy-decoding table in about twenty minutes. The resulting proofs verified that the table had the correct size, contained the right number of states, never produced invalid state numbers and provided exactly one valid transition for every reachable state. Langley checked that the proofs compiled and contained no unproven placeholders.
I strongly agree with the direction this suggests. The future may belong to programming languages that embed theorem provers deeply into their type systems. LLMs can generate implementations and much of the accompanying proof work, while the compiler verifies that both satisfy the specification.
Testing will not disappear. A proof cannot rescue an incorrect or incomplete specification, and applications will still need integration, performance and usability testing. But formal verification could replace many tests that merely sample whether an implementation behaves as intended.
That shifts the programmer’s most valuable skill. Writing code becomes less important than precisely describing what the code must do, which conditions must always hold and what outcomes must never be possible.
The future programmer may spend more time writing formal specifications than implementations. The LLM writes the code and proofs. The type checker decides whether either can be trusted.