DeFi Economic Invariant Fuzzing: Methods and Best Practices

In modern decentralized finance security, the highest-impact failures often come from valid transactions that compose into invalid economics. The contract does exactly what the source code says, no access control is bypassed, no compiler warning fires, and no single function reverts incorrectly. Yet after a sequence of deposits, borrows, swaps, liquidations, reward updates, oracle reads, and withdrawals, the protocol state violates a core promise: assets are undercollateralized, reserves are mispriced, shares are overminted, or rewards are claimable twice.

That class of bug is why economic invariant fuzzing matters. Traditional unit tests validate examples. Invariant fuzzing validates boundaries. Instead of asking "does this one borrow path work?", the auditor asks "after any allowed sequence of calls by any actor, is the system still solvent, internally consistent, and economically bounded?"

The open-source toolchain is mature enough that every serious DeFi audit should include it. Echidna provides property-based and coverage-guided smart contract fuzzing. Foundry gives fast Solidity-native invariant tests through Forge. Medusa adds parallelized, coverage-guided fuzzing powered by go-ethereum. Slither helps extract static structure and pre-audit signals before a campaign. Halmos brings symbolic testing to paths where fuzzing needs solver assistance.

1. What is an Economic Invariant?

An economic invariant is an assertion that should hold across the reachable state space of a protocol. It is stronger than a unit test because it does not assume a single transaction order. It is also more domain-specific than a generic safety property because it encodes a financial promise.

Good invariants are usually phrased as:

• Conservation: balances, shares, reserves, and debt sum to an expected accounting total.
• Solvency: protocol assets remain sufficient to satisfy liabilities under documented assumptions.
• Monotonicity: an index, accumulator, exchange rate, or checkpoint moves only in the intended direction.
• Bounded loss: fees, rounding, and slippage remain within explicit tolerances.
• Authorization: privileged transitions cannot occur without the expected role or delay.
• Non-extractability: no actor can end a sequence with more value than the model permits.

Mathematical Examples

Lending market solvency

For every healthy account, risk-adjusted collateral must cover debt:

$\sum_i collateral_i \cdot liquidationThreshold_i \ge \sum_i debt_i$

At the market level, cash plus outstanding borrows should cover redeemable supplier claims up to expected interest and reserve accounting:

$cash + borrows - reserves \ge supplyShares \cdot exchangeRate$

If a sequence lets a borrower withdraw collateral, manipulate a price, and remain marked healthy while the inequality fails, the protocol has an economic bug.

Constant-product AMM reserve integrity

For a basic AMM:

$x \cdot y = k$

After a swap with fees, the adjusted product should not decrease:

$k_{t+1} \ge k_t$

The invariant must account for fees, rounding, and token behavior. For fee-on-transfer or rebasing tokens, a naive reserve invariant is often wrong because balanceOf(pool) can move independently of pool accounting.

Staking and rewards

For a staking system:

$\sum_j balanceOf[j] = totalStaked$

For rewards:

$distributedRewards + undistributedRewards + protocolFees \le fundedRewards$

If reward debt is updated after transfer, or if an actor can checkpoint with zero shares and later claim historical rewards, a fuzzer can discover a sequence that breaks this budget.

2. Toolchain: What Each Project is Good For

In practice, these tools are complementary rather than mutually exclusive. A strong audit workflow often looks like:

1. Run Slither first to identify obvious hazards, inheritance structure, external calls, storage writes, and privileged methods.
2. Build Foundry invariants for fast local development and regression tests.
3. Port the highest-value properties to Echidna or Medusa for longer-running campaigns.
4. Use Halmos on small arithmetic or authorization properties where random exploration struggles.
5. Preserve every minimized counterexample as a regression test.

3. Harness Architecture

The harness is more important than the fuzzer. A weak harness gives false confidence because it explores irrelevant states or excludes the attacker behavior that matters.

A good DeFi invariant harness contains five pieces:

• Actors: normal users, whales, liquidators, keepers, governance, oracle updaters, and malicious receivers.
• Handlers: bounded wrapper functions that call the protocol in realistic but adversarial ways.
• Ghost accounting: model-side variables that track expected value independently from protocol storage.
• Assumptions: constraints that exclude impossible states without hiding real attacks.
• Invariants: compact properties that compare protocol state to the model.

