Echidna tutorial: advanced stateful fuzzing campaigns

You've run Echidna before. You've written a basic property, watched it churn through transactions, maybe caught a bug or two. Now you want to push it further. This tutorial covers the advanced stuff — config tuning, corpus management, and getting real coverage data out of your campaigns.

If you're completely new to Echidna, start with our stateful fuzzing explainer first. This picks up where the basics leave off.

Why advanced config matters

Echidna's default settings are fine for small contracts with shallow state spaces. But DeFi protocols aren't small or shallow. A lending protocol might need 15+ transactions in the right order to reach an interesting state, and defaults won't get you there.

The difference between a campaign that finds nothing and one that catches a critical bug often comes down to three config values.

Config tuning: the big three

seqLen (sequence length)

This controls the maximum number of transactions in a single test sequence.

seqLen: 50

Default is 100, but that's often too long for focused testing. Here's the thing: longer sequences take longer to shrink when they find a failure. If your bug needs 5 calls to trigger but Echidna finds it in a 100-call sequence, shrinking might take minutes.

My rule of thumb:

• Simple token contracts: 10-20
• Lending protocols: 30-50
• Complex multi-step flows (liquidations, governance): 50-100

Start shorter and increase if coverage plateaus.

testLimit

Total number of test sequences to run.

testLimit: 500000

Default is 50000. That's not enough for anything beyond trivial contracts. For real audits, I run 500K minimum. For critical paths, 2M+. Yes, it takes longer. But stateful fuzzing is a numbers game — more sequences means more state combinations explored.

shrinkLimit

How hard Echidna tries to minimize a failing sequence.

shrinkLimit: 10000

Default is 5000. Bump it up if you're getting long, hard-to-read failing sequences. The tradeoff is time. More shrink attempts means slower reporting, but the counterexamples you get back are much cleaner.

Full config file

Here's a production-ready echidna.yaml for a lending protocol:

testMode: "property"
testLimit: 500000
seqLen: 50
shrinkLimit: 10000
contractAddr: "0x00a329c0648769A73afAc7F9381E08FB43dBEA72"
deployer: "0x00a329c0648769A73afAc7F9381E08FB43dBEA72"
sender: ["0x10000", "0x20000", "0x30000"]
balanceAddr: 0xffffffff
balanceContract: 0xffffffff
codeSize: 0x6000
coverage: true
corpusDir: "corpus"
cryticArgs: ["--foundry-compile-all"]
filterBlacklist: true
filterFunctions: ["excludeThisFunction"]

Let's break down the less obvious ones.

sender

sender: ["0x10000", "0x20000", "0x30000"]

Echidna uses these addresses as transaction senders. Three is usually enough. It lets the fuzzer test interactions between different users. More senders means more combinations but slower exploration of each user's state space.

filterFunctions

filterBlacklist: true
filterFunctions: ["excludeThisFunction", "anotherOne"]

When filterBlacklist is true, Echidna skips functions in the list. Use this to exclude admin-only setup functions that would just waste fuzzing cycles. You can also set filterBlacklist: false to create a whitelist, only fuzzing the functions you specify.

Property mode vs assertion mode

Echidna supports two main testing approaches.

Property mode (default)

You write functions that return bool. Echidna calls them after every transaction sequence:

function echidna_solvency() public view returns (bool) {
    return totalAssets() >= totalLiabilities();
}

Properties run in a read-only context. They can't modify state. That's by design. Properties should be pure checks.

Assertion mode

testMode: "assertion"

In assertion mode, Echidna looks for assert() statements inside regular functions that revert:

function test_withdraw(uint256 amount) public {
    uint256 balanceBefore = token.balanceOf(address(this));
    vault.withdraw(amount);
    uint256 balanceAfter = token.balanceOf(address(this));

    assert(balanceAfter >= balanceBefore);
}

Assertion mode is powerful for testing specific operations, not just global invariants. If the assert fires, Echidna reports the full call sequence that led there.

