Invariant testing catches the states a unit test never reaches
Forge generates random call sequences and asserts a property after each call, which finds multi-step insolvency and misses any property nobody wrote.
Bits & Blocks||7 min read
A unit test checks a path someone already thought of. An invariant test checks a property that must hold on every path, by generating random sequences of function calls and asserting the property after each call.1 Lending and vault protocols lose money in the gap between those two sentences, because the dangerous state is reached by a legal sequence of legal calls rather than by one malformed input.
Assert a property rather than an outcome
The property is the artefact.
A unit test encodes an expected output for a chosen input, so coverage grows one case at a time while the reachable state space grows with sequence length. An invariant encodes a condition that holds over all reachable states, and the fuzzer searches for a sequence that breaks it. The alternative that lost is writing more scenario tests, which fails on arithmetic: each new state-changing function multiplies the sequences a reviewer would have to enumerate by hand.
The cost is that someone has to write the property in executable form, which is the step most teams skip. It is paid by starting from a published set. Echidna sits in the property-based family of fuzzers, aiming to break user-defined invariants instead of hunting for crashes.2 Trail of Bits released 168 pre-built properties for Echidna on 27 February 2023, covering common ERC token interfaces and fixed-point maths operations.3
The limit belongs in the same passage: the fuzzer checks only properties that were written. An unstated property is untested, and a green suite says nothing about it.
| INVARIANT CLASS | THE PROPERTY | WHAT A VIOLATION LOOKS LIKE ON CHAIN |
|---|---|---|
| Conservation | Sum of inputs equals sum of outputs | Shares exist that no deposit backs |
| Solvency | Assets cover liabilities | Bad debt that no liquidation clears |
| Monotonicity | A value moves in one direction only | Share price falls on a deposit |
| Bounds | A value stays inside a stated range | Health factor below 1 after the account's own call |
| Access control | Only authorised callers change state | A role-gated setter reachable from an unguarded path |
| State consistency | Related variables stay in sync | Total supply diverges from the sum of balances |
THE SIX CLASSES IN COLUMN ONE ARE THE COMMON INVARIANTS LISTED IN THE FOUNDRY GUIDE.1 COLUMN THREE IS OURS, WRITTEN SO THAT EACH PROPERTY FAILS VISIBLY IN A TEST.
Euler: the property held everywhere except in one function
Euler enforced solvency per function.
Every balance-changing path ended with an account health check. One did not. The donateToReserves feature, introduced in eIP-14 and audited by the Sherlock team in July 2022, let an account donate its eToken balance to reserves while leaving its dToken debt unchanged, and performed no health check on the donating account.4 The incident followed on 13 March 2023 at approximately 08:50 UTC.4
The missing check on its own is not an exploit. It becomes one when three preconditions hold together. Euler permitted a caller to mint and deposit in the same transaction, creating leverage in excess of the collateral the protocol held. The liquidation discount scaled with how far under water a position sat, and the maximum 20% discount was applied during the attack transaction.4 A caller could liquidate a position it controlled inside the same block. Remove any one of the three and the donation produces a self-inflicted loss instead of a profit. Severity here is a statement about preconditions rather than an adjective.
Omniscia's post-mortem computed the DAI leg at approximately 8,779,854 USD as of 13 March 2023 12:42 UTC, and recorded that the attack was replicated across further assets.4 Larger totals in circulation come from parties whose method that document does not state, so this note carries only the figure the post-mortem calculated.
The reviewing habit that lost here is auditing the diff. eIP-14 changed a small amount of code, and the property it broke belonged to the whole protocol, so reading the changed lines in isolation could not surface it. An invariant asserting that no account's health factor drops below 1 through that account's own call would fail on the sequence, on one condition: the handler has to expose the new function. That condition is the standing cost of the technique, because a function added to the protocol and not to the handler stays untested while the suite reports success.
The handler decides what gets tested
The fuzzer never touches the protocol directly.
Handlers wrap the target contracts, bound inputs to ranges that can succeed, rotate a set of actors, and track ghost variables holding cumulative state the contracts do not store.1 The alternative that lost is open invariant testing, pointed straight at the protocol, which spends most of its runs on calls that revert and change nothing.
The cost is that the handler is code, and code can be wrong in a direction that hides bugs. A handler that returns early on an unmet precondition, or bounds an amount too tightly, produces a green suite over a smaller state space than the one claimed. It is paid by counting calls per selector and reading the summary, and by bounding with bound() rather than discarding with vm.assume().1
| SETTING | WHAT IT CHANGES | WHAT IT COSTS |
|---|---|---|
runs | Call sequences per campaign | Linear wall-clock time |
depth | Calls per sequence | Deeper states, longer traces to shrink |
fail_on_revert | Whether a reverting handler call fails the test | False hides reverts, true demands an exact handler |
check_interval | 0 checks the last call only, 1 checks every call, N checks every N calls and the last | Above 1, a bug that breaks and restores the invariant between checks is missed1 |
max_time_delay, max_block_delay | Fuzzes elapsed time and block distance between calls | Needed for vesting, auctions, TWAPs and cooldowns, and widens the search |
| Optimization mode | An int256 return switches the engine from finding a failure to maximising a value | Yields worst-case slippage as a number, and proves no failure |
seed | Fixes the sequence generator | Reproducible campaigns, which re-explore the same ground |
OPTION NAMES AND SEMANTICS ARE FROM THE FOUNDRY INVARIANT GUIDE AS AT 17 AUGUST 2026.1 THE LAST THREE OPTIONS ARRIVED IN FOUNDRY V1.7.0.
Cost, and where it is paid
Depth costs more than runs.
The example configuration in the Foundry guide sets 256 runs at a depth of 100 calls, which is up to 25,600 calls per invariant per campaign.1 A campaign at that scale fits inside a pull request. A campaign deep enough to find a six-step insolvency path does not.
The decision is a bounded campaign on every pull request and a deep campaign nightly. The alternative that lost is making the deep campaign a merge gate, which ties merge latency to fuzzer luck and teaches the team to rerun until the suite is green, turning a failing property into noise. The cost of the split is that a nightly failure arrives after the merge that caused it. It is paid by pinning a seed so the campaign is reproducible, and by treating a nightly failure as an incident with the failing call sequence attached, which Forge prints when an invariant breaks.1
Before the next deployment
The check that settles whether a suite covers an upgrade is mechanical. Run it against the implementation that is deployed, then read the handler's call-count summary. If a function added since the last audit shows zero calls, the upgrade is untested and the passing suite is reporting on the old system. Euler's donateToReserves sat in production from July 2022 until 13 March 2023.4
| NOT COVERED | WHY NOT, AND WHAT WOULD CHANGE IT |
|---|---|
| Properties nobody wrote | The engine checks stated invariants only. Changes when the property is merged and shown failing against a deliberately broken build. |
| Absence of bugs | Fuzzing samples the state space and cannot guarantee complete coverage, which is why Trail of Bits pairs it with static analysis, formal verification and unit tests.5 Changes when a prover is run against the specific function, with its assumptions listed. |
| States the handler cannot reach | Bounds and early returns silently shrink the search. Changes when the call-count summary shows every selector exercised.1 |
| Bugs that break and restore between checks | check_interval above 1 evaluates the invariant every N calls.1 Changes when that suite is set to 1, at the corresponding increase in run time. |
| Live oracle prices and real liquidity | Invariants run against mocks and bounded price movements. Changes when the campaign runs forked at a recorded block number. |
| Governance and upgrade paths | The audited system stops being the deployed system at the first upgrade, which is the Euler case.4 Changes when the suite runs against the upgraded implementation as a release gate. |
| Off-chain actors | Keeper, relayer and sequencer liveness sits outside the contracts under test. Changes when each liveness assumption is written as a property with a named owner. |
| Ordering and MEV | A protocol can hold every invariant and still let a searcher extract value through ordering. Changes when the invariant bounds extractable value rather than solvency. |
Sources
Footnotes
-
FOUNDRY BOOK, INVARIANT TESTING GUIDE. getfoundry.sh
-
BUILDING SECURE CONTRACTS, INTRODUCTION TO FUZZING. secure-contracts.com
-
TRAIL OF BITS, REUSABLE PROPERTIES FOR ETHEREUM CONTRACTS. blog.trailofbits.com
-
OMNISCIA, EULER FINANCE INCIDENT POST-MORTEM. medium.com
-
TRAIL OF BITS, FUZZING ON-CHAIN CONTRACTS WITH ECHIDNA. blog.trailofbits.com
