Lean proved the program correct, but bugs were found inside it

Fuzzing the zlib implementation of lean-zip, formally verified with Lean, showed that while the verified application code itself had no memory vulnerabilities, problems surfaced in the Lean 4 runtime and the unverified archive parser.

• Using the AI fuzzer Claude along with AFL++, AddressSanitizer, UBSan, and Valgrind, 16 parallel fuzzers intensively tested 6 attack surfaces.
• Over 105,823,818 executions, 359 seeds, and 19 hours, 4 crashing inputs and 1 memory vulnerability were identified.
• There were two key findings.

1) Heap buffer overflow in the Lean runtime

In lean_alloc_sarray, the calculation sizeof(lean_sarray_object) + elem_size * capacity could cause an integer overflow. When capacity approaches SIZE_MAX, a small buffer gets allocated, and a subsequent large-size read causes a heap overflow.

• This is triggered by passing a very large nbytes to IO.FS.Handle.read.
• It was reproducible with a 156-byte file where the ZIP64 header's compressedSize was 0xFFFFFFFFFFFFFFFF.
• This issue is noted to affect all Lean 4 versions, and a fix PR has already been proposed.

2) Out-of-memory-based DoS in Archive.lean

The archive parser's readExact used the ZIP central directory's compressedSize as-is without validation, attempting an abnormally large memory allocation. This could terminate the process with INTERNAL PANIC: out of memory.

• Reproduced with a 156-byte ZIP claiming a size of several exabytes.
• The system unzip validates such header values, but the corresponding path in lean-zip did not.

What this case clearly demonstrates is this: formal verification is extremely powerful within the scope it verifies, but it does not automatically guarantee code outside the specification or the runtime layer. The compression/decompression algorithm was safe, but unverified parsers and runtime bugs inside the trusted computing base (TCB) could shake the reliability of the overall system.