back

Rick ·

How do I write useful invariant tests in Foundry?

Dev tooling

I wrote one constant-product pool, six one-line defects, and eight invariant setups that differ only in how the calls are generated and what is asserted. Then I ran all of them, five seeds each, twice — and the two cells that did not come back the same, many more times than that.

The setup with no targetContract call failed on the pool as written in 38 of 45 campaigns. Its counterexample was the pool sending its own tokens away.

The four setups with a proper target and progressively better handlers — raw arguments, vm.assume, bound — found exactly the same two defects out of six. Making the handler better moved that number by nothing.

The three setups that found all six were those same handlers with two more properties attached. Thirty-three lines including the comments, none of which changed how a single call is generated.

So the useful version of the question is not how to write a handler. The handler is not what finds the bug; it is what lets you write the property that finds the bug. Most of what gets argued about in handlers — bound against vm.assume, revert rates, call distribution — turns out to be about making a campaign readable rather than about making it find more.

The pool and the six defects

The contract is the smallest thing that still behaves like an automated market maker: two ERC-20s, one reserve each, proportional shares, a 0.3% swap fee, a permanently locked minimum liquidity, and a permissionless skim that sweeps anything sitting above the recorded reserves. 130 lines, 101 of them code. Four entry points that move tokens.

Then six deliberate defects, each one string replacement in the source, applied one at a time:

The change
D1 swap adds the fee instead of subtracting it
D2 addLiquidity mints on the larger side of an unbalanced deposit instead of the smaller
D3 skim treats the whole token0 balance as excess
D4 removeLiquidity burns the holder's shares but not the supply
D5 swap forgets to reduce the outgoing reserve
D6 removeLiquidity rounds the payout up

Everything runs on Foundry's defaults: 256 runs at a depth of 500, so 128,000 generated calls per invariant function, with fail_on_revert off. The numbers are from Foundry 1.5.1 with solc 0.8.36, the optimizer at 200 runs, forge-std 1.16.2, on an Apple M3 Pro. The pool, the eight setups, the harness and the raw results are in the repository under examples/articles/how-do-i-write-useful-invariant-tests-in-foundry.

Point it at everything and it reports a bug you do not have

The first setup does what the Foundry guide's basic example does minus one line: it deploys the pool, asserts two properties, and never calls targetContract.

function invariant_solvency() public view {
    assertGe(token0.balanceOf(address(pair)), pair.reserve0(), "token0 balance below reserve0");
    assertGe(token1.balanceOf(address(pair)), pair.reserve1(), "token1 balance below reserve1");
}

On the pool as written, that fails:

[FAIL: token0 balance below reserve0: 999999999997766374272 < 1000000000000000000000]
	[Sequence] (original: 172, shrunk: 1)
		sender=0xF62849F9A0B5Bf2913b396098F7c7019b51A820a
		addr=[src/MockERC20.sol:MockERC20]0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f
		calldata=transfer(address,uint256) args=[0x17f63AeB064b64f8a91AB6A202eaeC7aAfEF12d2, 2233625728 [2.233e9]]

Read the addresses. 0xF628… is the pool. 0x5615… is token0. The runner called token0.transfer with the pool as the sender, moved 2.23 gwei out of the pool's own balance, and correctly observed that the pool's balance was now below its reserve.

With no targets declared, Forge fuzzes every contract the setup deployed — here, the two mock tokens as well as the pool — and it draws senders from its fuzz dictionary, which contains the pool's own address. So the campaign is allowed to impersonate the contract under test and spend its balance, which nothing in the pool's own code would ever do.

That last part is checkable rather than folklore. Running the same setup 15 times per configuration: under the defaults the false failure landed in 10 of 15 campaigns; at dictionary_weight = 0, which stops the runner drawing from the dictionary at all, it disappeared completely, 0 of 15. Setting include_storage = false, the knob I had expected to be responsible, did not help — it landed in 15 of 15.

Pooling every campaign I ran against the pool as written under the defaults, the untargeted setup reported a bug that was not there in 38 of 45, and no seed pinned the verdict: the five seeds scored 6, 7, 9, 9 and 7 out of 9 identical repetitions each. A test that reports a bug most of the time on correct code is worse than no test, and the entire column for that setup — six of six defects "caught" — is worthless, because I cannot tell a real catch from the noise.

targetContract is not a tidiness setting. It is what makes the counterexample mean something.

What a handler is actually for

The four remaining pool-only setups add, in order: targetContract(address(pair)); a handler that fixes the caller but passes the fuzzer's raw 256-bit words straight through; the same handler with vm.assume rejecting the illegal inputs; and the same handler with every argument mapped into a legal range with bound.

