Tool selection guide
Smart contract fuzzing tools: choose a harness and campaign
Choose the state transitions and properties first. A campaign can run for hours without testing a withdrawal rule if its callers cannot reach funded vault states. The useful output is a reproducible violating sequence, together with enough setup information to explain why it violates the intended rule.
Sources checked . Published fixture reviewed; no local campaign was executed.
Decide what your review needs
- State the invariant in domain terms before encoding it: for example, which actors may withdraw and which liabilities must remain covered.
- Include realistic callers and setup actions. A harness that grants every caller privileged roles may test a different system.
- Review reverted calls and state reachability. Increasing the campaign budget does not repair an unreachable target.
- Preserve a failing corpus entry, the source revision and configuration. Re-run the smallest sequence after a fix and keep it as a regression case.
Use the domain examples to write protocol invariants.
Compare inputs, results and limits
| Tool & access | Input → output | When it fits | Limits & source |
|---|---|---|---|
| Echidna EVM | Input: Contracts, property functions and campaign configuration Output: Failing call sequences and optional coverage/corpus artifacts | You want property-based exploration with Solidity-defined invariants. | Reachable states depend on the harness, caller setup, corpus and campaign budget. Documentation reviewed. Official source |
| Medusa EVM | Input: Supported Solidity project and property/campaign configuration Output: Coverage-guided campaign results and test sequences | You need configurable parallel campaigns and can inspect the harness assumptions. | Coverage growth alone does not establish that the chosen invariants express the intended rules. Documentation reviewed. Official source |
| Foundry EVM | Input: Solidity tests and invariant handlers in a Foundry project Output: Unit/fuzz/invariant test outcomes and failure traces | You want the campaign beside the existing project tests and regression suite. | Fork tests inherit the selected block, RPC state and assumptions in the test harness. Documentation reviewed. Official source |
Public artifact walkthrough
Use the published Echidna flags fixture to identify the expected failure
The README points to tests/solidity/basic/flags.sol. It describes one property that can be falsified and one that should remain true under the example's setup. Use this pair to distinguish a functioning campaign from a project-specific assurance claim. Finding the example failure demonstrates the fixture's behavior; it does not establish that your own invariant expresses the correct economic rule.
- Read the fixture and identify which calls can change the state used by each property.
- Pin a repository revision and record the tool version before running the example in your own environment.
- Retain the failing sequence and campaign configuration. For your project, replace the fixture properties with named rules and explicit caller assumptions.