Echidna

Echidna is a property-based fuzzer for Ethereum smart contracts built by Trail of Bits. It generates random sequences of transactions to find violations of user-defined properties. Unlike static analysis (Slither) or symbolic execution (Mythril), Echidna executes real EVM bytecode with coverage-guided mutation — it learns which inputs reach new code paths and explores deeper.

What You Probably Got Wrong

LLMs treat Echidna like "just run the fuzzer." The hard part is designing properties, not invoking the tool.

• Property design is the entire game — Running echidna . on a contract with weak properties proves nothing. A property that always returns true passes 100% of the time and catches 0% of bugs. Invest time in thinking about what invariants your protocol must maintain.
• Echidna is stateful, not stateless — Unlike Foundry fuzz tests that run one function with random inputs, Echidna generates sequences of multiple transactions. It calls function A, then B, then C, checking properties after each. This is how it catches bugs that require specific state setup.
• Assertion mode catches panics, not properties — In assertion mode, Echidna looks for assert() failures and Solidity panics (division by zero, overflow in unchecked blocks, array out of bounds). It does NOT check echidna_* functions. These are two different testing strategies.
• echidna_ prefix is mandatory in property mode — Properties must be public/external functions starting with echidna_ that take no arguments and return bool. Naming a function check_invariant() does nothing — Echidna ignores it.
• Corpus is your most valuable artifact — The corpus directory contains minimized transaction sequences that achieve new coverage. Save it between runs. Share it with your team. It makes subsequent runs converge faster.
• Echidna does NOT support Foundry cheatcodes — vm.prank, vm.deal, vm.warp do not work in Echidna. For time-dependent properties, use hevm-compatible cheatcodes or restructure your test harness with helper functions.
• Shrinking is not optional — When Echidna finds a failing sequence of 50 transactions, shrinking reduces it to the minimal reproducing sequence (often 2-3 calls). Without shrinking, debugging is painful.
• More runs does not mean better coverage — 1 million random transactions with bad properties are worth less than 10,000 with good properties. Coverage-guided mutation helps, but only if your test harness exposes meaningful state transitions.

Installation