A week to prove zlib: verification starts looking like a line item, not a luxury

An AI translated the C zlib compression library into Lean, was required to pass the original test suite, and proved the strong property that decompressing a compressed payload returns the original data; the account comes from a published interview with Lean's founder, which puts the whole formalization at roughly one week ^[1][2][18]. If that holds, proving a widely deployed compression library now costs about what a serious refactor costs, which moves formal verification out of the research budget and into the plausible line item column for critical-path code.

Cost was always the objection. The same interview puts the historical price of writing proofs by hand and then maintaining them at often ten times the cost of writing the program itself ^[3]. The claim is that models are now good at both writing and maintaining those proofs, including long after the humans have forgotten why a particular step was there ^[4]. That maintenance half matters more than the authoring half. Industrial precedent exists on the old economics: the interview cites firms including Jane Street investing in this area, and the full verification of the seL4 microkernel ^[7].

The zlib job is not finished, and the unfinished part is the interesting part. What remains is performance optimization, and the optimization is not allowed to break the proofs already in place ^[2]. Complexity is described as the enemy of software verification, with automated proving workable only if the proofs are written modularly enough to extend ^[5]. Read that as an engineering constraint, not a caveat: a proof is a build artifact with a coupling problem, and a monolithic proof of a fast implementation will rot the first time someone tunes a hot loop.

The pattern offered is to keep a slow, obviously correct implementation as the specification, then have the model produce the fast version and prove the two equivalent ^[6]. That inverts the review burden. Humans read the slow reference; the machine argues about the fast one. The claimed second-order effect is that engineers stop avoiding aggressive rewrites, because equivalence either gets proved or a counterexample falls out ^[16]. This is also why an interactive prover is the substrate rather than an automatic solver: the interview's account of Z3 is that it succeeded at finding bugs and did not succeed at proving their absence, with heuristics failing or timing out on heavily quantified properties and small changes destabilizing proofs ^[15].

Volume is not the same as trust. On the mathematics side, a formalization of the unit distance conjecture ran to roughly a million lines of Lean and was completed in under two weeks after OpenAI released an informal proof ^[13], an average above 70,000 lines per day ^[14]. Nobody is reading that. What keeps it checkable is that the trusted component is small: a high-performance Lean kernel is about 5,000 lines, and while the shipped kernel is itself unverified, independent kernels exist, including one written in Lean and proved consistent with Lean's semantics ^[11][12]. Lean is also being used as an ordinary language, with an AWS AI accelerator compiler at around 500,000 lines where proofs are a side benefit ^[8].

Two limits on all of the above. It is one interview, with no artifact, no zlib line count, and no compute cost disclosed ^[18]. And the round-trip property, while strong, is not the whole safety story for a decompressor handling hostile input.

What to watch: whether zlib's optimization pass lands without reproving from scratch, since that is the actual test of modularity ^[2][5]; whether anyone ships a spec-as-slow-reference pair in production rather than a test suite ^[6]; and whether costs keep dropping, given that labs only began putting Lean seriously into reinforcement learning pipelines in the last year or two ^[17].