Testing

Smart Contract Fuzzing with Echidna: Property-Based Security Testing

05 Oct 2026 — 6 min read

Most security bugs in smart contracts aren't found by reading code — they're found by systematically breaking assumptions. A function you expected to always return a positive number returns zero under specific conditions. An invariant you assumed held under normal conditions breaks when two calls happen in the same block. These are the bugs that manual review misses and unit tests don't cover, because you have to know what to test for.

Echidna is a smart contract fuzzer from Trail of Bits. It systematically generates inputs to break properties you define. You write invariants — conditions that must always be true — and Echidna tries to falsify them by calling your contract functions in random orders with random arguments. When it finds a counterexample, it minimizes it to the smallest possible sequence of calls that demonstrates the failure.

This is property-based security testing, and it catches a different class of bugs than unit tests.

What Fuzzing Means for Smart Contracts

Traditional unit tests are example-based: you pick specific inputs and assert specific outputs. Property-based testing inverts this: you define properties that must hold for ALL inputs, and the fuzzer generates thousands of inputs trying to break those properties.

For smart contracts, useful properties include:

Supply invariants: Total supply always equals the sum of all balances
Balance invariants: No user balance exceeds total supply
Monotonicity: A withdrawable amount never increases without a deposit
Access invariants: Only owner can call admin functions, regardless of call sequence
Arithmetic invariants: No overflow or underflow in token calculations

Echidna doesn't just test single function calls — it generates sequences of function calls, which is critical for finding bugs that only appear through specific state transitions.

Installing Echidna

The simplest installation is via Docker:

docker pull trailofbits/echidna

Or install natively on macOS:

brew install echidna

Or use the pre-built binary from the GitHub releases page. Echidna requires Slither (the static analysis tool) for some features:

pip3 install slither-analyzer

Contract Under Test: A Vault Contract

Let's fuzz a simple vault contract that's more complex than a basic ERC-20 — it has deposit/withdrawal logic and fee calculation:

// contracts/Vault.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;

import "@openzeppelin/contracts/token/ERC20/IERC20.sol";
import "@openzeppelin/contracts/access/Ownable.sol";

contract Vault is Ownable {
    IERC20 public immutable token;
    uint256 public constant FEE_BASIS_POINTS = 30; // 0.3%
    uint256 public constant BASIS_POINTS_DENOMINATOR = 10000;

    mapping(address => uint256) public shares;
    uint256 public totalShares;
    uint256 public accumulatedFees;

    constructor(address _token, address _owner) Ownable(_owner) {
        token = IERC20(_token);
    }

    function deposit(uint256 amount) external {
        require(amount > 0, "Amount must be positive");
        token.transferFrom(msg.sender, address(this), amount);

        uint256 newShares;
        if (totalShares == 0) {
            newShares = amount;
        } else {
            uint256 vaultBalance = token.balanceOf(address(this)) - accumulatedFees;
            newShares = (amount * totalShares) / (vaultBalance - amount);
        }

        shares[msg.sender] += newShares;
        totalShares += newShares;
    }

    function withdraw(uint256 shareAmount) external {
        require(shareAmount > 0, "Share amount must be positive");
        require(shares[msg.sender] >= shareAmount, "Insufficient shares");

        uint256 vaultBalance = token.balanceOf(address(this)) - accumulatedFees;
        uint256 tokenAmount = (shareAmount * vaultBalance) / totalShares;
        uint256 fee = (tokenAmount * FEE_BASIS_POINTS) / BASIS_POINTS_DENOMINATOR;

        shares[msg.sender] -= shareAmount;
        totalShares -= shareAmount;
        accumulatedFees += fee;

        token.transfer(msg.sender, tokenAmount - fee);
    }

    function collectFees() external onlyOwner {
        uint256 fees = accumulatedFees;
        accumulatedFees = 0;
        token.transfer(owner(), fees);
    }
}

There's a bug in this contract — let's see if Echidna finds it.

Writing Echidna Properties

