Smart Contract Fuzzing: Echidna, Medusa or Foundry for Which Situation

Stateless or stateful: the decision path

In smart contract fuzzing, a tool feeds generated inputs into deployed bytecode and checks that stated properties survive. The three tools most teams shortlist share that definition and little else. Foundry's forge test runs a fuzz test as one call with random arguments, 256 times by default. Echidna and Medusa run sequences of calls against a persistent state, 100 calls per sequence by default, and reset only when the sequence ends. Foundry's invariant mode does the same with a default depth of 500 calls per run. The first choice is therefore not "which fuzzer" but "which shape of bug".

A stateless fuzz test answers whether one function behaves for every input: a math library, a rounding helper, a pure fee formula. A stateful fuzzing campaign, called invariant testing in Foundry and property testing in Echidna, answers whether a property still holds after any sequence of deposits, borrows, liquidations and transfers. A bug in call ordering can escape tests that exercise each operation in isolation.

Work through the path in this order.

1. Single function with no dependence on prior calls. Write a Foundry fuzz test. If the failing input is rare, such as a comparison that is false for one value in a range of 2²⁵⁶, random sampling will not hit it. Hand the same test to a symbolic tool, covered later in this guide.
2. Accounting that must balance across calls. Vault shares against assets, an AMM's constant product, a lending pool's total debt against the sum of positions. This is stateful territory. Start with Foundry invariant tests if the team already lives in Foundry and wants results inside the normal test run. Move the same properties to Echidna or Medusa when a campaign needs to run for hours with a persistent corpus.
3. A system already deployed. Fork it. Echidna and Medusa read chain state through an RPC endpoint and fuzz against real balances and real integrations, and Foundry's fork mode does the same for invariant tests.
4. An audit on the calendar. Write the suite once in a tool-neutral layout so the auditor can run it in their fuzzer of choice. Recon's Chimera framework exists for exactly that: one property suite, run under Foundry, Echidna, Medusa, Halmos or Kontrol.

Define the protocol invariants before choosing the engine.

Per-tool matrix: setup, shrinking, coverage and the Slither dependency

All three tools are actively maintained. On September 2, 2026, Echidna's latest release was 2.3.3 (July 27, 2026), Medusa's was 1.5.1 (March 11, 2026) and Foundry's was 1.8.1 (August 28, 2026). Echidna and Medusa come from Trail of Bits' Crytic team, and Foundry is maintained by Paradigm and the foundry-rs contributors. The matrix below is drawn from each tool's configuration reference and release notes as of those versions.

Trail of Bits reported similar coverage and corpus size for Echidna and Medusa in February 2025. Recon, which sells cloud campaigns, reports roughly 3 times faster coverage with Medusa on an 8-core machine and stronger shrinking with Echidna. Dacian's challenge set ends in a tie on 12 of 14 exercises.

The benchmarks use different harnesses and machines. Compare coverage growth and shrinking on your own suite before treating a speed claim as a selection rule.

The default budget row explains most "fuzzing found nothing" complaints: 256 runs of one call is a smoke test, not a campaign. Echidna's 50,000 transactions end in minutes on a small target. Production suites set very different numbers. Aave's invariant suite ships an Echidna config with testLimit of 20,000,000, seqLen of 300 and shrinkLimit of 10,000, and a medusa.json with testLimit and timeout at 0 so the campaign runs until someone stops it. Centrifuge's Echidna config sets shrinkLimit to 100,000.

The coverage row explains the second complaint, "it never reaches the interesting branch". Echidna and Medusa are coverage-guided out of the box. Foundry's fuzzer is random plus a dictionary of interesting values unless corpus_dir is configured, which turns on coverage guidance, persists coverage-increasing inputs and enables the forge fuzz subcommands for replaying, showing and minimizing a corpus.

Long campaigns need a persistent corpus and a harness that can reach every relevant contract. Compare those controls in the matrix before changing engines.

Compare stateful fuzzing tools by harness input and campaign output.

Slither, in the fourth row, is a practical setup cost. Both Crytic fuzzers call Slither to mine constants from the code, which the Medusa documentation says greatly improve system coverage. That means a Python toolchain and a compiler version that Slither can drive through crytic-compile. Foundry projects work with both, but a Hardhat project with unusual remappings often loses an afternoon here. Foundry needs nothing beyond itself.

What the largest protocols actually run

Method

Measured

September 2, 2026

Population

30 largest DefiLlama protocol records by positive total value locked with a website URL; exclude CEX, Chain and Bridge

Repository selection

Use DefiLlama GitHub metadata and a manually maintained candidate list; select the first existing candidate

Detection

Recursive repository trees plus code searches for Echidna, Medusa and Foundry fuzzing artifacts

Denominator

22 scannable EVM repositories; 2 non-EVM projects and 6 without an identified public repository

