Lean proved this program correct; then I found a bug

Original Article ↗ Hacker News Discussion ↗

Formal verification with the Lean theorem prover is showcased on a port of the zlib compression library, but fuzzing guided by an AI agent uncovers bugs in the surrounding archive parser and Lean’s own runtime. Commenters use this to highlight a core limitation of formal methods: proofs only guarantee correctness relative to the parts of the system and specifications they actually cover, leaving unverified runtimes, parsers, specs, and even hardware as potential sources of failure. Many still see the result as a win for verification and AI-assisted tooling, arguing it shifts bugs into narrower, more scrutinizable parts of the stack rather than eliminating them outright.

What actually went wrong

  • The verified part was the core zlib compression/decompression logic in Lean.
  • Two bugs surfaced:
    • A denial-of-service via unverified archive-header parsing in the Lean-zip code.
    • A heap buffer overflow in the Lean runtime’s scalar array support, affecting any Lean program using that feature.
  • Both issues were outside the formal proof’s stated scope, so the core correctness proof was not invalidated.

Limits of formal verification

  • Multiple comments stress: proofs are always “correct with respect to a specification,” not to human intent or the full system.
  • Common failure modes:
    • Spec bugs (the spec doesn’t capture what was really wanted).
    • Spec gaps (important behaviors like parsers, resource limits, or adversarial inputs not modeled).
    • Unverified layers (runtime, OS, hardware, compilers).
  • Some argue a “verified system” should be understood as the whole binary stack; others say that’s unrealistic unless every component is verified.

Trust in verification tools

  • Concern: why trust the verifier more than the verified code?
  • Replies: verifiers can be simpler, heavily scrutinized, and used by many, making serious undetected bugs less likely (though not impossible).
  • Distinction emphasized between Lean’s kernel (logic/proofs) and runtime (execution/FFI); a runtime bug doesn’t directly falsify existing mathematical proofs.

Spec correctness and completeness

  • Discussion about needing methods to “verify the specs” themselves, including adversarial thinking and high-level property proofs.
  • Recognized gap between:
    • Implementation soundness (“the code does X”) and
    • Design soundness (“doing X is actually the right, safe thing”).
  • Compression is highlighted as a good domain: simple correctness spec, complex implementation, but still vulnerable to unmodeled behaviors (e.g., malformed inputs).

AI, fuzzing, and “vibe-coded” proofs

  • Several commenters report success using LLMs to help write proofs and models (Lean, TLA+, etc.).
  • The AI-assisted fuzzing that found the Lean runtime overflow is seen as a significant, positive result.
  • Enthusiasm that combining AI, fuzzing, and formal methods can narrow where bugs hide, even if perfection remains impossible.

Title and framing debate

  • Many see the article title as misleading or clickbait, implying a flaw in the proof itself.
  • Others defend it as fair from an end-user perspective: if the binary crashes or is exploitable, the “verified program” is still buggy in practice.