Example: Actor-Based Handler Pattern

contract LendingHandler {
    LendingMarket market;
    MockERC20 collateral;
    MockERC20 debtAsset;

    address[] internal actors;
    mapping(address => uint256) public ghostDeposits;
    mapping(address => uint256) public ghostBorrows;

    constructor(LendingMarket _market, MockERC20 _collateral, MockERC20 _debtAsset) {
        market = _market;
        collateral = _collateral;
        debtAsset = _debtAsset;

        actors.push(address(0xA11CE));
        actors.push(address(0xB0B));
        actors.push(address(0xCAFE));
    }

    function actor(uint256 seed) internal view returns (address) {
        return actors[seed % actors.length];
    }

    function deposit(uint256 actorSeed, uint256 amount) external {
        address user = actor(actorSeed);
        amount = bound(amount, 1e6, 1_000_000e6);

        collateral.mint(user, amount);
        vm.startPrank(user);
        collateral.approve(address(market), amount);
        market.deposit(amount);
        vm.stopPrank();

        ghostDeposits[user] += amount;
    }

    function borrow(uint256 actorSeed, uint256 amount) external {
        address user = actor(actorSeed);
        amount = bound(amount, 1e6, 500_000e6);

        vm.prank(user);
        try market.borrow(amount) {
            ghostBorrows[user] += amount;
        } catch {}
    }
}

Handlers should not be too polite. They should attempt calls that might fail, vary actor order, operate near boundary values, and include malicious receiver contracts. If every handler avoids reverts perfectly, the campaign may miss the exact transition where the bug lives.

4. Dynamic Testing with Echidna

Echidna tests Solidity predicates by generating random transaction sequences against contract ABIs. Its classic property mode uses functions prefixed with echidna_ that return bool. It also supports assertion-style and Foundry-style modes, which makes it useful for both standalone audits and projects that already have Forge tests.

Vulnerable Staking Contract

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

contract StakingVault {
    mapping(address => uint256) public balanceOf;
    uint256 public totalStaked;

    function stake() external payable {
        require(msg.value > 0, "zero stake");
        balanceOf[msg.sender] += msg.value;
        totalStaked += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(balanceOf[msg.sender] >= amount, "insufficient balance");

        // Vulnerability: external call before accounting update.
        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "transfer failed");

        balanceOf[msg.sender] -= amount;
        totalStaked -= amount;
    }
}

Echidna Harness

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;

import "./StakingVault.sol";

contract StakingFuzzTest is StakingVault {
    address[] public users;

    constructor() payable {
        users.push(address(0x1001));
        users.push(address(0x1002));
        users.push(address(0x1003));
    }

    function echidna_total_staked_matches_balances() public view returns (bool) {
        uint256 computedTotal = 0;

        for (uint256 i = 0; i < users.length; i++) {
            computedTotal += balanceOf[users[i]];
        }

        return computedTotal == totalStaked;
    }
}

This first version still has a modeling weakness: Echidna will call the harness contract directly, but the users list does not automatically become msg.sender. A better harness uses handler functions that route calls through controlled actor addresses or proxy contracts. The distinction matters. Many DeFi bugs are actor-sensitive: the same function is safe for an EOA and unsafe for a contract with a callback.

Example Echidna Configuration

testMode: property
testLimit: 200000
seqLen: 80
shrinkLimit: 10000
corpusDir: corpus/echidna
balanceContract: 100000000000000000000
coverage: true
filterFunctions:
  - "StakingFuzzTest.stakeAs(uint256,uint256)"
  - "StakingFuzzTest.withdrawAs(uint256,uint256)"

Configuration should be versioned alongside the audit harness. Changing seqLen, balances, actor sets, or filtered functions changes the meaning of the campaign.

5. Foundry Invariant Testing

Foundry is often the fastest way to develop invariants because the tests are Solidity-native and fit directly into existing Forge workflows.