Reproduction uses seo/research/fuzz-suite-survey.py and saved output seo/research/fuzz-suite-survey-2026-09-02.json are kept in the site repository and are not published as web pages. The figures retain their original measurement date.

Results

Among the 22 EVM repositories we could scan, 12 keep a stateful suite and 15 keep some form of fuzz test. Foundry invariant tests appear in 9 of the 12 stateful suites, Echidna in 4 and Medusa in 3. The three teams that run two or more engines, Aave, Centrifuge and Veda, all run at least one Crytic fuzzer next to Foundry. Certora specs or CI jobs appear in 6 of the 22 repositories, at Aave, Morpho Blue, EigenLayer, ether.fi, Spark Liquidity Layer and Veda, so formal verification and fuzzing are complements rather than alternatives for the teams that can afford both.

Limits

• Repository selection uses a candidate list, so a missed or differently named repository can affect the classification.
• Artifact presence does not prove that tests run in CI or cover the deployed revision.
• Inherited harnesses count as present. The scan does not attribute their authorship to the protocol team.

1. The largest suites were written by outside specialists and then kept in the protocol's tree. Aave's actor-based suite was built by Enigma Dark under an engagement from BGD Labs, Centrifuge's Chimera layout came with a 2025 Recon engagement, and PancakeSwap's Echidna harnesses are the ones Trail of Bits wrote for Uniswap v3.
2. The repositories with no fuzzing at all are mostly tokenized assets and older CDP code, where the contract surface is small and the risk sits in custody and governance rather than in call ordering.

What fuzzing finds that manual review misses

A fuzzer can expose failures that require a precise combination of values or a long sequence of individually valid calls.

Trail of Bits' first engagement devoted entirely to invariants, nine weeks with Curvance in 2024, produced 216 invariants and 13 critical findings. One of them had survived several earlier reviews because the unit tests asserted an incorrect postcondition and so certified the bug. A six-week Badger DAO eBTC engagement by Recon wrote more than 40 properties, confirmed findings from Spearbit's manual review and turned up previously undisclosed bugs, but only after the harness reached 100 percent line coverage. Before that point the fuzzer was not even executing the paths that held them. Trail of Bits' own comparison of fuzzing against formal verification, on a DAI bug and a Compound V3 bug, found both with a fuzzer in minutes on a laptop, and its conclusion is the useful one: writing good invariants is 80 percent of the work, the tool is secondary.

Dacian's 14 exercises come from simplified private audit findings. Guided harnesses solve most on all three engines. A comparison false for a tiny fraction of inputs defeats the fuzzers but yields to Halmos and Certora, illustrating when a symbolic test earns its cost.

Four kinds of finding show up in fuzz campaigns and rarely in review notes.

• Rounding that drifts in the protocol's disfavor. Each operation rounds correctly by itself. A sequence of deposits and withdrawals of specific sizes leaks value anyway. Invariant tests that compare total shares against total assets after every call catch this, and no reviewer computes it by hand.
• State reachable only through an ordering nobody documented. Pause, then upgrade, then unpause, then a call that assumed the pre-upgrade layout. Sequence fuzzers with a call depth of hundreds find these. Unit tests only encode the orderings the author imagined.
• Accounting invariants broken by an edge value. Zero-amount calls, type(uint256).max approvals, a fee set to 100 percent. Fuzz dictionaries seed exactly these constants, which is why Echidna and Medusa mine them from the source with Slither.
• Reentrancy through token hooks. Foundry's call_override exists for this.

Rounding has a recent price tag. On November 3, 2025, Balancer v2 stable pools lost more than 120 million dollars to repeated small swaps. OpenZeppelin's analysis traces it to scaling functions that always rounded down regardless of swap direction, so that at low balances the entire intended increment was truncated away. Certora, which had formally verified parts of the pools, wrote afterward that the verified properties did not constrain rounding behavior across swaps, and named two properties, roundtrip swap invariance and share value, that would have captured the bug class. Neither post-mortem says whether a fuzz campaign was run against those pools, so the honest claim is narrower: a roundtrip-swap invariant is exactly the kind of property a stateful fuzzer checks thousands of times an hour.

A wrong specification can pass every test. The Echidna fuzz testing guide walks through writing a first property.

Symbolic execution versus fuzzing

A fuzzer samples inputs. A symbolic execution engine treats inputs as variables, collects the conditions along each path and asks an SMT solver whether an assertion can be violated. For a stateless function with bounded loops it proves absence of a counterexample instead of failing to find one. The cost is path explosion: every branch doubles the work, loops must be bounded and external calls or hashes force the engine to concretize.

