Echidna is a smart contract fuzzer developed by Trail of Bits that specializes in property-based testing for Ethereum contracts. Unlike random fuzzers that just look for crashes, Echidna tests user-defined properties (invariants) by generating sequences of transactions and checking if any sequence can violate the specified properties. It uses grammar-based fuzzing and coverage-guided mutation to efficiently explore contract state spaces, making it one of the most powerful tools for finding logic bugs in DeFi protocols.

How Echidna Works

Echidna operates in three phases:

1. Property definition: You write Solidity functions that return true if an invariant holds
2. Transaction generation: Echidna generates random sequences of function calls with random parameters
3. Property checking: After each sequence, Echidna checks if any property returns false

1contract TokenTest {
2    Token token;
3    
4    constructor() {
5        token = new Token();
6    }
7    
8    // Echidna property: must always return true
9    function echidna_total_supply_constant() public view returns (bool) {
10        return token.totalSupply() == 1000000;
11    }
12    
13    // Echidna will call transfer() with random addresses and amounts
14    function transfer(address to, uint256 amount) public {
15        token.transfer(to, amount);
16    }
17}

If Echidna finds a sequence of calls that makes echidna_total_supply_constant return false, it reports the exact sequence as a counterexample.

Installation and Usage

1# Install via pip (recommended)
2pip install echidna
3
4# Or via Docker
5docker pull trailofbits/echidna
6
7# Run on a contract
8echidna contract.sol --contract TestContract
9
10# With config file
11echidna . --config echidna.yaml

Basic config file (echidna.yaml):

1testMode: property
2testLimit: 50000
3seqLen: 100
4deployer: "0x10000"
5sender: ["0x10000", "0x20000", "0x30000"]

Writing Echidna Properties

Echidna recognizes properties by naming convention:

1contract EchidnaTest {
2    // Properties: functions starting with echidna_ that return bool
3    function echidna_balance_never_negative() public view returns (bool) {
4        // Solidity uint256 can't be negative, but you might check invariants like:
5        return address(this).balance >= minimumBalance;
6    }
7    
8    // Or check protocol invariants
9    function echidna_pool_solvent() public view returns (bool) {
10        return pool.totalAssets() >= pool.totalLiabilities();
11    }
12}

Property types:

• echidna_*: Must always return true
• echidna_revert_*: Must always revert (for testing access control)

Echidna vs Other Fuzzers

Echidna's strength is its sophisticated shrinking—when it finds a bug, it minimizes the counterexample to the shortest possible sequence.

Stateful Invariant Testing

Echidna excels at stateful testing where bugs emerge from specific sequences:

1contract LendingTest {
2    Lending lending;
3    
4    // Setup initial state
5    constructor() {
6        lending = new Lending();
7        lending.deposit{value: 100 ether}();
8    }
9    
10    // Actions Echidna can take
11    function deposit(uint256 amount) public {
12        lending.deposit{value: amount}();
13    }
14    
15    function borrow(uint256 amount) public {
16        lending.borrow(amount);
17    }
18    
19    function repay(uint256 amount) public {
20        lending.repay{value: amount}();
21    }
22    
23    // Invariant: protocol should never be insolvent
24    function echidna_solvent() public view returns (bool) {
25        return address(lending).balance >= lending.totalBorrowed();
26    }
27}

Echidna might find a sequence like:

1. deposit(1 ether)
2. borrow(0.9 ether)
3. deposit(0.1 ether)
4. borrow(0.5 ether) ← breaks solvency!

Advanced Features

Coverage-Guided Fuzzing

Echidna tracks code coverage and prioritizes inputs that explore new paths:

1coverage: true
2corpusDir: "corpus"

The corpus directory saves interesting inputs for future runs, improving efficiency over time.

Assertion Mode

Test for specific assertions instead of properties:

1testMode: assertion

1function testWithdraw(uint256 amount) public {
2    uint256 balanceBefore = token.balanceOf(address(this));
3    vault.withdraw(amount);
4    assert(token.balanceOf(address(this)) == balanceBefore + amount);
5}

Optimization Mode

Find inputs that maximize or minimize a value:

1testMode: optimization

1function echidna_optimize_gas() public returns (int256) {
2    // Echidna will find inputs that maximize this value
3    return int256(gasleft());
4}

Real-World Example: Finding a Reentrancy Bug

1contract VulnerableVault {
2    mapping(address => uint256) public balances;
3    
4    function deposit() external payable {
5        balances[msg.sender] += msg.value;
6    }
7    
8    function withdraw() external {
9        uint256 amount = balances[msg.sender];
10        (bool success,) = msg.sender.call{value: amount}("");
11        require(success);
12        balances[msg.sender] = 0;  // State update after external call!
13    }
14}
15
16contract EchidnaAttack {
17    VulnerableVault vault;
18    
19    constructor() {
20        vault = new VulnerableVault();
21    }
22    
23    function deposit() public payable {
24        vault.deposit{value: msg.value}();
25    }
26    
27    function attack() public {
28        vault.withdraw();
29    }
30    
31    receive() external payable {
32        if (address(vault).balance > 0) {
33            vault.withdraw();  // Reentrant call
34        }
35    }
36    
37    // This property will fail due to reentrancy
38    function echidna_vault_solvent() public view returns (bool) {
39        return address(vault).balance >= vault.balances(address(this));
40    }
41}

Echidna discovers the attack sequence: deposit() → attack() → reentrancy drains funds.

Integration with CI/CD

1# GitHub Actions example
2- name: Run Echidna
3  uses: crytic/echidna-action@v2
4  with:
5    files: .
6    contract: TestContract
7    config: echidna.yaml

Best Practices

1. Start simple: Begin with basic invariants, add complexity as needed
2. Bound inputs: Use require() to constrain parameters to realistic ranges
3. Multiple senders: Configure multiple sender addresses to test access control
4. Long sequences: Increase seqLen for complex state machine bugs
5. Save corpus: Persist the corpus directory between runs for faster testing
6. Combine with Medusa: Medusa offers parallel fuzzing that complements Echidna

Limitations

EVM-only: Echidna works on EVM bytecode, not other chains natively.

Property specification: You must know what properties to test—Echidna won't discover invariants for you.

External dependencies: Mocking external contracts requires setup work.

Time-dependent bugs: Testing time-based logic requires careful configuration of block timestamps.

Echidna is a cornerstone of smart contract security testing, used by leading security firms and protocols to find bugs before deployment. Combined with static analysis and manual review, it forms a robust security testing pipeline.