contract LendingInvariantTest is Test {
    LendingMarket market;
    LendingHandler handler;

    function setUp() public {
        market = new LendingMarket();
        handler = new LendingHandler(market, collateral, debtAsset);

        targetContract(address(handler));
        targetSelector(FuzzSelector({
            addr: address(handler),
            selectors: selectors()
        }));
    }

    function selectors() internal pure returns (bytes4[] memory s) {
        s = new bytes4[](4);
        s[0] = LendingHandler.deposit.selector;
        s[1] = LendingHandler.borrow.selector;
        s[2] = LendingHandler.repay.selector;
        s[3] = LendingHandler.liquidate.selector;
    }

    function invariant_marketSolvent() public {
        assertGe(market.cash() + market.totalBorrows(), market.totalSupplyAssets());
    }
}

Foundry is also useful for fork-based invariants. For example, a lending market can be tested against live token behavior, live Chainlink decimals, or real AMM reserves. Fork fuzzing is slower and less deterministic, so it should supplement local mocks rather than replace them.

6. Medusa for Long Campaigns

Medusa is useful when a property needs deeper sequence exploration or more parallel compute. It is especially appropriate for:

• AMM and lending systems with many valid transaction orders.
• Protocols where failures require long setup sequences.
• Handler suites with many actors and multiple markets.
• Regression campaigns that run overnight or in CI on dedicated runners.

The audit pattern is to develop fast properties in Foundry, validate the harness manually, then run the same or equivalent properties in Echidna or Medusa for deeper exploration. If Medusa finds a sequence, reduce it to a readable regression test.

7. Slither and Static Pre-Analysis

Slither is not a substitute for economic fuzzing, but it helps decide what to fuzz. Before writing invariants, run static analysis and review:

• External calls before storage updates.
• Unbounded loops over user-controlled arrays.
• Privileged setters for oracle, interest model, fee recipient, or reserve factor.
• Token transfers that ignore fee-on-transfer behavior.
• Upgradeable storage layout and initializer patterns.
• Functions that update accounting indexes.

Static findings become fuzzing targets. For example, if Slither flags an external call before a state write in a rewards contract, the invariant campaign should include a malicious receiver actor and a conservation property for funded rewards.

8. Halmos and Symbolic Testing

Halmos is useful for narrow properties where the important question is path feasibility rather than broad state exploration. Examples:

• Can healthFactor(account) >= 1e18 while account equity is negative?
• Can rounding produce zero shares for a nonzero deposit above the documented minimum?
• Can two different governance operations hash to the same operation ID?
• Can a fee calculation exceed the configured maximum basis points?

Symbolic tools are not magic. They work best when the target function is small, dependencies are mocked, and the property is precise. Use them to harden arithmetic and authorization paths that fuzzers struggle to hit reliably.

9. Invariant Design for Common DeFi Systems

Lending Markets

Core invariants:

• Total supplier claims do not exceed cash plus borrows minus reserves.
• A borrow cannot make an account unhealthy unless the protocol explicitly allows it.
• Liquidation improves or preserves protocol solvency.
• Interest indexes are monotonic.
• Reserve factor and protocol fee extraction cannot exceed configured caps.
• Oracle staleness prevents new borrows or liquidations.

Example solvency property:

function invariant_cashPlusBorrowsCoversSuppliers() public {
    uint256 assets = market.cash() + market.totalBorrows() - market.reserves();
    uint256 liabilities = market.totalSupplyShares() * market.exchangeRate() / 1e18;
    assertGe(assets + roundingTolerance, liabilities);
}

AMMs

Core invariants:

• Swaps preserve or increase fee-adjusted k.
• LP token supply tracks proportional ownership of reserves.
• Protocol fees cannot be minted from stale reserves.
• Oracle accumulators cannot be updated twice for the same time interval.
• Skim/sync paths cannot steal value from LPs.

Precision matters. A strict equality invariant will fail because integer math rounds. Use an explicit tolerance and make it small enough to catch real leakage.

function invariant_kDoesNotDecreaseBeyondTolerance() public {
    uint256 currentK = pair.reserve0() * pair.reserve1();
    assertGe(currentK + 10, ghostLastK);
}

Staking and Reward Systems

Core invariants:

• Sum of user stake equals protocol total stake.
• Rewards claimed plus rewards remaining never exceeds funded rewards.
• Reward-per-token accumulators are monotonic.
• Users cannot claim rewards for time before they staked.
• Emergency withdrawal cannot leave reward debt reusable.

Reward accounting bugs often require a sequence like stake, checkpoint, transfer, withdraw, donate rewards, restake, claim. This is exactly the type of multi-step path that invariant fuzzing is designed to find.