When to use which? Properties for system-wide invariants (solvency, access control). Assertions for operation-specific correctness (withdraw gives you the right amount, liquidation clears debt properly).

Multi-contract testing: the lending protocol example

Real protocols have multiple interacting contracts. Here's how to set up a multi-contract Echidna test for a simple lending protocol.

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

import "../src/LendingPool.sol";
import "../src/PriceOracle.sol";
import "../src/InterestRateModel.sol";

contract LendingFuzzTest {
    LendingPool pool;
    PriceOracle oracle;
    InterestRateModel rateModel;
    MockERC20 collateralToken;
    MockERC20 debtToken;

    constructor() payable {
        collateralToken = new MockERC20("COL", 18);
        debtToken = new MockERC20("DEBT", 18);
        oracle = new PriceOracle();
        rateModel = new InterestRateModel();

        pool = new LendingPool(
            address(oracle),
            address(rateModel)
        );

        // Seed initial state
        collateralToken.mint(address(this), 1_000_000e18);
        debtToken.mint(address(pool), 500_000e18);
        collateralToken.approve(address(pool), type(uint256).max);

        // Set initial prices
        oracle.setPrice(address(collateralToken), 2000e8);
        oracle.setPrice(address(debtToken), 1e8);
    }

    // === Fuzzer entry points ===

    function deposit(uint256 amount) external {
        amount = bound(amount, 1, collateralToken.balanceOf(address(this)));
        pool.deposit(address(collateralToken), amount);
    }

    function borrow(uint256 amount) external {
        amount = bound(amount, 1, 100_000e18);
        pool.borrow(address(debtToken), amount);
    }

    function repay(uint256 amount) external {
        amount = bound(amount, 1, pool.getUserDebt(address(this)));
        debtToken.approve(address(pool), amount);
        pool.repay(address(debtToken), amount);
    }

    function manipulatePrice(uint256 newPrice) external {
        // Let the fuzzer move the oracle price
        newPrice = bound(newPrice, 100e8, 10_000e8);
        oracle.setPrice(address(collateralToken), newPrice);
    }

    function accrueInterest() external {
        pool.accrueInterest();
    }

    // === Properties ===

    function echidna_pool_solvency() public view returns (bool) {
        // Pool should never owe more than it holds
        return debtToken.balanceOf(address(pool)) >= pool.totalBorrows()
            || pool.totalBorrows() == 0;
    }

    function echidna_no_bad_debt() public view returns (bool) {
        // No position should have debt exceeding collateral value
        uint256 collValue = pool.getCollateralValue(address(this));
        uint256 debtValue = pool.getDebtValue(address(this));

        if (debtValue > 0 && collValue == 0) {
            return false; // Bad debt: debt with zero collateral
        }
        return true;
    }

    function echidna_interest_monotonic() public view returns (bool) {
        // Total borrows should only grow from interest, never shrink randomly
        return pool.totalBorrows() >= pool.lastRecordedBorrows()
            || pool.totalBorrows() == 0;
    }

    // === Helper ===
    function bound(uint256 x, uint256 min, uint256 max) internal pure returns (uint256) {
        if (max <= min) return min;
        return min + (x % (max - min + 1));
    }
}

Key patterns here:

1. Constructor does all deployment. Echidna deploys one contract (your test wrapper). Everything else gets deployed inside the constructor.
2. Fuzzer entry points are thin wrappers. They take raw fuzzer input, bound it to valid ranges, and call the target. This prevents wasting cycles on obviously-reverting calls.
3. Properties check system-level invariants. Solvency, no bad debt, monotonic interest. These should hold regardless of what call sequence the fuzzer generates.

Corpus management

The corpus is where Echidna saves interesting transaction sequences, ones that increased code coverage or got close to breaking a property.

corpusDir: "corpus"

After a campaign, you'll find two directories:

corpus/
  coverage/        # Sequences that increased coverage
  reproducers/     # Sequences that broke properties

