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. Most losses in DeFi sit in the second category, because the bug appears only after a specific ordering of calls that nobody wrote a unit test for.

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.

The catalog of properties to encode for each protocol type is a separate topic, covered in protocol invariants auditors expect. This guide is about picking and running 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.

One statement from the maintainers frames the Echidna versus Medusa question. In February 2025, Trail of Bits wrote that it would keep maintaining Echidna for minor bug fixes while its primary focus shifted to Medusa, and published an internal benchmark in which the two performed similarly on coverage and corpus size. Echidna then received a 2.3 line with symbolic modes anyway. Recon, which runs both in its cloud, reports that Medusa reaches broad coverage roughly 3 times faster than Echidna on an 8-core machine and that Echidna still has the best sequence shrinking, cutting a failing 100-call sequence to 4 or 5 calls.

Three rows matter more than the rest.

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.

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

Documentation says what a tool can do. Repositories say what teams do. On September 2, 2026, we took the 30 largest DeFi protocols by total value locked on DefiLlama, using the same filter as our security.txt survey (no exchanges, chains or bridges), located the public contracts repository for each, and scanned the full file tree of every repository for Echidna configs and harnesses, medusa.json files and Foundry invariant tests. A GitHub code search for invariant_ and testFuzz functions cross-checked the tree scan. The script and raw results are kept in the site repository as seo/research/fuzz-suite-survey-2026-09-02.json for anyone who wants to re-run the scan.

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. Formal verification artifacts (Certora specs or CI jobs) sit next to the fuzzers at Aave, Morpho Blue, EigenLayer and Veda.

Two details are worth reading into.

First, 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. Second, 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 reviewer reads one path at a time and reasons about it. A fuzzer executes millions of paths and reasons about none of them. The bugs that favor the second approach share a shape: they need a precise combination of values or a long ordering of calls, and each step looks correct in isolation.

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.

Public evidence of that shape comes from the fuzzing challenge set maintained by the auditor Dacian, built from simplified versions of findings in his private audits at Cyfrin. Each challenge is run with Foundry, Echidna and Medusa in a "basic" unguided configuration and in an "advanced" guided one. In four of the first five challenges the three fuzzers tie in the guided configuration. Two results separate them. In the Token Sale challenge, only Medusa breaks both invariants unguided, while Foundry and Echidna break the easier one. In the Omni Protocol challenge, all three run guided against 16 invariants on a real lending codebase: Medusa typically breaks 2 within 5 minutes, Echidna sometimes breaks 1 and Foundry breaks none inside that window. The sixth challenge, a comparison that is false for a tiny fraction of inputs, defeats every fuzzer. Halmos and Certora solve it.

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.

What fuzzing does not find is equally consistent: a wrong specification. If the property encodes the same misunderstanding as the code, the campaign passes, and it passes with a green coverage report that makes everyone feel better. The Echidna fuzz testing guide on this site walks through writing a first property. The discipline of asking "what must never happen" before "what does the function do" is the part that transfers between tools.

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.

Use the split this way.

Fuzz first, always. Add symbolic testing for pure math, encoding and permission checks where a single rare input is the failure mode, and where loops are bounded. Do not expect it to handle a 300-call lending sequence. That remains fuzzing's job. 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. The research frontier is hybrid: DepFuzz, presented at OOPSLA 2025, adds a symbolic execution module to a feedback-driven fuzzer and was evaluated on 286 benchmark and 500 real-world contracts, and Verite, published in January 2025, targets profitable exploits directly and reports 29 detections against 10 for ItyFuzz on the same targets. 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 existing suite changes what an audit engagement spends its hours on. The auditor starts from properties the team believes, checks which are wrong or missing, and runs the campaign on hardware and for a duration the team could not. Without a suite, the first days go to building a harness, which the client then pays for at audit rates.

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.

Among DeFi Security Alliance members, Trail of Bits maintains Echidna, Medusa and Slither, sells invariant development as a standalone service since October 2023, and ships the harnesses it writes back to the client, as the Uniswap v3 audit folder shows. Its pre-review checklist asks for a frozen commit and higher test coverage before the engagement starts. When requesting quotes, say whether a suite exists and in which tool. The Audit Builder lets you put fuzzing scope on the request, and the DSA tools page collects the member utilities that run before a campaign, such as HashEx's fork checker.

When fuzzing is not enough

Fuzzing tests the properties you wrote. The exploits that cost the most in the last three years were mostly not ordering bugs in isolated contracts. They were compromised keys, malicious upgrades, oracle and economic manipulation and integrations with a dependency that behaved differently from its documentation. No property in a harness covers a signer who has been phished.

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. A 256-run fuzz test in CI is regression protection for a known input, not a search. Budget compute for the search separately, and replay the corpus in CI so a found input stays found.