Lean formalization of Julia Base surfaces hundreds of bugs

Miles Cranmer has begun formalizing Julia’s Base library in Lean 4, turning function behavior and docstring promises into theorems that automated provers attempt to discharge. Failed proofs yield counterexamples that are checked against real Julia; so far the effort has produced roughly 400 candidate bugs, of which he has filed 75 after manual filtering for novelty and maintainer value.

The work does not claim Base is unusually buggy relative to other large codebases. Instead it argues that machine-checked proofs catch classes of defects (silent wrong results, overflow at type extremes, empty-range edge cases, mismatched exception types) that heavy property testing can miss. Cranmer previously applied the same pipeline to his own packages, including DynamicExpressions.jl, and reported many previously unnoticed correctness issues there as well.

Coverage so far focuses on concrete Base types whose methods are fully defined in Julia source (machine integers, floats, ranges, Dict, String, and similar) together with selected standard-library pieces. The C runtime and compiler remain early. Generic code is handled by parameterizing Lean models on the properties required of user methods; theorems then state those assumptions explicitly rather than attempting proofs about vague abstract interfaces such as Number or AbstractArray. When a docstring’s contract is unclear, findings are tagged as possibly intended rather than filed as definitive bugs.

Cranmer attributes the scale of the effort to recent AI systems strong enough to generate and discharge large numbers of Lean proofs, something previously impractical by hand. The public repository already contains modeled fragments of Base; broader formalization continues locally.