Invariant testing is a discipline, not a feature flag. You can run forge test with a handful of invariant_ functions and get a green suite that tells you almost nothing. Or you can build a structured test harness that, over 256 runs of 512 calls each, genuinely explores your protocol’s state space and catches the class of multi-transaction bugs that unit tests cannot. The difference between those two outcomes is almost entirely in the implementation infrastructure — the handler, the ghost variables, the actor model, and the careful translation of your specification into falsifiable properties.
This guide walks you through every component of that infrastructure, using a simplified lending vault as the running example. By the end you will have a complete, working invariant suite you can adapt to real protocols.
1. What Invariant Testing Actually Does
Invariant tests are stateful fuzz tests that assert “rules” which must always hold true, even after any sequence of contract calls. The fuzzer does not just try random inputs to a single function — it constructs random sequences of calls across the entire target surface and checks your assertions after each one.
In practice, you write test functions with the prefix invariant_, and Forge will generate random sequences of transactions on your contracts to try to violate those invariants.
The practical power of this comes from the stateful nature: a bug that only appears after a deposit, then a borrow, then an accrue, then a liquidate in a specific ratio will never be found by unit testing. Stateful fuzzing explores exactly that combinatorial space. This approach excels at finding unexpected state transitions and complex multi-transaction bugs that static analysis might miss.
2. Identifying Protocol Invariants from Specifications
Before writing a single line of test code, you need to read your protocol specification as a set of invariants — properties that must hold in every reachable state, not just at initialization.
The Taxonomy of DeFi Invariants
Every DeFi protocol has at least four families of invariants you should enumerate:
Solvency invariants concern whether the protocol can meet its obligations. Solvency refers to the availability of assets within a contract, particularly the liquidity provided by LPs, to facilitate trades. For a protocol to be considered solvent, it must always have enough funds to satisfy all withdrawals. For a lending protocol, this is: totalAssets >= totalBorrows.
Accounting invariants concern internal consistency between tracked values. The canonical example: token.totalSupply() == sum(balanceOf(user) for all users). A more lending-specific version: sumOfAllUserShareBalances == pool.totalShares().
Access control invariants concern who can do what. The owner can never be address(0). A paused protocol must reject state-changing calls. A user cannot withdraw more than they deposited.
Economic invariants concern the financial logic of the system — often the hardest to specify precisely. Five invariants for every lending protocol: solvency, liquidation feasibility, no atomic profit, collateral factor bounds, and oracle sanity.
Local vs. Global Invariants
This distinction matters for prioritization and test structure.
A local invariant constrains a specific function’s behavior independent of protocol history: “a single withdraw(x) call must decrease the caller’s balance by exactly x.” These are better expressed as unit tests or property-based fuzz tests on a single function, not invariant tests.
A global invariant constrains state that can only be violated through a sequence of operations: “the sum of all user balances must always equal totalSupply regardless of the order and combination of deposit, withdraw, transfer, and borrow calls.” This is the class invariant testing is designed for. Every invariant in your suite should be global — if it can be falsified in a single call, write a unit test.
Extracting Invariants from a Specification
Take a simplified specification for a collateralized lending vault:
- Users deposit ERC20 tokens and receive shares proportional to the pool's NAV.
- Users may borrow up to their collateral value multiplied by the LTV factor.
- The health factor of any position must be ≥ 1.0 for a withdrawal to succeed.
- Interest accrues per-block on outstanding borrows.
- Liquidations are available when health factor < 1.0.From this, extract:
| Property | Invariant Expression |
|---|---|
| Share accounting | totalShares == sum(shares[user]) |
| Solvency | totalAssets >= totalBorrows |
| No under-collateralized withdrawal | healthFactor(user) >= 1e18 after withdraw |
| Interest monotonicity | totalDebt >= totalDebt at any prior block |
| Liquidation precondition | liquidatable positions always have healthFactor < 1e18 |
Write these down as a table before opening your editor. Invariants you cannot state in prose will not become useful tests.
3. The Handler Pattern in Detail
With open invariant testing, the fuzzer makes random sequences of function calls to the protocol contracts directly with fuzzed parameters. This will cause reverts for more complex systems. An unconstrained fuzzer hitting borrow(uint256) with amount = type(uint256).max will revert on every single call and explore nothing meaningful.
The handler is the solution. By manually adding all handler contracts to the targetContracts array, all function calls made to protocol contracts can be made in a way that is governed by the handler to ensure successful calls.
With this layer between the fuzzer and the protocol, more powerful testing can be achieved.
The Three Responsibilities of a Handler
A well-built handler does exactly three things:
- Bounds inputs to valid ranges using
bound()so calls don’t revert on trivial precondition failures. - Sets up preconditions — minting tokens, giving approvals, advancing time, setting actor context — before calling the real protocol.
- Updates ghost variables to maintain a shadow model of expected state alongside every state-changing call.
Handler Structure
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
contract LendingVaultHandler is Test {
/*//////////////////////////////////////////////////////////////
STATE
//////////////////////////////////////////////////////////////*/
LendingVault public vault;
MockERC20 public asset;
// --- Actor management ---
address[] public actors;
address internal currentActor;
// --- Ghost variables ---
uint256 public ghost_depositSum;
uint256 public ghost_withdrawSum;
uint256 public ghost_borrowSum;
uint256 public ghost_repaySum;
mapping(address => uint256) public ghost_userShares;
mapping(address => uint256) public ghost_userBorrows;
// --- Call counters (for coverage metrics) ---
mapping(bytes4 => uint256) public calls;
/*//////////////////////////////////////////////////////////////
SETUP
//////////////////////////////////////////////////////////////*/
constructor(LendingVault _vault, MockERC20 _asset) {
vault = _vault;
asset = _asset;
// Create a fixed actor set — avoids the fuzzer exploring
// the entire address space and missing repeated interactions.
actors.push(address(0xA001));
actors.push(address(0xA002));
actors.push(address(0xA003));
actors.push(address(0xA004));
// Pre-fund all actors
for (uint256 i; i < actors.length; i++) {
asset.mint(actors[i], 100_000e18);
vm.prank(actors[i]);
asset.approve(address(vault), type(uint256).max);
}
}
/*//////////////////////////////////////////////////////////////
MODIFIERS
//////////////////////////////////////////////////////////////*/
modifier useActor(uint256 actorIndexSeed) {
currentActor = actors[bound(actorIndexSeed, 0, actors.length - 1)];
vm.startPrank(currentActor);
_;
vm.stopPrank();
}
modifier countCall() {
calls[msg.sig]++;
_;
}
/*//////////////////////////////////////////////////////////////
HANDLER FUNCTIONS
//////////////////////////////////////////////////////////////*/
function deposit(
uint256 actorSeed,
uint256 assets
) external useActor(actorSeed) countCall {
assets = bound(assets, 1, asset.balanceOf(currentActor));
if (assets == 0) return;
uint256 sharesBefore = vault.totalShares();
uint256 shares = vault.deposit(assets, currentActor);
// Ghost bookkeeping
ghost_depositSum += assets;
ghost_userShares[currentActor] += shares;
}
function withdraw(
uint256 actorSeed,
uint256 sharesToBurn
) external useActor(actorSeed) countCall {
uint256 userShares = vault.sharesOf(currentActor);
if (userShares == 0) return;
sharesToBurn = bound(sharesToBurn, 1, userShares);
uint256 assetsOut = vault.withdraw(sharesToBurn, currentActor);
ghost_withdrawSum -= assetsOut; // net against deposits
ghost_userShares[currentActor] -= sharesToBurn;
}
function borrow(
uint256 actorSeed,
uint256 amount
) external useActor(actorSeed) countCall {
uint256 maxBorrow = vault.maxBorrow(currentActor);
if (maxBorrow == 0) return;
amount = bound(amount, 1, maxBorrow);
vault.borrow(amount, currentActor);
ghost_borrowSum += amount;
ghost_userBorrows[currentActor] += amount;
}
function repay(
uint256 actorSeed,
uint256 amount
) external useActor(actorSeed) countCall {
uint256 debt = vault.debtOf(currentActor);
if (debt == 0) return;
amount = bound(amount, 1, debt);
// Repayer needs tokens — mint fresh if needed
if (asset.balanceOf(currentActor) < amount) {
asset.mint(currentActor, amount);
}
vault.repay(amount, currentActor);
ghost_repaySum += amount;
ghost_userBorrows[currentActor] -= amount;
}
function accrueInterest() external countCall {
// Advance time to trigger interest accrual; bound to
// realistic windows so NAV doesn't go astronomically wrong.
uint256 warpSeconds = bound(
uint256(keccak256(abi.encode(block.timestamp))),
1,
7 days
);
vm.warp(block.timestamp + warpSeconds);
vault.accrueInterest();
}
function liquidate(
uint256 actorSeed,
uint256 targetActorSeed
) external useActor(actorSeed) countCall {
address target = actors[bound(targetActorSeed, 0, actors.length - 1)];
if (!vault.isLiquidatable(target)) return;
uint256 debt = vault.debtOf(target);
if (debt == 0) return;
// Fund liquidator if needed
if (asset.balanceOf(currentActor) < debt) {
asset.mint(currentActor, debt);
}
vault.liquidate(target, currentActor);
// Adjust ghost state for liquidated position
ghost_userBorrows[target] = 0;
ghost_userShares[target] = 0;
}
/*//////////////////////////////////////////////////////////////
VIEW HELPERS
//////////////////////////////////////////////////////////////*/
function actorCount() external view returns (uint256) {
return actors.length;
}
function getActor(uint256 i) external view returns (address) {
return actors[i];
}
}By leveraging the prank cheatcodes in forge-std, each handler can manage a set of actors and use them to perform the same function call from different msg.sender addresses. This allows for more granular ghost variable usage as well.
4. Ghost Variables for Tracking Expected State
Within handlers, “ghost variables” can be tracked across multiple function calls to add additional information for invariant tests. The name comes from formal verification — a ghost variable exists only in the proof environment (here: the test harness) and has no on-chain counterpart.
Ghost variables serve a critical purpose: they let you express invariants that compare the protocol’s actual state against your model of what it should be, not just against itself. This catches a whole class of off-by-one, rounding, and accounting drift bugs that pure protocol-state comparisons miss.
A good example of this is summing all of the shares that each LP owns after depositing into an ERC-4626 token as shown above, and using that in the invariant (totalSupply == sumBalanceOf).
Ghost variables are essentially state variables that are used only for testing purposes.
The Ghost Variable Contract Pattern
For complex suites, extract ghost state into its own contract to share it across multiple handlers:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
/// @dev Mutable store for cross-handler ghost state.
/// Only handlers and the invariant contract should write here.
contract GhostStore {
address public owner;
// Aggregate deposit/withdraw tracking
uint256 public totalDeposited;
uint256 public totalWithdrawn;
// Per-user share ledger (our expected model)
mapping(address => uint256) public expectedShares;
uint256 public expectedTotalShares;
// Debt model
mapping(address => uint256) public expectedDebt;
uint256 public expectedTotalDebt;
// Flags set by handlers on meaningful state transitions
bool public anyLiquidationOccurred;
constructor() { owner = msg.sender; }
modifier onlyOwner() {
require(msg.sender == owner, "GhostStore: not owner");
_;
}
function recordDeposit(address user, uint256 assets, uint256 shares) external onlyOwner {
totalDeposited += assets;
expectedShares[user] += shares;
expectedTotalShares += shares;
}
function recordWithdraw(address user, uint256 assets, uint256 shares) external onlyOwner {
totalWithdrawn += assets;
expectedShares[user] -= shares;
expectedTotalShares -= shares;
}
function recordBorrow(address user, uint256 amount) external onlyOwner {
expectedDebt[user] += amount;
expectedTotalDebt += amount;
}
function recordRepay(address user, uint256 amount) external onlyOwner {
expectedDebt[user] = expectedDebt[user] > amount ? expectedDebt[user] - amount : 0;
expectedTotalDebt = expectedTotalDebt > amount ? expectedTotalDebt - amount : 0;
}
function recordLiquidation(address user) external onlyOwner {
expectedTotalDebt -= expectedDebt[user];
expectedTotalShares -= expectedShares[user];
expectedDebt[user] = 0;
expectedShares[user] = 0;
anyLiquidationOccurred = true;
}
}The handler then writes into the GhostStore after every successful protocol call. The invariant contract reads both the protocol state and the GhostStore and diffs them.
5. The Invariant Contract
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
contract LendingVaultInvariantTest is Test {
LendingVault internal vault;
MockERC20 internal asset;
LendingVaultHandler internal handler;
GhostStore internal ghost;
function setUp() public {
asset = new MockERC20("Test Token", "TST", 18);
vault = new LendingVault(address(asset));
ghost = new GhostStore();
handler = new LendingVaultHandler(vault, asset, ghost);
// Transfer ownership of ghost store to handler so only it can write
ghost.transferOwnership(address(handler));
// Tell Forge: only call the handler, never the vault directly.
targetContract(address(handler));
// Optionally restrict to a specific selector list — useful when
// iterating incrementally (see §10).
bytes4[] memory selectors = new bytes4[](6);
selectors[0] = LendingVaultHandler.deposit.selector;
selectors[1] = LendingVaultHandler.withdraw.selector;
selectors[2] = LendingVaultHandler.borrow.selector;
selectors[3] = LendingVaultHandler.repay.selector;
selectors[4] = LendingVaultHandler.accrueInterest.selector;
selectors[5] = LendingVaultHandler.liquidate.selector;
targetSelector(FuzzSelector({
addr: address(handler),
selectors: selectors
}));
}
/*//////////////////////////////////////////////////////////////
SEVERITY-1: SOLVENCY (CRITICAL)
//////////////////////////////////////////////////////////////*/
/// @notice The protocol must always hold enough assets to cover all borrows.
/// Violation = undercollateralized system = user funds at risk.
function invariant_solvency() public view {
assertGe(
asset.balanceOf(address(vault)),
vault.totalBorrows(),
"SOLVENCY: vault assets < total borrows"
);
}
/// @notice Assets held plus outstanding loans must equal total deposits minus withdrawals.
/// This is the conservation-of-value invariant.
function invariant_conservationOfValue() public view {
uint256 netDeposited = ghost.totalDeposited() - ghost.totalWithdrawn();
// After interest, the vault may hold more than deposited — but never less
// than what is owed on outstanding borrows.
assertGe(
vault.totalAssets() + vault.totalBorrows(),
netDeposited,
"CONSERVATION: total tracked value < net deposits"
);
}
/*//////////////////////////////////////////////////////////////
SEVERITY-2: SHARE ACCOUNTING (HIGH)
//////////////////////////////////////////////////////////////*/
/// @notice The vault's totalShares must equal the sum of all individual share balances.
/// Discrepancy here means shares can be created or destroyed from nothing.
function invariant_shareSumMatchesTotalShares() public view {
uint256 sumShares;
uint256 actorCount = handler.actorCount();
for (uint256 i; i < actorCount; i++) {
sumShares += vault.sharesOf(handler.getActor(i));
}
assertEq(
vault.totalShares(),
sumShares,
"SHARES: totalShares != sum of individual shares"
);
}
/// @notice Ghost model shares must match actual vault shares.
/// This catches rounding bugs that the protocol might silently absorb.
function invariant_ghostSharesMatchActual() public view {
uint256 actorCount = handler.actorCount();
for (uint256 i; i < actorCount; i++) {
address actor = handler.getActor(i);
assertApproxEqAbs(
vault.sharesOf(actor),
ghost.expectedShares(actor),
// Allow 1 wei of rounding per operation (generous upper bound)
actorCount * 1,
"GHOST_SHARES: ghost share model diverged from vault"
);
}
}
/*//////////////////////////////////////////////////////////////
SEVERITY-3: DEBT ACCOUNTING (HIGH)
//////////////////////////////////////////////////////////////*/
/// @notice Total debt tracked by protocol must match sum of user debts.
function invariant_debtSumMatchesTotalBorrows() public view {
uint256 sumDebt;
uint256 actorCount = handler.actorCount();
for (uint256 i; i < actorCount; i++) {
sumDebt += vault.debtOf(handler.getActor(i));
}
assertEq(
vault.totalBorrows(),
sumDebt,
"DEBT: totalBorrows != sum of individual debts"
);
}
/*//////////////////////////////////////////////////////////////
SEVERITY-4: LIQUIDATION LOGIC (MEDIUM)
//////////////////////////////////////////////////////////////*/
/// @notice No liquidatable position should have health factor >= 1.0.
/// A breach means the protocol allows healthy positions to be liquidated.
function invariant_noHealthyPositionIsLiquidatable() public view {
uint256 actorCount = handler.actorCount();
for (uint256 i; i < actorCount; i++) {
address actor = handler.getActor(i);
if (vault.isLiquidatable(actor)) {
assertLt(
vault.healthFactor(actor),
1e18,
"LIQUIDATION: healthy position marked liquidatable"
);
}
}
}
/// @notice Every position with debt must have non-zero collateral.
/// This guards against ghost positions that owe but cannot be liquidated.
function invariant_debtRequiresCollateral() public view {
uint256 actorCount = handler.actorCount();
for (uint256 i; i < actorCount; i++) {
address actor = handler.getActor(i);
if (vault.debtOf(actor) > 0) {
assertGt(
vault.collateralOf(actor),
0,
"COLLATERAL: debt without collateral"
);
}
}
}
/*//////////////////////////////////////////////////////////////
SEVERITY-5: MONOTONICITY (LOW/INFORMATIONAL)
//////////////////////////////////////////////////////////////*/
/// @notice Cumulative interest accrued can only go up, never down.
/// Regression here points to negative interest or reset bugs.
function invariant_interestMonotonicity() public view {
assertGe(
vault.totalInterestAccrued(),
vault.initialInterestSnapshot(),
"INTEREST: total interest decreased"
);
}
/*//////////////////////////////////////////////////////////////
POST-INVARIANT CALLBACK
//////////////////////////////////////////////////////////////*/
/// @dev Called by Forge after every run. Use for end-of-sequence checks
/// and coverage reporting.
function afterInvariant() public view {
// Verify call distribution — alert if any handler function was never called
assertGt(handler.calls(LendingVaultHandler.deposit.selector), 0, "deposit never called");
assertGt(handler.calls(LendingVaultHandler.withdraw.selector), 0, "withdraw never called");
assertGt(handler.calls(LendingVaultHandler.borrow.selector), 0, "borrow never called");
}
}6. Handling External Calls in Invariant Tests
DeFi protocols interact with external systems: oracles, token contracts, other protocols via callback interfaces. These create two problems:
Problem 1: Uncontrolled external state. If your vault reads a Chainlink oracle, the fuzzer cannot mutate that oracle’s response unless you give it the tools to do so. Add an oracle handler function:
function setOraclePrice(uint256 price) external countCall {
// Bound to a realistic range — avoid absurd prices that only
// exercise impossible paths.
price = bound(price, 0.01e8, 100_000e8); // 8-decimal price feed
mockOracle.setPrice(price);
}Problem 2: Reentrancy via callbacks. If your protocol calls token.transfer() which can trigger an onTokenReceived callback on a receiver contract, the invariant can be checked in an intermediate state. There are two approaches:
- Use
vm.mockCallto neutralize the callback in the handler. - Deploy a
MaliciousReceiverthat the fuzzer can trigger, and verify your protocol’s reentrancy guards hold:
/// @dev Attempts reentrant withdraw during deposit callback.
contract ReentrantReceiver {
LendingVault vault;
bool public reentered;
constructor(LendingVault _vault) { vault = _vault; }
function onTokenReceived(address, uint256) external {
if (!reentered) {
reentered = true;
try vault.withdraw(1, address(this)) {
// If this succeeds, reentrancy guard is broken
} catch {}
}
}
}Then in your invariant: assertFalse(reentrantReceiver.reentered(), "reentrancy guard bypassed").
For time-based operations, use vm.warp and vm.roll inside handler functions. The fuzzer can use vm.warp and vm.roll to find time progressions that exercise time-based code paths. You can optimize for maximum interest accrual over time.
With handlers, input parameters can be bounded to reasonable expected values such that fail_on_revert in foundry.toml can be set to true. This can be accomplished using the bound() helper function from forge-std. This is one of the most important settings: with fail_on_revert = true, any unexpected revert inside a handler is a test failure, not a silent discard. It forces you to write handlers that only exercise valid paths — which is what gives you confidence that your fuzzer is actually exploring meaningful state.
7. Translating to Echidna
Echidna uses a different model: the core Echidna functionality takes a contract and a list of invariants as input. For each invariant, it generates random sequences of calls to the contract and checks if the invariant holds. If it can find some way to falsify the invariant, it prints the call sequence that does so.
Invariants are expressed as Solidity functions with names that begin with echidna_, have no arguments, and return a boolean.
The same lending vault invariants translate directly:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
contract LendingVaultEchidna {
LendingVault internal vault;
MockERC20 internal asset;
// Ghost variables live directly in the test contract for Echidna
uint256 internal ghost_totalDeposited;
uint256 internal ghost_totalWithdrawn;
address[] internal actors = [
address(0x10000),
address(0x20000),
address(0x30000)
];
constructor() {
asset = new MockERC20("Test", "TST", 18);
vault = new LendingVault(address(asset));
for (uint256 i; i < actors.length; i++) {
asset.mint(actors[i], 100_000e18);
}
}
// === Actions (called by Echidna) ===
function deposit(uint256 actorIdx, uint256 amount) public {
actorIdx = actorIdx % actors.length;
address actor = actors[actorIdx];
amount = clamp(amount, 1, asset.balanceOf(actor));
if (amount == 0) return;
asset.approve(address(vault), amount); // actor context is msg.sender
uint256 shares = vault.deposit(amount, actor);
ghost_totalDeposited += amount;
}
function withdraw(uint256 actorIdx, uint256 shares) public {
actorIdx = actorIdx % actors.length;
address actor = actors[actorIdx];
uint256 maxShares = vault.sharesOf(actor);
if (maxShares == 0) return;
shares = clamp(shares, 1, maxShares);
uint256 assets = vault.withdraw(shares, actor);
ghost_totalWithdrawn += assets;
}
// === Invariants ===
function echidna_solvency() public view returns (bool) {
return asset.balanceOf(address(vault)) >= vault.totalBorrows();
}
function echidna_total_shares_consistency() public view returns (bool) {
uint256 sum;
for (uint256 i; i < actors.length; i++) {
sum += vault.sharesOf(actors[i]);
}
return vault.totalShares() == sum;
}
function echidna_conservation_of_value() public view returns (bool) {
uint256 netDeposited = ghost_totalDeposited - ghost_totalWithdrawn;
return vault.totalAssets() + vault.totalBorrows() >= netDeposited;
}
// === Helpers ===
function clamp(uint256 value, uint256 low, uint256 high)
internal pure returns (uint256)
{
if (high < low) return low;
return low + (value % (high - low + 1));
}
}Echidna configuration (echidna.yaml):
testMode: "property"
testLimit: 100000
seqLen: 100
shrinkLimit: 5000
corpusDir: "echidna-corpus"
coverage: true
workers: 4In stateful mode, Echidna will maintain the state between each function call and attempt to break the invariants. Stateful is more powerful and can allow breaking invariants that exist only if the contract reaches a specific state.
8. Prioritizing Invariants by Severity
Not all invariants are equally important. When you have limited compute time or are iterating quickly, run high-severity invariants at higher depth and with more runs.
| Severity | Category | Example | What Violation Means |
|---|---|---|---|
| Critical | Solvency | totalAssets >= totalBorrows | User funds can be stolen |
| Critical | Token conservation | totalSupply == sumBalances | Token minting from thin air |