My invariant test passed on the first try. Two hundred and fifty-six runs, depth 32, 8,192 calls into the protocol, zero failures, zero reverts.
In a report that line looks like proof. It was not proof. The bug was sitting in the code the whole time, and my test had never once walked past it.
This post is about the number I was not printing.
The setup
The target was a constant-product AMM — a Uniswap V1 clone. Two tokens in a pool, x * y = k, a 0.3% fee that stays behind. The kind of contract where "did anything leave that should not have" is the only question worth asking.
I did the responsible thing and wrote a stateful fuzz test with a handler, because pointing a fuzzer straight at the contract is theatre: it feeds garbage into arguments, ninety-nine percent of calls die on a require, and the fuzzer never gets deep enough into state to find anything. A handler is a facade of legal moves. Each method is something a real user could actually do, with bound() turning a random number into a sensible one.
Then I wrote the invariant. And here is the part I would keep even if you take nothing else from this post.
Do not re-implement the math you are testing
The obvious invariant for an AMM is x * y == k. It is also useless. The fee makes k grow legitimately, so equality gives you false alarms and any inequality loose enough to survive the fee is too loose to catch a thief.
The version that works is causal:
Every change in reserves must match what the protocol's own pricing function predicted.
I do not recompute AMM math myself — that is just a second chance to be wrong in the same direction. I catch the contract on its own word:
// before the action: what the contract's own math promised
expectedDeltaWeth = -1 * int256(outputWeth);
expectedDeltaPoolToken = int256(pool.getInputAmountBasedOnOutput(...));
// ... the action happens ...
// after: what the balances actually did
actualDeltaWeth = int256(weth.balanceOf(address(pool))) - int256(startingWeth);
And the invariant is one line:
assertEq(actualDeltaWeth, expectedDeltaWeth, "WETH left the pool without pricing math");
The strength of this phrasing is that it does not know, and must not know, how the tokens left. A gift, a fee, a backdoor, a typo in next quarter's feature — anything that moves value without pricing math behind it breaks the same assert. One line closes an entire class.
So: good invariant, proper handler, green run. I was ready to write "no violations found."
The denominator
Almost as an afterthought, I had left counters in the handler. Not for the test — for me, to see what the fuzzer was actually doing. After the green run I printed them:
deposits: 15
swaps: 3
Three.
Out of roughly sixteen attempted swaps per run, three reached the pool. The rest hit my own guard clause and returned early. I had bounded the requested output as bound(outputWeth, minWeth, wethReserves - 1), and near the top of that range the required input overflowed uint64, so my guard bailed out before ever calling the pool.
The bug in that protocol triggers roughly every tenth swap.
Three swaps per run cannot reach a one-in-ten event with any reliability. The test was not green because the protocol was sound. The test was green because it was barely doing anything.
I narrowed the bound to wethReserves / 10 and raised depth to 64. It failed on the first run:
Error: WETH left the pool without pricing math
Left: -1000000001000000000
Right: -1000000000
That extra 1e18 is an incentive payout the contract hands out on every tenth swap, straight out of the pool's reserves, with no pricing math behind it. The invariant caught it the moment the fuzzer was allowed to get there.
Same contract. Same invariant. Same tooling. The only thing that changed was whether my test could reach the thing it was testing.
Why this is the dangerous failure mode
A test that fails wrongly costs you an afternoon. You investigate, you find the mistake, you move on. Annoying, self-correcting.
A test that passes wrongly costs you the audit. Nobody investigates a green check. It ends up in a report as "invariant testing performed, no violations found," and it is worse than having written no test at all, because now there is a piece of paper telling everyone not to look there.
That asymmetry is the whole reason to care about denominators. Coverage tools will not save you either: line coverage said my handler was covered. It was. Covered lines are not reached states.
The two numbers I now require
Before I believe any green invariant run, I print two things:
- How many times each interesting action actually completed — not how many times it was attempted. Attempts are the fuzzer's business. Completions are the test's.
- Whether that count is enough to reach the rarest event in the system. If the protocol does something unusual every tenth swap and my run produces three swaps, the run has not tested that path. It has tested my guard clauses.
Both numbers go in the report, next to the result. "256 runs × depth 64, 1,914 completed swaps, 0 violations" is a finding. "0 violations" on its own is a decoration.
And there is a companion habit that costs nothing: run the suite against a deliberately broken build. Introduce the bug you are most afraid of, confirm the suite goes red, then remove it. A test that has never failed has never been shown to be capable of failing. If your CI has been green since the day it was written, that is not evidence of quality — it is an untested claim about your tests.
The general shape
This is not really about Solidity. Every fuzzer, property test and simulation harness has the same failure mode: the guard clauses you wrote to keep the generator sensible quietly become the walls of a very small room, and then you measure the room instead of the building.
The question to ask of any passing test, in any language:
Could this test have failed, for the reason I am afraid of?
If you cannot answer that with a number, you do not have a result yet. You have a colour.

Top comments (0)