Echidna properties are Solidity functions that return bool and start with echidna_. Create a test contract that extends or wraps your contract:

// test/VaultEchidna.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;

import "../contracts/Vault.sol";
import "../contracts/MockERC20.sol";

contract VaultEchidna {
    Vault vault;
    MockERC20 token;

    address constant OWNER = address(0x41414141);
    address constant USER1 = address(0x42424242);
    address constant USER2 = address(0x43434343);

    constructor() {
        token = new MockERC20("Test", "TST", 18);
        vault = new Vault(address(token), OWNER);

        // Give users tokens
        token.mint(USER1, 1_000_000e18);
        token.mint(USER2, 1_000_000e18);

        // Approve vault
        token.approveAs(USER1, address(vault), type(uint256).max);
        token.approveAs(USER2, address(vault), type(uint256).max);
    }

    // Property 1: Total shares always reflect total deposits
    function echidna_total_shares_consistent() public view returns (bool) {
        if (vault.totalShares() == 0) return true;

        uint256 vaultBalance = token.balanceOf(address(vault)) - vault.accumulatedFees();
        // Each share represents some positive token amount
        return vaultBalance > 0;
    }

    // Property 2: No individual share count exceeds total shares
    function echidna_individual_shares_le_total() public view returns (bool) {
        return vault.shares(USER1) <= vault.totalShares() &&
               vault.shares(USER2) <= vault.totalShares();
    }

    // Property 3: Vault balance always covers outstanding shares + fees
    function echidna_vault_solvent() public view returns (bool) {
        uint256 balance = token.balanceOf(address(vault));
        uint256 fees = vault.accumulatedFees();
        return balance >= fees;
    }

    // Property 4: After withdraw, user gets tokens back
    // (this is tested through the invariant on total shares + balance)
    function echidna_total_supply_conserved() public view returns (bool) {
        uint256 user1Balance = token.balanceOf(USER1);
        uint256 user2Balance = token.balanceOf(USER2);
        uint256 vaultBalance = token.balanceOf(address(vault));
        uint256 ownerBalance = token.balanceOf(OWNER);

        // Total tokens in system should not exceed initial mint
        // (fees are real tokens redistributed to owner, so we track all)
        return user1Balance + user2Balance + vaultBalance + ownerBalance <= 2_000_000e18;
    }
}

Configuring Echidna

Create an echidna.yaml configuration file:

# echidna.yaml
testMode: "property"
testLimit: 50000
seqLen: 100
shrinkLimit: 5000

# Corpus directory (saves interesting sequences)
corpusDir: "echidna-corpus"

# Contract addresses that Echidna can call
deployer: "0x41414141"
sender: ["0x41414141", "0x42424242", "0x43434343"]

# Coverage-guided fuzzing
coverageFile: "coverage.txt"

# Gas limit per transaction
gasLimit: 10000000

Key configuration options:

testLimit: Number of test cases to generate (more = better coverage, slower)
seqLen: Max length of call sequences (longer = finds more complex bugs)
shrinkLimit: How hard to minimize counterexamples

Running Echidna

# Basic run
echidna test/VaultEchidna.sol --contract VaultEchidna --config echidna.yaml

# With Docker
docker run --rm -v $(pwd):/code trailofbits/echidna \
  /code/test/VaultEchidna.sol \
  --contract VaultEchidna \
  --config /code/echidna.yaml

Expected output when a bug is found:

Analyzing contract: test/VaultEchidna.sol:VaultEchidna
echidna_total_shares_consistent: PASSED
echidna_individual_shares_le_total: PASSED
echidna_vault_solvent: PASSED
echidna_total_supply_conserved: failed!
  Call sequence:
    deposit(1000000000000000000) from: 0x42424242
    deposit(999999999999999999) from: 0x43434343
    withdraw(999999999999999999) from: 0x43434343

  Event sequence: Panic(17) (code 17 = arithmetic underflow/overflow)