Why this matters: You can commit the corpus to your repo and Echidna will replay those sequences at the start of the next campaign. This means:

• New campaigns don't start from scratch
• Coverage ratchets forward across runs
• CI can build on previous campaign results

# Run with existing corpus
echidna test/LendingFuzzTest.sol --config echidna.yaml

Echidna automatically loads from corpusDir if it exists. Pro tip: periodically clean out old corpus files if the contract interface changes. Stale sequences just cause reverts.

Reading coverage reports

Enable coverage:

coverage: true

After a run, Echidna dumps an HTML coverage report. Open it and look for red lines. Those are uncovered branches.

Common reasons for low coverage:

• Missing entry points. If your test contract doesn't expose a function, Echidna can't call it. Make sure every relevant public function has a wrapper.
• Tight bounds. If you over-constrain your bound() calls, the fuzzer can't explore edge cases. Balance validity with exploration.
• Unreachable states. Some states need a specific transaction ordering. Increase seqLen or add helper functions that set up intermediate states.

If coverage is stuck below 70%, something's wrong with your test setup. Don't just increase testLimit and hope. Fix the test contract.

Using crytic-compile

Echidna uses crytic-compile under the hood for compilation. For Foundry projects:

cryticArgs: ["--foundry-compile-all"]

For Hardhat:

cryticArgs: ["--hardhat-ignore-compile"]

If you hit compilation issues, try running crytic-compile standalone first:

crytic-compile . --foundry-compile-all

This helps isolate whether the problem is compilation or Echidna config.

Advanced patterns

Time-dependent bugs

Some bugs only appear after time passes. Use Echidna's block advancement:

function advanceTime(uint256 delta) external {
    delta = bound(delta, 1, 365 days);
    // Echidna advances block.timestamp between calls
    // This function is just a no-op that lets time pass
}

Multi-sender testing

Deploy separate action contracts for each actor:

contract BorrowerActions {
    LendingPool pool;

    constructor(LendingPool _pool) { pool = _pool; }

    function borrow(uint256 amount) external {
        pool.borrow(amount);
    }
}

contract LiquidatorActions {
    LendingPool pool;

    constructor(LendingPool _pool) { pool = _pool; }

    function liquidate(address user) external {
        pool.liquidate(user);
    }
}

Ghost variables for tracking

Track values across calls to write richer properties:

uint256 totalDeposited;
uint256 totalWithdrawn;

function deposit(uint256 amount) external {
    amount = bound(amount, 1, 1e24);
    pool.deposit(amount);
    totalDeposited += amount;
}

function echidna_accounting() public view returns (bool) {
    return totalDeposited >= totalWithdrawn;
}

Comparison with Medusa

Both are excellent fuzzing tools. See the full Echidna vs Medusa comparison for details, but the quick version:

• Echidna has a more mature corpus system and better shrinking
• Medusa has native parallelism (multiple workers out of the box)
• Echidna is Haskell, Medusa is Go, which matters for debugging and contributions
• Both support property mode and assertion mode

For maximum coverage, run both. The Chimera framework lets you write a single test setup that works with either tool.

CI integration

Add Echidna to your CI pipeline:

# .github/workflows/echidna.yml
name: Echidna
on: [push, pull_request]
jobs:
  echidna:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: crytic/echidna-action@v2
        with:
          files: test/LendingFuzzTest.sol
          config: echidna.yaml
          crytic-args: --foundry-compile-all

Keep CI campaigns short (testLimit: 50000) for fast feedback. Run longer campaigns nightly or before releases.

What to do next

You've got the advanced toolkit now. Here are your next steps:

• Study how invariant testing principles apply to your specific protocol
• Read about combining fuzzing with formal verification for deeper assurance
• Try Halmos for the properties that fuzzing struggles to reach
• Look into coverage-guided fuzzing theory to understand why corpus management matters

The goal isn't 100% coverage. It's catching the bugs that matter before someone else does.

Get a professional fuzzing audit

Try Recon Pro