Tooling has consolidated around Foundry-native engines. Halmos, from a16z, runs Foundry test functions symbolically. Its latest release is 0.3.3 from July 31, 2025, and the repository has not been pushed to since August 2025. hevm, the engine that also powers Echidna's symbolic modes, released 0.58.0 on June 29, 2026. The older generation has faded: Mythril's last release is 0.24.8 from March 2024, and Trail of Bits archived Manticore. The two fuzzers moved toward the middle. Echidna added a symbolic worker in 2.2.4 and a verification mode for stateless functions in 2.3.0, and Foundry 1.8.0 shipped native symbolic testing as an opt-in preview with Z3 as the default solver, including export of counterexamples as fuzz corpus entries and Solidity regression tests.

Choose by the constraints below.

• Fuzz first, with one exception. If the protocol is the shape our survey found without suites, a tokenized asset or a small CDP contract whose risk sits in custody, issuance permissions and governance rather than in call ordering, spend the hours on access-control review and key management instead. For everything with cross-call accounting, fuzz first.
• Add symbolic testing for bounded pure functions. Math, encoding and permission checks where a single rare input is the failure mode and loops are bounded. Halmos unrolls loops twice by default and Foundry's symbolic mode reports a timed-out path as incomplete rather than passed, so a green run is bounded by the limits you set, not a proof of the EVM.
• Do not point it at long sequences. A 300-call lending campaign remains fuzzing's job. The research direction is hybrid, with DepFuzz at OOPSLA 2025 wiring a symbolic module into a feedback-driven fuzzer, but nothing there is production tooling yet.

The cost side of a full proof, with an auditor writing the specification, is the subject of when to pay for formal verification.

How auditors reuse your fuzz suite

Aave's V4 program, described by the team in March 2026 under a 1.5 million dollar security budget ratified by the DAO, shows the full loop. Enigma Dark extended the V3 invariant suite to V4 on Echidna and Medusa, Trail of Bits built its own independent suite during the audit, and the two were then merged into the codebase and CI as one combined suite. Recon's three-week Centrifuge engagement ran the same way on a smaller scale: Medusa for short iteration cycles while coverage was being built, then longer Echidna runs in the cloud, with the harness left in the repository where our scan found it.

An auditor can challenge and extend an existing harness. Without one, the engagement must budget time to build it.

Make the suite reusable before the engagement starts. Four habits do most of the work.

• Keep the harness tool-neutral. Chimera's boilerplate compiles under Foundry, Echidna, Medusa, Halmos and Kontrol, with one caveat that its README spells out: only hevm-supported cheatcodes work across all of them, so a Foundry-only cheatcode such as etch compiles fine and then fails at runtime under Echidna with an unhandled cheatcode error. Strip those before the auditor sees the suite.
• Commit the corpus, or a minimized one. A corpus encodes hours of coverage discovery. Foundry's forge fuzz cmin reduces it to the entries that add coverage, and Medusa's corpus clean command drops entries invalidated by a harness change.
• Write down what each property means in one sentence, as Aave's suite does in a specs folder. An auditor who has to reverse-engineer a property from Solidity will spend the time and bill it.
• State the campaign that was run. Tool version, budget, workers, wall time, coverage.

Ask member firms which harness they will reuse and which properties they will add. Trail of Bits maintains Echidna, Medusa and Slither. Specify the scope in the Audit Builder and consult the tools directory. Record property coverage in the audit report and agree who owns monitoring after deployment.

When fuzzing is not enough

• Fuzzing tests the properties you wrote. Whole loss categories sit outside any harness: the 1.5 billion dollar Bybit compromise in 2025 was a signing failure rather than a contract bug. No invariant covers a signer who has been phished, a malicious upgrade approved by a real key or an oracle reporting a real but manipulated price. Chainalysis counted more than 3.4 billion dollars stolen across the industry that year against that mixed backdrop.
• A fuzzer sees the code you compile. A proxy pointing at a different implementation, an external price feed, a bridge message that arrives out of order: each has to be modeled, and the model is where the assumption hides. On-chain fuzzing through an RPC endpoint narrows this gap for existing integrations and does nothing for a future upgrade of them.
• Coverage is not correctness. A campaign that reaches 95 percent of lines and checks three weak properties has proved little. The strength of a suite is in the invariants, and the invariants come from understanding the protocol's economics, which is a manual job. Static analysis before the campaign clears the cheap findings that would otherwise stop every sequence early. Static analysis triage covers what to fix, suppress or hand to the auditor.
• The campaign has to run long enough, on a corpus. Trail of Bits' Echidna FAQ calls the right duration an open research question and points to coverage growth as the signal to extend a run. Recon puts serious campaigns at many hours and often days or weeks. The measured suites above set million-transaction budgets or no budget at all, run 10 workers and persist a corpus between runs. That is a compute line, and it is small enough that nobody should skip the campaign over it. Medusa's default 10 workers held for 24 hours is 240 core-hours, which is one machine left running overnight and a weekend, or a few dollars per hour of general-purpose cloud compute. A 256-run fuzz test in CI costs nothing and buys nothing beyond regression protection for a known input. Budget the search separately from CI, then replay the minimized corpus in CI so a found input stays found.