Here is what that ladder does to the campaign.

Two panels. Left: horizontal stacked bars showing what one 128,000-call campaign did in each of five setups, as the median of five seeds. With no targeting, 41.5% of calls landed and the rest reverted. With the pool targeted directly, 35.2% landed. With a handler passing raw arguments, 49.5% landed. With a handler using vm.assume, 88.3% of the accepted calls landed, 15,031 reverted, and a further 103,411 generated inputs were discarded before acceptance, for 231,411 inputs in total. With a handler using bound, 100.0% landed and nothing reverted. Right: a bar chart of how many of six deliberate defects each setup caught. The pool targeted directly caught 2. The raw-argument handler caught 2 on every seed plus 1 on some seeds. The vm.assume handler caught the same 2 plus 1. The bound handler caught 2. Adding two properties that track state raised the raw-argument, vm.assume and bound handlers to 6 of 6 on every seed.

Left: what each campaign executed, median of five seeds on the pool as written. Right: defects caught, with and without the two properties that read state the pool does not keep.

The left panel is what the guides are about, and it is real. Pointing the runner at the pool directly, 35.2% of calls landed and the rest reverted, because a randomly generated sender holds no tokens, has approved nothing, and owns no shares. A handler that picks one of three funded, approving actors takes that to 49.5%. Bounding every argument takes it to 100%: zero reverts in 128,000 calls, on every seed.

The right panel is the part they mostly skip. Across those four setups, the number of defects found went 2, 2, 2, 2.

bound, vm.assume, and the calls that never happen

The two filtering approaches look similar in a handler and behave nothing alike.

vm.assume rejects the generated input and asks for another one. The rejected attempt is not a call; Forge counts it in a separate column and the run's budget is untouched.

function swap(uint256 actorSeed, bool zeroForOne, uint256 amountIn) external record("swap") {
    address actor = _actor(actorSeed);
    MockERC20 tokenIn = zeroForOne ? token0 : token1;
    vm.assume(amountIn > 0 && amountIn <= tokenIn.balanceOf(actor));
    vm.prank(actor);
    pair.swap(zeroForOne, amountIn);
}

bound maps the input into range instead, so every generated word becomes a legal call.

function swap(uint256 actorSeed, bool zeroForOne, uint256 amountIn) external record("swap") {
    address actor = _actor(actorSeed);
    MockERC20 tokenIn = zeroForOne ? token0 : token1;
    uint256 reserveIn = zeroForOne ? pair.reserve0() : pair.reserve1();
    // A trade larger than the reserve it pays into is not a trade.
    uint256 cap = _min(_min(tokenIn.balanceOf(actor), MAX_AMOUNT), reserveIn);
    if (cap < MIN_AMOUNT) return _decline("swap");

    amountIn = bound(amountIn, MIN_AMOUNT, cap);

    vm.prank(actor);
    pair.swap(zeroForOne, amountIn);
}

Foundry's own best-practices table says to use bound() instead of vm.assume(), and the measurement supports it on cost. To execute its 128,000 calls one recorded vm.assume campaign generated 230,549 inputs and threw 102,549 of them away — 44% of everything it produced — and it still ended with 14,977 reverts, because assuming the amount fits in a balance does not make the resulting deposit mint a share. It took 9.6 seconds against 5.5 for the raw handler.

It never came close to failing, though, and it is worth knowing why. max_assume_rejects defaults to 65,536 and is documented as "the maximum number of rejects via vm.assume which can be encountered during a single invariant run". Per run, not per campaign. 102,549 rejects over 256 runs is about 400 each. A handler that rejects hard enough to break that limit has to be rejecting more than 99.9% of what it is given.

The better argument against vm.assume is not cost. It is that a rejection rate tells you nothing about what was rejected: from a green campaign you cannot tell whether you threw away the uninteresting half of the input space or the interesting half. bound makes the same decision in code you can read line by line.

bound also is not a clamp. Reading forge-std's implementation, a value already inside the range is returned unchanged, 0 through 3 map to the bottom of the range, the top four uint256 values map to the top, and everything else wraps modularly. That matters because the fuzzer's dictionary deliberately feeds boundary values and addresses it found in storage; a clamp would flatten all of them onto one endpoint.

And the third case, the one neither keyword covers: the handler declining. Four of my five entry points start with a guard that returns early when the chosen actor cannot legally do anything — no shares to burn, no balance to deposit. That call did not revert and was not discarded. Forge counts it as a successful call. It did nothing.

Reverts are the number to watch

