Lean proved this program correct, but a bug was found anyway

We fuzzed lean-zip with a Claude agent to check whether real flaws could still surface in a verified Lean implementation.

The target was a trimmed-down version of the lean-zip codebase. During cleanup, theorems, specifications, documentation, and the zlib implementation linked via C FFI were removed, leaving only the core DEFLATE, gzip, ZIP, and tar code written in Lean.

Running 16 parallel fuzzers for 19 hours produced 105,823,818 executions, and as a result:

• No memory vulnerabilities were found in the application code.
• A heap buffer overflow was found in lean_alloc_sarray in the Lean 4 runtime.
• A denial-of-service was confirmed in the unverified archive parser.

The most significant vulnerability was lean_alloc_sarray in the Lean runtime. When allocating a scalar array such as a ByteArray, the capacity calculation could overflow, actually allocating a small buffer of about 23 bytes, after which a read of size SIZE_MAX could follow. A minimal reproduction was presented via IO.FS.Handle.read, passing n = SIZE_MAX to h.read n. This issue affects all versions of Lean 4, and a patch PR has been submitted.

The second issue was in the ZIP parser in Archive.lean. It passed the compressedSize value from the central directory to h.read without validation, so even a very small ZIP file declaring an abnormally large size could lead to an out of memory panic. The system unzip prevents this by cross-checking the file size against the header, but lean-zip did not.

The reason verification failed to catch these was clear.

• The ZIP archive parser was never subject to proof in the first place.
• The runtime bug lay outside the proof, in the trusted computing base.

In conclusion, the verified Lean code itself was remarkably robust even under 105M fuzzing runs, and both issues found lay outside the scope of the proof. Verification is powerful, but it's only complete when it also covers what is specified and what is trusted.