Lean proved this program correct; then I found a bug

Lean proved this program was correct; then I found a bug.

lean formal_verification security fuzzing

I fuzzed a verified implementation of zlib and found a buffer overflow in the Lean runtime. AI agents are getting very good at finding vulnerabilities in large-scale software systems.

Anthropic, was apparently so spooked by the vulnerability-discovery capabilities of Mythos, they decided not to release it as it was "too dangerous" (lol). Whether you believe the hype about these latest models or not, it seems undeniable that the writing is on the wall: The cost of discovering security bugs is collapsing, and the vast majority of software running today was never built to withstand that kind of scrutiny.

We are facing a looming software crisis. In the face of this oncoming tsunami, recently there has been increasing interest in formal verification as a solution. If we state and prove properties about our code using a mechanical tool, can we build robust, secure and stable software that can overcome this oncoming barrage of attacks?

One recent development in the Lean ecosystem has taken steps towards this question. 10 agents autonomously built and proved an implementation of zlib, lean-zip, an impressive landmark result. Quoting from Leo De Moura, the chief architect of the Lean FRO: the key result is that lean-zip is not just another implementation of zlib. It is an implementation that has been verified as correct end to end, guaranteed by Lean to be entirely free of implementation bugs.

What does "verified as correct" actually look like? Here is one of the main theorems:

theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
(hsize : data.size < 1024 * 1024 * 1024) :
ZlibDecode.decompressSingle
(ZlibEncode.compress data level) = .ok data

For any byte array less than 1 gigabyte, calling ZlibDecode.decompressSingle on the output of ZlibEncode.compress produces the original data. The decompress function is exactly the inverse of compression. This pair of functions is entirely correct. Or is it?

I pointed a Claude agent at lean-zip over a weekend, armed with AFL++, AddressSanitizer, Valgrind, and UBSan. Over 105 million fuzzing executions, it found:

• Zero memory vulnerabilities in the verified Lean application code.
• A heap buffer overflow in the Lean 4 runtime (lean_alloc_sarray), affecting every version of Lean to date.
• A denial-of-service in lean-zip's archive parser, which was never verified.

The setup

The setup for the experiment was quite simple. I took the lean-zip codebase and produced a stripped down version and pointed Claude at it. In particular: (1) I dropped all theorems and specifications, (2) removed all markdown documentation, and (3) stripped out lean-zip's C FFI bindings. What remained was purely the verified code. The idea with dropping theorems was to avoid biasing the Claude agent – I figured if it knew the code "had no bugs" then it might pre-emptively give up.

Results

Over the course of a night, Claude launched 16 parallel fuzzers across the 6 attack surfaces. This resulted in 105,823,818 fuzzing executions, uncovering 4 crashing inputs, and 1 memory vulnerability in the code.

Bug 1: Heap buffer overflow in the Lean runtime

The most substantial finding was a heap buffer overflow in the Lean runtime itself, specifically in lean_alloc_sarray, which allocates all scalar arrays. For a ByteArray of capacity n, the allocation size is 24 + n. When n is close to SIZE_MAX, the addition wraps around to a small number. The runtime allocates a tiny buffer, but the caller proceeds to read n bytes into it. A 156-byte crafted ZIP file is sufficient to trigger it. The bug affects every version of Lean 4 up to the latest nightly.

Bug 2: Denial-of-service in the archive parser

AFL also found a DoS in lean-zip's own code. The readExact function passes the compressedSize field from the ZIP header straight to h.read without validating it. A ZIP claiming a compressedSize of several exabytes causes the process to panic with an out-of-memory error.

Why verification didn't catch these bugs

The OOM DoS is straightforward: the archive parser was never verified. Verification works where it is applied. The heap buffer overflow is more fundamental. lean_alloc_sarray is part of the trusted computing base. Every Lean proof assumes the runtime is correct. A bug here undermines the entire system's safety guarantees.