Not sure how much people have been following the ongoing cybersecurity apocalypse, but one of the interesting things I’ve learned from it is how exactly teams have been finding exploits. Some of these exploits are found by formalizing software into Lean 4, and then attempting to prove (or refute) rigorously that certain properties are respected. This can identify problems that even the most heavy-handed prop-testing can fail to catch. Before AI coding agents, this would be a huge pain in the ass, because you literally need to write a formal math proof for every single property, but nowadays with the strong math performance of AI, it’s actually possible to do this en masse for software.
I have taken a stab at modelling some of my own packages into Lean, and this has identified TONS of bugs that had gone undiscovered for a while (in DynamicExpressions.jl):
Some of which seem to be problematic correctness bugs that could have been encountered silently. Now, I should also mention that I try very hard to avoid bugs in the first place (this is actually a carefully written, heavily-tested, 100%-human-reviewed codebase, not some AI slop!!) - which I want to point out to emphasize just how powerful Lean formalization is for catching bugs.
The way this works is that each Julia function gets a Lean model, and each docstring promise turns into a theorem which the agents try to prove. When any proof fails, the counterexample is usually a bug, which then gets checked against real Julia.
I have now, also, taken a stab at doing this for Julia itself - formalizing the full source code in Lean. This has also been quite fruitful: so far this has found about 400 (!) bugs in Base. I have filed 75 of the ones I manually filtered: these are the ones I thought were worth a maintainer’s time, after checking each against existing issues and PRs for duplicates. Again I should emphasise that this does not mean Base is buggy relative to most software, it just means that Lean formalization is a very powerful way to catch bugs!
Anyways, I thought it might be useful for others to see how this all worked, and potentially use it themselves, so I put together a repository with a writeup, and all of the Lean code I used for these:
GitHub - MilesCranmer/julia-in-lean: Notes on modelling Julia in Lean · GitHub.
I discuss this more below.
What one of these looks like
Here is a real issue, filed as #64124. Julia reverses an ordinal range by rebuilding it with the negated step:
_reverse(r::OrdinalRange, ::Colon) = (:)(last(r), negate(step(r)), first(r))
The Lean version mirrors that line, with Julia’s fixed-width integer arithmetic:
def reverse (r : Rng) : Jl Rng := do
let st ← Num.negate (step r)
colon3 (last r) st (first r)
The property, from the reverse docstring: reversing a range that Julia successfully constructed keeps the same number of elements.
def reverseCardinalityProp : Prop :=
∀ (a st b : Num) (r : Rng), stepRange a st b = .ok r →
match reverse r with
| .ok out => trueCount out = trueCount r
| .error _ => False
This property can’t be proven, because it is false. The counterexample the agent found is Int8(0):typemin(Int8):typemin(Int8), which has two elements. Negating a step of -128 wraps back around to -128, so the reversed range goes from -128 “down” to 0, which is empty:
julia> r = Int8(0):typemin(Int8):typemin(Int8)
0:-128:-128
julia> length(r), length(reverse(r))
(2, 0)
The same wraparound makes sort return an empty range for some inputs, since sorting a descending range calls reverse.
Many of the bugs look like that: an edge case at typemin, an empty collection, an unsigned type. (Some of which would be hard to run into in typical use). But some are nastier:
- #64183: a miscompilation on master, where inference folds an
isacheck across loop iterations and a small loop returns the wrong answer. This one showed up becauseMarkdown.rststarted printing the wrong thing. - #64147: resizing
vec(M)of aBitArraycorruptsM, since the two share storage. - #64185:
@sprintfof a largeBigFloatafter other output writes past the end of Printf’s output buffer. - #64193: an artifact path lookup can reach outside the artifact directory.
How it works
Each Julia function gets a Lean definition that follows the source line by line: same branches, same order of checks, same integer wraparound. Exceptions become values (Except JlError α, where JlError lists Julia’s exception types). Then each property gets stated as a Lean Prop taken from a docstring, the manual, or an obvious invariant. Each property has to quantify over the space of all inputs.
The main problem with letting agents do formal work is that they are good at producing things that look like proofs. So most of the setup checks them:
- Differential testing first. Before proving anything, the Lean model is run on lots of inputs and compared against real Julia. For example, the integer core matched an exhaustive table of all 656,896 Int8/UInt8 cases, and the Float64 model matched on 236,954 operations. If the model disagrees with Julia, the model is wrong.
- An audit of the build. The build fails unless every property is proven or refuted, each theorem has exactly the type of its property (or the negation), and no proof uses
sorry,native_decide, or extra axioms. A separate check rejects statements that only test worked examples. - A refutation only counts with a reproducer. A Lean counterexample by itself is just a claim about the model. It only counts once a plain Julia script shows the same behavior on the real thing.
- Duplicate search. Before anything is written up, the agent searches existing issues and PRs. A lot of what it finds is already known, for example #58245.
Even with all these checks, the agents can cut corners. When I moved on to proving that every @inbounds and unsafe_* access in base/ stays in bounds (1,152 sites), the first pass came back with 130 “proven” sites in under an hour. That seemed too fast… and indeed it was: a review against a fixed rubric found that 128 of those 130 proofs had just assumed the index was in bounds. The audit can’t catch that, since the theorem is technically valid. So now every proof there has to pass that review too. (The memory-safety proofs are still unfinished.)
Models and cost
Everything so far has cost about $5,000 in API-equivalent usage, mostly Claude Opus 5.5 and OpenAI’s Daybreak Blue (via Codex). Regular models kept refusing parts of the task, since “find overflow bugs in this source code” trips their cybersecurity filter. Daybreak Blue is meant for authorized security work, so it is less likely to refuse it (you can sign up at https://chatgpt.com/cyber)
Reporting
When I asked on Slack how to report these, the advice was one issue per bug rather than a single tracking issue, so that is what I do, and only for the bugs that are (1) new and (2) plausible to hit in real code. (A few people there also asked how I was finding them, which is why I wrote this up.)
I worked hard to avoid duplicates. The agent searches open and closed issues and PRs before writing anything up, and records every search. Before an issue goes up, the agent searches again, and I push back whenever something looks familiar. Many of the bugs are already known, some with a fix PR open, and I never post those. I read every issue before it goes up. The issues come from @MilesCranmerBot, which is also me (I split my GitHub activity by whether an AI wrote the text, so the provenance is easier to follow). And then any bug that might be exploitable goes to security@julialang.org instead.
All of the bugs are in the repo, including the ones I didn’t post, as YAML files with a priority, the reproducer, and the output on Julia 1.13.2 and master: julia-in-lean/julia-base/bugs at main · MilesCranmer/julia-in-lean · GitHub. Most of these have not yet been reported because they are too much of an edge-case. For example, stuff like: wrong exception types, hard-to-reach edge cases, docs that contradict the code. (A handful of security-relevant ones are held back for now.)
Caveats
“Proven” means proven about the Lean model. But inevitably this model is also written by agents and checked against Julia by differential testing, not generated from Julia automatically, so a proof is only as good as the model. The bugs do not have this problem: every one has a reproducer on real Julia. Coverage is partial: parts of about 90 files in base/ plus some stdlib packages. I have also started on the C runtime (the GC, etc.). It is only about 10% done, so it is not in the repo yet.
Trying it on your own package
The repo has the DynamicExpressions.jl model as a template. I would recommend starting with one small central module, set up the differential test and the audit, and only then let agents prove things. Also, good to write down the ambiguous cases, since some “bugs” are intended behavior. When a fix is written, your agent can update the model to the new source: the same statement should now be provable, and proving it acts like a check.
Interested to hear what people think!