ERC-4626 Vaults

Core invariants:

• previewDeposit, previewMint, previewWithdraw, and previewRedeem are internally consistent.
• Share price cannot be inflated by donations beyond documented behavior.
• First depositor cannot force later depositors to receive zero shares.
• Total accounted assets match strategy balances within tolerance.
• Fees cannot make share conversion violate ERC-4626 rounding expectations.

10. Oracle and Market Assumptions

Many false positives come from unrealistic oracle behavior. Many false negatives come from overly trusted oracle behavior. The right model is adversarial but bounded.

For a Chainlink-like price feed, model:

• stale prices,
• zero or negative answers,
• decimals mismatches,
• sudden but bounded price moves,
• sequencer downtime for L2 deployments,
• delayed update windows.

Example handler:

function updatePrice(uint256 rawPrice, uint256 age) external {
    uint256 price = bound(rawPrice, 500e8, 2_000e8);
    uint256 updatedAt = block.timestamp - bound(age, 0, 2 hours);
    oracle.setLatestAnswer(price, updatedAt);
}

Do not let the fuzzer set price to zero unless the protocol is expected to handle broken feeds. Do include stale and extreme-but-plausible values because production failures often live at those edges.

11. Handler Anti-Patterns

Avoid these patterns:

• Only happy paths: handlers that skip every call likely to revert.
• Over-bounding: constraints so narrow that the exploit state is unreachable.
• No malicious receivers: missing callback actors for ERC-777, ERC-721, ERC-1155, ETH transfers, and custom hooks.
• No privileged actors: governance, keeper, oracle, and fee-recipient paths are left unfuzzed.
• No ghost accounting: invariants compare protocol variables only to other protocol variables, so correlated accounting bugs go undetected.
• Too many assumptions: vm.assume filters away the bug instead of modeling a real-world precondition.

The harness should be adversarial but honest. It should not violate the protocol's documented external assumptions, but it should push every allowed behavior to its boundary.

12. From Counterexample to Fix

When a fuzzer finds a failure, the work is not done. The audit workflow should be:

1. Save the seed, corpus entry, and minimized call sequence.
2. Convert the sequence into a deterministic regression test.
3. Identify whether the invariant is wrong, the harness is unrealistic, or the protocol is vulnerable.
4. Patch the protocol or narrow the documented assumption.
5. Re-run the original sequence and the broader campaign.
6. Add the regression test to CI.

Example regression structure:

function test_regression_withdrawBeforeAccountingBreaksStakeTotal() public {
    attacker.deposit{value: 10 ether}();
    attacker.attackWithdraw(10 ether);

    assertEq(vault.totalStaked(), vault.balanceOf(address(attacker)));
}

Every true positive should end as a readable test that future maintainers understand without replaying fuzzer output.

13. CI Strategy

Invariant campaigns should run at different depths:

Persist corpora between runs. Coverage-guided fuzzers become more effective when they keep interesting sequences. Treat the corpus as an audit artifact.

14. Practical Checklist

• Tooling links and versions are pinned: Echidna, Foundry, Medusa, Slither, Halmos.
• Harness includes multiple actors, malicious receivers, liquidators, keepers, and privileged roles where relevant.
• Ghost accounting independently tracks deposits, borrows, shares, rewards, and fees.
• Oracle model includes stale, delayed, and bounded extreme prices.
• AMM invariants account for fees and rounding tolerances.
• Lending invariants check both account-level health and market-level solvency.
• Staking invariants check funded rewards against claimed plus remaining rewards.
• Counterexamples are minimized and converted to deterministic tests.
• CI has short PR campaigns and longer scheduled campaigns.

15. Conclusion

Economic invariant fuzzing is not a checkbox. It is a modeling exercise. The value comes from encoding the protocol's financial promises in a way that an adversarial transaction generator can challenge repeatedly.

The best results come from layered tooling: Slither to map the code, Foundry to iterate quickly, Echidna and Medusa to search deeper state spaces, and Halmos to prove narrow arithmetic or authorization properties. When those tools are paired with realistic actors, ghost accounting, oracle models, and preserved regression tests, they catch the class of DeFi bugs that ordinary unit tests routinely miss.