With fail_on_revert off — the default, in Foundry and in Hardhat 3, which mirrors the same defaults down to runs = 256 and depth = 500 — a reverting call is discarded and the sequence continues. That is the right default for a fuzzing campaign and a terrible default for reading one, because a suite where two thirds of the calls revert is green for the same reason an empty suite is green.

My bounded handler looked finished. Across its four campaigns it reverted 19, 21, 32 and 54 times per 128,000 calls, which reads as rounding error. Setting fail_on_revert = true turned that into a failure shrunk to three calls, and the trace of the last one was:

[48993] HandlerBoundUnguarded::addLiquidity(3, 1, 1540)
    ├─ [2317] Pair::totalSupply() [staticcall]
    │   └─ ← [Return] 500000001001 [5e11]
    ├─ [2360] Pair::reserve0() [staticcall]
    │   └─ ← [Return] 812422441870372002971578 [8.124e23]
    ├─ [0] VM::prank(alice: [0x328809Bc894f92807417D2dAD6b7C998c1aFdac6])
    ├─ [1090] Pair::addLiquidity(1000000000001 [1e12], 999999999999000000001541 [9.999e23])
    │   └─ ← [Revert] ZeroAmount()

A large withdrawal followed by a lopsided swap had left the pool with 8.12e23 of token0 against a supply of 5e11 shares, so one share was worth about 1.6e12 wei on that side — more than my handler's minimum deposit of 1e12. The deposit rounded down to zero shares and reverted. I had picked the floor out of the air, and for most of the campaign it was fine.

The fix adds three lines and rewrites the three that used the constant, and it changes the bound from a number I chose to a number the pool determines:

uint256 supply = pair.totalSupply();
uint256 floor0 = _max(MIN_AMOUNT, _ceilDiv(pair.reserve0(), supply));
uint256 floor1 = _max(MIN_AMOUNT, _ceilDiv(pair.reserve1(), supply));

Afterwards the same campaign runs to completion with fail_on_revert = true and zero reverts in 128,000 calls. That setting is not a mode you leave on; it is a check you run to find out whether the handler you wrote is the handler you think you wrote.

The call summary is one run, not the campaign

The standard way to see what a campaign did is the call summary from Foundry's guide: count calls in the handler, expose a callSummary(), and log it from an invariant function. Mine prints this at the default depth of 500:

handler calls: entered / declined
  addLiquidity 95 0
  removeLiquidity 112 4
  swap 110 0
  donate 91 0
  skim 92 0
  total 500 4

500, against a campaign of 128,000 calls. Set depth to 37 and the total becomes 37. The counters describe one run, not the campaign, because each run restarts from the state setUp left behind and the handler's storage goes back with it.

That is not a reason to skip the counters — the declined column is the only place a silently skipped call shows up at all — but they belong in afterInvariant(), which Forge calls once per run against its final state. A per-run budget assertion is a property of the handler and can be asserted like one:

function afterInvariant() public view {
    uint256 total = handler.entered("total");
    assertGt(total, 0, "the handler was never called");
    assertLe(handler.declined("total") * 20, total, "more than 5% of the run was declined");
    for (uint256 i = 0; i < 5; i++) {
        assertGt(handler.entered(handler.names(i)), 0, "an entry point was never called");
    }
}

For the campaign-wide view, Forge already prints one. show_metrics defaults to true, and the table under each result gives calls, reverts and discards per selector:

╭---------------+-----------------+-------+---------+----------╮
| Contract      | Selector        | Calls | Reverts | Discards |
+==============================================================+
| HandlerAssume | addLiquidity    | 46047 | 10062   | 29794    |
| HandlerAssume | donate          | 46316 | 0       | 21433    |
| HandlerAssume | removeLiquidity | 46067 | 778     | 30148    |
| HandlerAssume | skim            | 46177 | 0       | 0        |
| HandlerAssume | swap            | 45942 | 4137    | 21174    |
╰---------------+-----------------+-------+---------+----------╯

Calls counts attempts, so the column sums to 230,549 against a campaign budget of 128,000, and Calls − Reverts − Discards is what actually executed.

The properties are the whole experiment

The two properties every setup so far asserted are properties of the pool's own storage: its balances cover its reserves, and shares are never outstanding against nothing. They are worth writing. They caught D3 and D5 on every seed and in every setup, including the one with no handler at all, because both defects break the pool's storage on the call that introduces them.

They cannot catch the other four, and no amount of handler work changes that, because the facts those defects break are not in the pool's storage. A constant-product pool does not record what a share was worth a moment ago and cannot enumerate who holds one. Both of those live in the handler, because the handler is what chose the actors and what sits between the runner and every call.

