Writing invariants that find bugs

Fuzzers and provers are often described as tools that find bugs. More precisely, they find counterexamples to properties someone has written down. A fuzzer with no properties checks only that nothing reverts unexpectedly. A prover with a weak specification proves something true and unimportant. The quality of the property sets the ceiling on what the tool can find.

This primer describes how Quantix reviewers turn requirements into properties precise enough to fail, using an ERC-4626 vault as a running example.

Start from consequences

The most useful properties rarely come from reading the code. They come from asking what must never happen to the people who use the system: depositors must be able to withdraw what they are owed; nobody may mint shares without paying for them; only governance may change a fee; the protocol must not owe more than it holds.

Each of those sentences can be made precise. “Depositors can withdraw what they are owed” becomes a statement about the relationship between the vault’s asset balance and the value of all outstanding shares. Writing it down forces decisions the specification may have left open: owed at which exchange rate, rounded in which direction, under which assumptions about the underlying token.

Three kinds of property

State invariants are the most powerful because they must hold after any sequence of calls, including sequences nobody thought to test. Transition properties catch errors in a single step that an invariant might only reveal much later. Economic properties capture what users actually care about, and are often where the most serious findings come from.

Handlers and ghost variables

Stateful fuzzers call functions in random sequences with random inputs. Unconstrained, most of those calls revert: random amounts exceed balances, random addresses lack approvals. A handler sits between the fuzzer and the system, choosing realistic actors, bounding inputs to meaningful ranges, and setting up preconditions such as minting and approving tokens before a deposit.

Handlers also keep ghost variables: running totals the system does not store itself, such as the sum of all deposits and withdrawals. Ghost variables give invariants an independent model to compare against. The system’s own accounting is never the only witness to its correctness.

An invariant suite for a vault

1// Illustrative Foundry invariant suite for an ERC-4626 vault.2// The handler constrains inputs and records what *should* have happened.3contract VaultHandler is Test {4    Vault internal vault;5    TestToken internal asset;6    address[] internal actors;7 8    uint256 public ghostDeposited;   // ghost variables: the model's view9    uint256 public ghostWithdrawn;   // of the system, kept independently10 11    constructor(Vault v, TestToken a, address[] memory users) {12        vault = v;13        asset = a;14        actors = users;15    }16 17    function deposit(uint256 seed, uint256 assets) external {18        address actor = actors[seed % actors.length];19        assets = bound(assets, 1, 1e30);20        asset.mint(actor, assets);21        vm.startPrank(actor);22        asset.approve(address(vault), assets);23        vault.deposit(assets, actor);24        vm.stopPrank();25        ghostDeposited += assets;26    }27 28    function redeem(uint256 seed, uint256 shares) external {29        address actor = actors[seed % actors.length];30        shares = bound(shares, 0, vault.balanceOf(actor));31        if (shares == 0) return;32        uint256 preview = vault.previewRedeem(shares);33        vm.prank(actor);34        uint256 assets = vault.redeem(shares, actor, actor);35        // ERC-4626: previewRedeem must not promise more than redeem delivers.36        assertGe(assets, preview, "redeem returned less than previewRedeem");37        ghostWithdrawn += assets;38    }39}40 41contract VaultInvariants is Test {42    Vault internal vault;43    TestToken internal asset;44    VaultHandler internal handler;45 46    function setUp() public {47        asset = new TestToken();48        vault = new Vault(asset);49        handler = new VaultHandler(vault, asset, _actors());50        targetContract(address(handler));51    }52 53    /// Solvency: every outstanding share can be redeemed for what it claims.54    function invariant_solvency() public view {55        assertGe(asset.balanceOf(address(vault)), vault.convertToAssets(vault.totalSupply()));56    }57 58    /// Conservation: with no yield source, assets in = assets held + assets out.59    function invariant_conservation() public view {60        assertEq(asset.balanceOf(address(vault)), handler.ghostDeposited() - handler.ghostWithdrawn());61    }62}

