A few days ago I wrote Lean for People Who Already Write Tests. In it I said I had decided to use Lean on as many of my projects as I could, and that in three days it found real bugs in four of them. I also said I'd write a follow-up when I'd done this for longer than three days. This is that follow-up, sooner than planned, because some of what I said was wrong.
What the first post claimed
The claim was simple. Tests check the cases you thought of. Lean checks a claim about every input. So model the small, hard cores of your code in Lean, prove the rules, and run a differential test to check that the model matches the real code. The bugs were real: a retry counter that never told a human about repeated merge conflicts, a timing bug in my jam tool, and colours that failed their own contrast claims. A day later it also found a login lockout in my site starter: one IP address could lock anyone's email out.
All of that is still true. What I had not done was ask whether something cheaper would have found the same bugs.
A friend asked the right question
A friend, who I won't name, pushed back. Their point was that I was spending a lot of time on an approach that wasn't paying for itself, and that I should check before I spent more. They were right, and I'm grateful. Without that push I would have kept putting Lean on everything.
So I measured it.
What happened when I measured
I took the code from before each fix, with the history removed so the fixes were not visible. For each case I wrote down only the rule, in the words the Lean theorem used, plus the file and function names. No bug, no counterexample, no fix. Then a fresh AI agent ran each case blind with property-based tests: fast-check for TypeScript and proptest for Rust. Property tests generate many random inputs and check that a rule holds for all of them.
They found all four bugs Lean found. They also found a fifth bug that an audit had found, not Lean, and a few extra issues that Lean's models never covered.
The cost was the bigger surprise. Across the four Lean cases, Lean took 40.9 minutes and about 350,000 output tokens. The property tests took 10.2 minutes and about 99,000 tokens for all five cases. That is roughly a quarter of the time, on a cheaper model.
I want to be fair about that comparison, because it isn't clean. Lean ran on a more expensive model, so the price gap is bigger than the token gap. The Lean times include writing fixes and the differential tests. It was five cases, one run each, and I judged the results. And the property tests started from rules that Lean had already made me write down. That last point turns out to be the important one.
Property tests are also samples, not guarantees. The first random run missed the login lockout until it was given a property that hammered one email address. Lean's results are about every input: every 8-bit colour under the exact contrast formula, every tempo above 150 bpm, any attack sequence from one IP address.
What Lean taught me anyway
Lean was not wasted time. It found real bugs in shipped code, and I fixed them.
The bigger lesson is where the bugs came from. In every case, the bug was found by writing the rule down precisely. "However many times it fails, a human is told." "One IP address can never lock someone else out." Once a rule is written that way, both tools can check it. Lean forced me to write rules like that, because it won't accept anything vaguer. That habit is what I'm keeping.
Lean also forced one piece of code into a small pure function so it could be modelled, and the property tests could not reach that logic without it. Making hard logic pure and testable is good for any tool.
Then I tried Dafny
The other weak spot in the first post was the gap between the model and the code. A Lean proof is about a Lean model. The differential test checks that the model and the TypeScript agree, but only on the inputs you generate.
Dafny is a language with proofs built in that compiles to JavaScript. So the proof is about the code that runs. I tried it on the same login throttle from my site starter. It proved that one IP address cannot lock out another user, using a model with real time windows. The proof checked in 1.7 seconds. The compiled functions now run inside the real login code, on a local branch, and the full test suite still passes.
It took about 7 minutes and about 41,000 output tokens. The Lean path on the same case took 23.4 minutes and about 104,000 tokens. That's roughly a third of the cost.
It even found something Lean had missed. The Lean model had no clock. With time in the model, Dafny showed that a code comment about why the email window is fixed gives the wrong reason. The window still matters, but for a different reason.
Dafny has costs. It adds about 14 KB gzipped to the bundle, plus a dependency for big numbers. The build needs Dafny installed. The glue around the proved core, like reading and writing storage, is still unproved, so the old differential test stays. And it is not a fit for everything. For the contrast checker, which is about real numbers, Lean is still the better tool.
How I work now
There are three tiers.
- Every feature with a rule gets property tests, in the same change. This is cheap and it finds the bugs.
- High-stakes TypeScript cores get Dafny. That means auth and permissions, rate limits and lockouts, money, and keeping one user's data away from another's. The core is written in Dafny, compiled to JavaScript and used by the TypeScript. The login throttle is the pattern.
- Lean is for designs and maths that are not shipped code. Music rules, protocol models. This is rare now.
The one-sentence version: the written rule finds the bug. Property tests are the cheap way to check it. Dafny is the way to prove it on code you ship. Lean is for when "never" must be literally true and there is no shipped code to prove.
If you read the first post and installed Lean, keep it. But start with property tests on Monday. Write the rule first, the way Lean would make you, and see what the random inputs find.