modifier record(string memory name) {
    entered[name]++;
    entered["total"]++;
    shareValueBefore = shareValue();
    _;
}

/// @notice Reserve product per share squared: what stands behind one share.
///         Swaps raise it through the fee, proportional deposits and
///         withdrawals leave it where it is, and nothing should lower it.
function shareValue() public view returns (uint256) {
    uint256 supply = pair.totalSupply();
    if (supply == 0) return 0;
    return (pair.reserve0() * pair.reserve1() * 1e18) / (supply * supply);
}
function invariant_sharesAddUp() public view {
    assertEq(pair.totalSupply(), coreHandler.sumOfShares(), "totalSupply is not the sum of the shares");
}

function invariant_shareValueNeverFalls() public view {
    assertGe(coreHandler.shareValue(), coreHandler.shareValueBefore(), "one share is worth less than it was");
}

Thirty-three lines including the comments and the sumOfShares helper the first one reads. With them, the same three handlers went from two of six to six of six, on all five seeds:

Defect Two pool-only properties Plus the two that track state
D1 fee added instead of subtracted missed caught, share value
D2 mints on the larger side missed caught, share value
D3 skim sweeps the reserve caught, solvency caught, solvency
D4 supply not burned missed caught, share value and share sum
D5 outgoing reserve not reduced caught, solvency caught, solvency
D6 payout rounded up missed in 69 of 80 campaigns caught, share value

What makes shareValueNeverFalls the property that did most of the work is not that it is clever. It is that it is the pool's promise to the people holding shares, stated without reference to how the pool computes anything. reserve0 * reserve1 / totalSupply² never falls is a sentence a liquidity provider would recognise. It happens to be violated by a wrong fee direction, by a wrong min, by a supply that is not burned and by a payout that rounds the wrong way, none of which I was thinking about when I wrote it.

The counter-example is sharesAddUp, which I wrote because it seemed obviously true and which caught exactly one defect, alongside the property that would have caught it anyway. Properties derived from what the code does tend to agree with the code. Properties derived from what the system promises do not.

Where bounding did change the answer

One cell in that table is not unanimous, and it goes the wrong way for the tidy conclusion.

D6 rounds the withdrawal payout up. With the two pool-only properties it is the only defect that is not all-or-nothing, so I ran that row twenty times per setup rather than five. The bounded handler never caught it: 0 of 20. The three handlers that do not bound their withdrawals caught it 11 times in 60 — the pool targeted directly once, the raw-argument handler three times, the vm.assume handler seven — always through sharesAreBacked, the property that says shares cannot be outstanding against an empty reserve.

The reason is my removeLiquidity bound. It refuses to propose a withdrawal small enough that the pool would owe zero of one token, which is a legal-call guard and also a floor on how far it will drain the pool. The sloppier handlers propose those withdrawals, most of them revert, and occasionally one lands in exactly the state where rounding up empties a reserve completely.

So bounding did cost a detection here. It bought a campaign with zero reverts, a fail_on_revert = true guarantee, and a metrics table I can read — and it gave up a path that a handler proposing illegal calls stumbles into about one campaign in six. That is a trade I would still make, because the property that catches D6 every time and on every handler costs four lines. But "constrain the inputs" and "explore the state space" are the same dial, and the bound you write is the specification of what you are searching.

There is a reason those counts are out of twenty and eighty rather than five. I ran the full 280-campaign matrix twice at the same five seeds — one test file picked up an unrelated environment guard in between — and 260 verdicts came back identical. Every one of the 18 that flipped was in the untargeted setup or on D6, the two cells that are marginal by construction. Nothing that was unanimous on the first pass moved on the second.

That is worth saying plainly, because --fuzz-seed looks like it should settle it: a fixed seed does not pin an invariant verdict. The repetitions above are on byte-identical code with the same seed, and the same seed both passed and failed. It is not a large effect — it only reaches the campaigns that were close to the edge — but "close to the edge" is exactly where a defect that your properties barely reach lives. If a defect is found on one run out of six, one run is not evidence either way.

Having found one handler decision that mattered, I went looking for more. With the four properties in place I varied the actor list from three down to one, and the per-call size limit from 1e24 down to 1e18 and up to 1e27: three more handler configurations, a control and six defects each, three seeds apiece, 63 campaigns. Every configuration caught all six defects on every seed, and none of them reported a false failure on the pool as written. Whether the handler drives one account or three, and whether it trades in millionths or billions, did not change a single verdict.

What it cost

Median wall clock of the whole forge test command over seven measured runs after two discarded warmups, with the order of the setups rotated each round:

