Smart contract fuzzing tools compared: Echidna, Medusa, Halmos, and Foundry

Four tools dominate smart contract fuzzing today. Each one approaches the problem differently, and picking the wrong one wastes time. This guide breaks down Echidna, Medusa, Halmos, and Foundry's built-in fuzzer so you can match the right tool to your project — or use all four together through Chimera.

<a href="/request-audit" class="cta-button">Get expert fuzzing for your protocol</a>

Four fuzzers in 2025

Smart contract fuzzing has split into four distinct approaches.

Echidna is the original. Built in Haskell, it pioneered grammar-based stateful fuzzing for Solidity and still has the best corpus management of any tool in the space. Medusa came later as a Go-based alternative, trading Echidna's single-threaded precision for parallel throughput. Halmos isn't a fuzzer at all in the traditional sense. It's a symbolic execution engine that provides bounded model checking and mathematical proofs. And Foundry's built-in fuzzer (forge test) handles fast stateless and stateful fuzzing directly inside the development workflow most teams already use.

These aren't competing products. They're complementary tools that cover different parts of the bug-finding spectrum.

Feature comparison table

Feature	Echidna	Medusa	Halmos	Foundry fuzz
Language	Haskell	Go	Python	Rust
Execution model	Single-threaded	Parallel (N workers)	Symbolic	Single-threaded
Stateful fuzzing	Yes (directed)	Yes (parallel)	N/A (symbolic)	Yes (invariant tests)
Corpus management	Excellent (binary, persistent)	Good (JSON, readable)	N/A	None (no persistence)
Optimization mode	Yes	Yes	N/A	No
Symbolic execution	No	No	Yes (bounded)	No
Throughput (8 cores)	~2,000 exec/s	~8,000 exec/s	~10-50 paths/s	~3,000 exec/s
Sequence shrinking	Excellent	Good	N/A	Basic
Setup time	Moderate	Moderate	Low	Minimal
CI integration	Good (Docker)	Good (binary)	Good (pip)	Excellent (native)
Community maturity	Since 2019	Since 2022	Since 2023	Since 2022

Echidna

Echidna runs a single-threaded fuzzing loop that builds transaction sequences incrementally. It generates a call, executes it, and extends sequences that hit new code paths. This directed approach makes it the strongest tool for complex stateful protocols where the order of operations matters.

Its corpus management is the best in the ecosystem. Echidna persists interesting sequences to disk and aggressively shrinks failing sequences on restart. A 100-call failure trace becomes 4-5 calls that you can actually debug. No other tool produces reproducers this clean.

# echidna.yaml
testMode: assertion
testLimit: 500000
seqLen: 100
corpusDir: "corpus-echidna"

When to use Echidna: complex DeFi protocols with multi-step user flows and any project where you need minimal reproducers for specific state transitions. It's the tool you run overnight when you need thorough coverage.

Medusa

Medusa spawns N parallel workers, each with its own EVM instance, exploring the state space independently. Workers share coverage data through a synchronized corpus, so a discovery in one worker benefits all others. On an 8-core machine, it reaches 80% coverage roughly 3x faster than Echidna.

Its corpus is stored as human-readable JSON, which makes debugging easier. Medusa also supports optimization testing. Instead of just checking boolean properties, it can minimize or maximize a numeric value, useful for finding worst-case scenarios.

{
  "fuzzing": {
    "testLimit": 500000,
    "callSequenceLength": 100,
    "workers": 8,
    "corpusDirectory": "corpus-medusa"
  }
}

When to use Medusa: large codebases where throughput matters, CI/CD pipelines where wall-clock time is constrained, projects that need fast initial coverage before deeper exploration. It's the tool you run first when starting a new campaign.

Halmos

Halmos doesn't fuzz at all. It uses symbolic execution to mathematically prove whether a property holds for all inputs within a given bound. Echidna and Medusa test millions of concrete inputs hoping to find a violation. Halmos encodes the problem as an SMT formula and asks a solver to find a counterexample, or prove none exists.

This makes it uniquely powerful for arithmetic-heavy code. If you need to verify that a rounding operation never underflows for any possible input combination, Halmos gives you a mathematical guarantee (up to the configured bound). Fuzzers can only give you statistical confidence.

// Halmos checks this for ALL possible inputs within bounds
function check_noUnderflow(uint128 x, uint128 y) public {
    vm.assume(y <= x);
    uint128 result = x - y;
    assert(result <= x);
}

When to use Halmos: critical arithmetic and accounting logic, verifying invariant properties over bounded input ranges, any situation where "probably correct" isn't good enough. It pairs well with fuzzing — use fuzzers for broad exploration, then Halmos to prove the critical paths.

Foundry fuzz

Foundry's built-in fuzzer runs inside forge test. It handles both stateless fuzzing (random inputs to a single function) and stateful fuzzing (random call sequences against invariant_ functions). There's no separate tool to install and no configuration file to manage. Results show up in the same test output developers already read.

It won't match Echidna's sequence quality or Medusa's throughput, and it doesn't persist a corpus between runs. But its zero-friction setup makes it the fastest path from "I should test this property" to actually testing it.

// Foundry stateless fuzz test, just add a parameter
function testFuzz_depositWithdraw(uint256 amount) public {
    amount = bound(amount, 1, type(uint128).max);
    vault.deposit(amount);
    uint256 shares = vault.balanceOf(address(this));
    vault.withdraw(shares);
    assertEq(vault.balanceOf(address(this)), 0);
}

When to use Foundry fuzz: quick property checks during development, Foundry-native projects that want fuzzing without adding dependencies, unit-test-adjacent properties where stateless fuzzing is sufficient. It's where you start before reaching for heavier tools.

Using all four with Chimera

You don't have to pick one. The Chimera framework provides a unified interface that lets you write properties once and run them with Echidna, Medusa, and Foundry without changing a line of code. Halmos tests require symbolic-style assertions, but Chimera's structure keeps your property logic organized so adapting it for Halmos is straightforward.

// One property, three fuzzers
contract CryticTester is TargetFunctions, CryticAsserts {
    constructor() {
        setup();
    }
}

The workflow we use at Recon on every engagement:

1. Write properties with Chimera's unified interface
2. Iterate fast with Foundry (forge test)
3. Run Medusa for quick parallel coverage
4. Run Echidna for deep directed exploration
5. Run Halmos on critical arithmetic properties
6. Run everything in Recon Pro for cloud-scale campaigns

Each tool catches bugs the others miss. If you want the full comparison between just Echidna and Medusa, we've covered that in detail in our practical comparison post.

Which tool should you pick

If you're already using Foundry and want to start fuzzing today, start with forge test and add fuzzed inputs to your existing tests.

If you're building a DeFi protocol with complex state transitions, add Echidna. Its directed exploration and sequence shrinking are unmatched for finding multi-step bugs.

If your codebase is large and CI time is limited, add Medusa. Its parallel execution fits naturally into automated pipelines.

If you have critical arithmetic that needs mathematical guarantees, add Halmos. Statistical confidence isn't enough for code that handles user funds.

If you want all of the above without vendor lock-in, use Chimera. Write once, run everywhere. Our beginner's guide covers the full setup.

Related

• What is Echidna?
• What is Medusa?
• What is Halmos?
• What is Foundry?
• Chimera framework explained
• Echidna vs Medusa: a practical comparison
• Stateful fuzzing explained

If you want expert help setting up a multi-tool fuzzing pipeline, or want to run intensive campaigns on cloud infrastructure, request an audit with Recon. We'll build a custom invariant test suite and run it with every tool in our arsenal.