Memory-safety failures account for a large share of serious vulnerabilities in C and C++ codebases. We show how LLMs and proof assistants such as Lean 4 can substantially reduce the cost of formally verifying memory safety in legacy C.

In under two weeks, we built an experimental C-to-Lean pipeline and proved that the Clight (CompCert's C intermediate representation) model of zlib’s 266-line inflate_table function is memory-safe and terminating. We also describe the methodology behind the result and how it could scale to larger parts of existing C codebases.

Background - our target application for memory safety

zlib is the compression library behind gzip, zip, and PNG. It is ubiquitous: it runs in the Linux kernel, in every major browser, in Git and in OpenSSH, on billions of devices. Furthermore, it parses untrusted input, meaning that a single out-of-bounds write can become a remote-code-execution vulnerability.

We chose to focus on inflate_table, 266 lines of C that build the Huffman decoding tables that the main inflate function uses to decompress a stream. Its input is an array of code lengths derived from the compressed stream.  Those values determine table indices used in low-level pointer operations, making this the place where attacker-controlled data comes closest to raw pointer arithmetic. Specifically, from that data it computes the table indices and writes through a caller-supplied pointer, and on most of those writes there are no runtime bounds checks by design.

The arithmetic is supposed to guarantee the table indices stay in range. What makes each write safe is an invariant of the algorithm. A comment dating from the original implementation records the intended invariant, but does not supply its derivation:

/* fill in remaining table entry if code is incomplete (guaranteed to have
   at most one remaining entry, since if the code is incomplete, the
   maximum code length that was allowed to get this far is one bit) */

This comment relies on a mathematical property of Huffman codes to guarantee that there is enough room in the table whose indices we compute. The key idea is the Kraft inequality: a Huffman code of length n consumes 2-n of the total available code space. For example, a 1-bit code uses half the space, while a 3-bit code uses one eighth. zlib performs an upfront check that the set of code lengths supplied by the input does not consume more space than is available. It also restricts incomplete codes so that, in the cases it accepts, at most one table entry can be left over.

After that check, the rest of the function relies on this accounting staying correct. Every unchecked write downstream is in bounds because of that accounting, that is the offsets place exactly as many symbols as were counted, the fill loop's countdown ends exactly on zero, and the final write can only hit index 0 or 1. The problem is that this guarantee is spread across seven loops, so it is difficult to establish just by reading, which is where a rigorous mathematical treatment shines.

From code to math - converting from C to Lean and reasoning about memory safety

We built an experimental tool, CLean (C to Lean), as a fork of CompCert (Leroy, CACM 2009), the formally verified C compiler. CompCert's ecosystem already supports program verification on this representation in Rocq - that is what VST does, with proofs that additionally connect to CompCert's compiler-correctness theorem. CLean is an experiment in doing the same kind of reasoning in Lean 4. CompCert ships a tool clightgen that exports a C file's Clight AST for verification in Rocq; CLean extends it to emit Lean4 instead, and pairs the exported AST with a Lean port of CompCert's Clight semantics plus a separation logic to reason about it. 

The pipeline is simple: CLean parses inftrees.c and generates its Lean model mechanically. We then write the specification, specifically a list of memory regions the function is allowed to touch and the preconditions the function’s caller must meet. We then come up with proofs of the theorems which the Lean kernel checks step by step.

In the Clight semantics, an invalid load, store, or deallocation that is out of bounds, misaligned, or lacks the required permission has no successor state. The execution becomes stuck, representing undefined behavior.
An execution may therefore return, become stuck, or continue indefinitely. Memory safety rules out reachable stuck states; termination separately rules out infinite execution. Our theorem establishes both: every reachable state can continue to a return state. Because the modeled semantics is deterministic, this excludes both undefined behavior and divergence for calls satisfying the stated preconditions.

The theorem we proved says, in English:

Given a caller that satisfies five documented preconditions:

A1. the buffers it passes are real, separate C objects with the sizes and permissions inflate_table expects: the input array of code lengths readable, the scratch array and the output table writable, none of them overlapping;

A2. every code length is at most 15 (zlib's own documented, unchecked precondition), and the provided type is either CODES, LENS or DISTS;

A3. the symbol count fits the code type: at most 19 code-length, 288 literal/length, or 32 distance codes;

A4. the output table has the required capacity for the selected code type: at least 852 entries for LENS, 592 for DISTS, or 2 for CODES;

A5. on the one path where the function itself never checks capacity, the requested root table is wide enough for the longest code;

then: every state inflate_table can ever reach either takes another step or is the state where it has returned. It always returns, with a code in {−1, 0, 1}. It hands back everything it borrowed, touches nothing else, and performs no observable interaction with the outside world.

Four independent guarantees are bundled there:

P1. Memory safety: no reachable state is stuck;

P2. Termination: it returns rather than looping forever which the step-by-step construction of the execution gives us on top, since a memory-safe function could still loop forever;

P3. Frame preservation: every byte outside the declared region is untouched;

P4. no I/O (no system calls). Since the semantics is deterministic, the safe execution established by the proof is the only execution, that is "some run is safe" becomes "every run is safe."

The theorem itself:

theorem inflate_table_no_stuck (ge : CGenv) …
  (hsc : SideConds L ty codes cap b0)    -- side conditions of the memory model
  (ha  : Assumptions ty codes cap b0 lensF) : -- what the caller must guarantee
  ∃ r m', (r = -1 ∨ r = 0 ∨ r = 1) ∧ postHeap …
    -- returns -1, 0 or 1; memory handed back
    ∧ ∀ t s', Star (Step ge fe) (.Callstate f_inflate_table args m) t s' →
      t = E0 ∧ Star (Step ge fe) s' E0 (.Returnstate r m')

The last clause packs the whole claim into one line: every state reachable from the call was reached without any observable event (t = E0), and can still reach the return. Instantiate it at the call itself and you get termination; instantiate it anywhere else and you get that no reachable state is stuck, i.e. memory safety. 

There are no sorrys (Lean's placeholder for an unfinished proof) anywhere in the development. Beyond Lean's three standard axioms, the development carries two axioms mirroring CompCert's own treatment of external functions and inline assembly, plus their determinism. inflate_table calls no external function, so none of them is exercised by this proof. The semantics is a Lean port of CompCert's Clight semantics; the trust base is that port and the Lean kernel. Everything in between is machine-checked.

Proving the hard parts

Most of the 266 lines are routine once the framework exists, but some are more difficult to handle. We show two examples and how we handled them. 

(1) The sort loop writes at an index it reads from memory.

for (sym = 0; sym < codes; sym++)
    if (lens[sym] != 0) work[offs[lens[sym]]++] = sym;

In the snippet here, the index into work is offs[lens[sym]], a value loaded from memory and incremented in place. However, there is no check that it is within bounds. It stays in bounds because offs was built as a running sum of the length counts, and the number of non-zero lengths is exactly the number of symbols that will ever be written. Furthermore, the invariants have to prove that every index of work is eventually written, to ensure later reads of the work array will be valid. Proving that meant building a small combinatorial model of the function (counts, offsets, live symbols) as pure mathematics independent of the program, about 1,600 lines of it, and then showing the loop maintains the correspondence.

(2) The fill loop can underflow.

fill = 1U << curr;
do {
    fill -= incr;
    next[(huff >> drop) + fill] = here;
} while (fill != 0);

Here, fill counts down and stops at exactly zero. If incr didn't divide fill, it would wrap below zero and the loop would write thousands of entries past the end of the table. The invariant that rules this out was the hardest single proof in the development: it required tracking the Huffman code being built in bit-reversed form and relating zlib's left variable to the unused code space, that is the Kraft inequality as a loop invariant.

The 1995 comment shows the difference between a review and a proof: a reviewer reads it and might believe it, the proof needs to be derived.  The derivation depends on a validity check 150 lines earlier and a counting argument over the whole length distribution. It also surfaced something a review would rarely state: for the CODES type, zlib performs no runtime room check at all. Safety for that code type relies on an unwritten contract with the caller that inflate.c honors. Writing the proof is what forced that contract onto paper as the fifth of the five assumptions (A5): the caller must request a root table wide enough for the longest code, because on this path nothing in the function checks the table's capacity. Formally, every code length is bounded by some Lc ≤ root, and the table has at least 2^Lc entries. inflate.c satisfies these constraints since it calls inflate_table with root equal to 7, at most 19 codes whose lengths come from 3-bit fields (so ≤ 7), and a table of 1444 entries ≥ 2⁷. Nothing in inftrees.c checks or enforces it.

Trusting the proof

A proof is only as good as the spec, or in our case, the Lean model. The Lean semantics is validated by differential testing with CompCert as the oracle: 71,222 operation-level checks computing each integer, value, and memory operation with our Lean definitions and with CompCert's own code and comparing the results, plus 516 whole C programs run under our Lean interpreter and under CompCert's reference interpreter (ccomp -interp), all agreeing, plus checks of our zlib model against zlib's real output. This testing caught three real bugs in the port.

One cheap test that we perform in all our projects is a negative control. We wrote a C function that reads the tenth element of a nine-element array and tried to prove it safe. The attempt fails since the proof obligation reduces to 9 < 9, which Lean reports as false.

Notice that the theorem we proved is about memory safety and termination, not (yet) functional correctness. We cannot infer from the proof that the decoding tables are correct. In addition, the proof is about the Clight representation of the C source, not about compiled machine code. CompCert's own correctness theorem, which carries Clight-level proofs down to assembly, lives in Rocq; our Lean development does not connect to it. A proof in CompCert's native Rocq pipeline (e.g. via VST) would; ours stops at the C semantics level.

A different route to a verified zlib is to write a new implementation inside the proof assistant: lean-zip did this in Lean recently and proved functional correctness, a stronger property than ours. The two approaches are complementary. A rewrite verifies new code and ships it on the Lean runtime; we verify the legacy C that is already deployed, unchanged. A third-party audit of lean-zip found a heap overflow in the unverified Lean runtime and a DoS in its one unverified module. This verified/unverified boundary exists in both approaches, and for the zlib that runs in the kernel and in browsers today, ours is the boundary that covers it.

Measuring the effort

Our scope included 266 lines of C, 7 loops, and 7 return sites. The proof of memory safety produced around 20,000 lines of Lean, roughly 500 per-statement proofs, one main-loop invariant with 32 clauses and a termination measure. About 127 lines of proof per non-blank non-comment line of C. The whole pipeline builds in under three minutes; the proof itself rechecks in 29 seconds.

A 127:1 ratio has historically been considered very expensive and unscalable. Developments of this shape (semantics, program logic, and a full proof about production code) are measured in months or years of specialist time. That is why formal verification of C has stayed confined to a handful of heroic projects.

The entire proof of concept described here took about two weeks: the C-to-Lean tool, the semantics, the program logic, and the finished memory-safety proof, having no verification pipeline from C to Lean at the beginning at all.

The difference was, of course, LLM support. The proofs were written almost entirely by LLMs. The humans wrote next to none of the 20,000 lines; our work was reviewing the theorem statement, the assumptions, and the main memory-safety proof. The Lean kernel checked every step.
Nothing in the guarantee rests on trusting an AI. The 20,000 lines of proof are exactly as rigorous as they would have been in a multi-year project; they just took far less human time to produce. Proof assistants have always offered certainty at a price few were willing to pay, but now the price is collapsing.

Next steps

Nothing in the technique is specific to zlib. The proof architecture is designed to grow bottom-up: inflate_table trusts its caller, so its five assumptions are hypotheses today; the next step is to prove, inside inflate.c, that the caller establishes every one of these hypotheses, turning assumptions into theorems. Then the rest of inflate, then deflate, then the public API. From memory safety, the same machinery extends to functional correctness, up to statements like decompress(compress(data)) = data. The long-term goal is full functional correctness for any C library.

The two-week figure is a starting point. Much of what a human still does here (proposing invariants, drafting specifications, assembling proofs) is exactly the kind of work we are now working to automate end to end. As LLMs get more and more sophisticated in their ability to find bugs in code humans have long considered safe, proving code to be correct is the ultimate antidote. If your organization depends on C code whose safety currently rests on comments from 1995, we'd like to hear from you.