Setup Calls Wall clock CPU
No targeting, 2 properties 256,000 2.2 s 3.5 s
Pool targeted, 2 properties 256,000 2.6 s 4.5 s
Raw handler, 2 properties 256,000 5.5 s 10.2 s
Raw handler, 4 properties 512,000 6.1 s 21.9 s
vm.assume handler, 2 properties 256,000 9.6 s 18.5 s
vm.assume handler, 4 properties 512,000 11.1 s 41.0 s
Bounded handler, 2 properties 256,000 9.5 s 18.2 s
Bounded handler, 4 properties 512,000 10.8 s 39.3 s

Two things in that table are worth carrying away.

The first is the call counts. Every invariant_ function starts its own campaign, so going from two properties to four doubles the work. On a twelve-core machine the campaigns run in parallel and wall clock barely moves — 9.5 to 10.8 seconds — while CPU time goes from 18.2 to 39.3 seconds. On a CI runner with two cores that is a very different bill, and it is the number to plan against.

The second is that the cheap-looking setups are cheap because they are not doing anything. The version with no targeting finishes in two seconds partly because most of its calls revert on entry and partly because it gave up early: it reported its false failure in six of the seven measured rounds. Doubling the properties on the bounded handler cost 1.3 seconds of wall clock and tripled what the suite finds.

I re-ran the whole matrix on Foundry 1.8.1 and timed the same eight setups the same way. Wall clock barely moved, between 0.84x and 1.39x. The CPU time Forge reports moved a lot: 0.29x to 0.58x. On 1.5.1 it comes out at 1.6x to 1.9x the wall clock for a two-property setup and 3.6x for a four-property one. On 1.8.1 it is 0.94x to 0.99x for all eight. Whatever that reflects, the four-property setups no longer read as four campaigns running at once, and I did not chase the cause. Six of the 56 verdicts differed between the two releases, and all six were the untargeted setup or D6 — the same two cells that disagree with themselves between two runs of one release.

When I benchmarked Foundry against Hardhat 3, the closing caveat was that finishing the same number of runs faster does not mean finding more. This is the same caveat from inside one tool: four of these eight setups executed the same 128,000 calls and found a third as much.

How I would write one

In the order the measurements suggest.

Call targetContract before anything else. Without it the runner can impersonate the contract under test, and a counterexample you have to argue with is not a counterexample.

Write the handler for the properties you want, not for the fuzzer. Its real job is to be the place your actor list, your before-and-after state and your counters live. Constraining inputs is the side effect.

Bound against what the chosen actor can actually do, not against a constant. The handler bug in this experiment was a floor I had chosen rather than derived, and it only showed up in a state the campaign reached a few dozen times in 128,000 calls.

Run once with fail_on_revert = true. Not permanently — as a check that the handler only proposes legal calls. It found a bug in mine that 128,000 calls under the default had reported as between nineteen and fifty-four reverts.

Then read the metrics table, not the tick. Reverts, discards and your own declined counter are three different kinds of call that never happened, and all three look like a passing campaign.

Re-run anything that was not unanimous. A pinned --fuzz-seed does not pin an invariant verdict. Running this matrix twice moved 18 verdicts out of 280, and every one of them was a cell that had already looked marginal on the first pass.

Write at least one property about what the system promises its users. Not about what the code computes. In this experiment the properties derived from the pool's storage caught a third of the defects and the one derived from what a liquidity provider is owed caught all six.

If you only change one thing after reading this, make it the last one. Better handlers made this campaign cleaner, cheaper to interpret and, on one defect, slightly worse at its job. The properties are where the finding came from.

What this does not settle

Six defects that I chose, in one contract, with three actors and one handler design. A different six would move the table; the honest version of this experiment is mutation testing, and Foundry's documentation now describes a forge test --mutate MVP that is not in the release I measured against.

All eight setups asserted properties I wrote, which makes them exactly as good as I am. shareValueNeverFalls found four defects because I happened to state the pool's promise in a form that integer arithmetic can check. I did not find a way to know in advance which of my properties would turn out to be that one.

Every number here is from Foundry 1.5.1 with a 1.8.1 cross-check; 1.8.3 was published while I was measuring and I have not run anything against it.

The budgets are Foundry's defaults and the machine has twelve cores, which flatters anything that parallelises across invariant functions. Foundry 1.7.0 also added check_interval, which evaluates the invariant every N calls rather than every call and, in the documentation's own words, "can miss bugs that break and then restore the invariant between checks" — I ran everything at the default of 1 and did not measure what raising it costs.

And none of this is Foundry-specific except the syntax. Hardhat 3 runs Solidity invariant tests through its own engine with the same defaults, and its comeback means the question of what to assert is now the portable part of the problem.