Three properties are checked here. The assertion inside redeem encodes a requirement from the ERC-4626 standard: previewRedeem must return no more than redeem actually delivers in the same transaction. The solvency invariant states that outstanding shares are backed. The conservation invariant compares the vault’s balance with the ghost record of what went in and out; it would catch an accounting path that loses or creates assets, even if every individual function looked plausible.

Letting the handler behave like an attacker

The handler above models honest users. Real systems also face users who do things the designers did not expect, and the most valuable handlers include those actions deliberately.

• Donations. A donate action that transfers assets directly to the vault, bypassing deposit, is how share-price inflation attacks begin. Adding it immediately exposes vaults that lack virtual offsets. It also means the conservation invariant must change from equality to “at least”, which is itself a useful prompt to think about where donated value should go.
• Boundary values. Bounds such as bound(assets, 1, 1e30) keep calls meaningful, but they should still include the edges: one unit, the full balance, and amounts that exercise rounding at both ends. Many accounting bugs live only at those values.
• Time and external state. If the system accrues interest, rebalances or reads prices, the handler should be able to advance time and move the external inputs within realistic ranges, including the extreme ones.
• Privileged actions. Governance changes, pauses and upgrades belong in the handler too, executed by the roles allowed to perform them. Properties should state what remains true across those changes, and which guarantees users lose while the system is paused.

Each new action widens the space the fuzzer explores and usually forces at least one property to be restated more precisely. That is the process working as intended: the specification becomes more exact every time the model of the world becomes more realistic.

Proving your properties can fail

A passing invariant suite is weak evidence until you know it could have failed. Two checks make it stronger.

• Coverage of calls. Inspect how many handler calls succeeded. If nearly every call returns early or reverts, the fuzzer explored almost nothing and the invariants passed vacuously. Tooling can report call summaries; review them.
• Mutation of the system. Introduce deliberate bugs, such as flipping a rounding direction, removing an access check or skipping a state update, and confirm that at least one property fails for each. A mutation that survives marks a gap in the specification.

Quantix applies the same discipline to its own formal specifications: every rule delivered to a client has been shown to fail against a mutated version of the code.

From fuzzing to proofs

Fuzzing samples behaviours; formal verification reasons about all of them within a model. The properties are the same. A well-written invariant suite is therefore also the starting point for formal verification, and moving between the two is cheaper than starting either from scratch.

What changes is the treatment of assumptions. A prover will ask what the token does on transfer, what an oracle may return, and whether arithmetic can overflow. Each answer becomes an explicit assumption in the result. Those assumptions are not a weakness of formal methods; they are a precise record of what the guarantee depends on, and they should be monitored in production like any other critical dependency.

It also helps to be precise about what kind of result each tool gives. A fuzzing campaign that finds nothing after many millions of calls is evidence, not proof: it says the explored sequences were safe, weighted by how well the handler steered exploration. A bounded model check proves the property for every sequence up to a given length, and nothing beyond it. An unbounded proof covers every reachable state of the model, under its assumptions. Reports should say which of these a result is, because readers will otherwise assume the strongest.

A short summary of the approach:

• Write properties from requirements and user consequences, not from the implementation.
• Prefer state invariants that must hold after any sequence of calls.
• Use handlers to make calls meaningful and ghost variables to keep an independent record.
• Check call coverage and mutation results before trusting a passing suite.
• State every assumption explicitly, and carry it from fuzzing into verification.

Conclusions

The tools that check properties are mature; the bottleneck is the properties themselves. Invariants written from users’ requirements, compared with an independent model in ghost state, exercised by handlers that include adversarial actions, and shown to be capable of failing, find bugs that reviews and unit tests miss.

The same properties carry over from fuzzing to proofs. Smart contract fuzzing techniques covers how to make a fuzzer explore, and formal verification in DeFi covers what a proof of the same property adds.

Recommendations