Echidna found the bug in our vault contract: the deposit calculation on line newShares = (amount * totalShares) / (vaultBalance - amount) subtracts amount from vaultBalance AFTER the transfer has already happened. When the second user deposits, vaultBalance already includes their deposit, so vaultBalance - amount double-counts it.

Interpreting Results and Fixing Bugs

When Echidna reports a failure, it gives you the minimal call sequence. Work through it manually:

USER2 deposits 1e18 tokens → vault has 1e18, USER2 has 1e18 shares
USER3 deposits ~1e18 tokens → vault tries to calculate shares, but vaultBalance - amount is nearly zero (underflow)

The fix:

function deposit(uint256 amount) external {
    require(amount > 0, "Amount must be positive");

    uint256 vaultBalanceBefore = token.balanceOf(address(this)) - accumulatedFees;
    token.transferFrom(msg.sender, address(this), amount);

    uint256 newShares;
    if (totalShares == 0) {
        newShares = amount;
    } else {
        // Use balance BEFORE the transfer for the share calculation
        newShares = (amount * totalShares) / vaultBalanceBefore;
    }

    shares[msg.sender] += newShares;
    totalShares += newShares;
}

Writing Better Invariants

The quality of your fuzzing depends entirely on the quality of your invariants. Common patterns:

Conservation invariants — tokens don't appear from nowhere:

function echidna_no_token_creation() public view returns (bool) {
    return token.totalSupply() == INITIAL_SUPPLY;
}

Monotonic invariants — values that should only increase or decrease:

function echidna_accumulated_fees_monotonic() public view returns (bool) {
    // Fees should never decrease (only collectFees resets them, called by owner)
    return vault.accumulatedFees() >= lastKnownFees;
}

Access control invariants — restricted state should only change through authorized paths:

function echidna_only_owner_can_drain() public view returns (bool) {
    // If vault balance decreased without user withdrawals, something is wrong
    // (simplified — real implementation would track state)
    return token.balanceOf(address(vault)) >= minimumExpectedBalance;
}

Echidna vs. Foundry Fuzzing: A Comparison

Both tools do property-based testing but with different strengths:

Feature	Echidna	Foundry Fuzz
Language	Solidity properties	Solidity fuzz tests
Call sequences	Multi-call sequences	Single-function only
Invariant testing	Native (property mode)	Via invariant tests
Corpus saving	Built-in	Limited
Integration	Standalone tool	Built into forge
Speed	Moderate	Fast
Setup complexity	Higher	Lower

Use Foundry's built-in fuzz testing for individual function properties. Use Echidna when you need stateful fuzzing — testing that invariants hold across arbitrary sequences of calls. For DeFi protocols with complex state machines, Echidna is the stronger tool.

Integrating Echidna into CI

# .github/workflows/echidna.yml
name: Echidna Security Tests

on:
  push:
    branches: [main]
  pull_request:

jobs:
  echidna:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Run Echidna
        uses: crytic/echidna-action@v2
        with:
          files: test/VaultEchidna.sol
          contract: VaultEchidna
          config: echidna.yaml

      - name: Upload corpus
        if: always()
        uses: actions/upload-artifact@v3
        with:
          name: echidna-corpus
          path: echidna-corpus/

The crytic/echidna-action handles Docker and dependency setup automatically.

When Echidna Finds Nothing

If Echidna runs to completion without finding a counterexample, that means one of two things:

Your invariants are correct and hold under all tested conditions (good)
Your invariants are too weak to catch bugs that exist (bad)

After every Echidna run, review your properties: could you write a property that's harder to satisfy? Could you add more actors? Could you increase sequence length?

The goal isn't to run Echidna once and declare victory — it's to build a corpus of properties that grows with the protocol's complexity. Start with the obvious supply conservation invariants, then add protocol-specific invariants as you understand the system better.

Security researchers who've audited major DeFi protocols consistently say the same thing: the protocols that got hacked didn't lack code quality, they lacked systematic property verification. Echidna is how you get that verification.