Echidna: the Haskell fuzzer that falsifies Solidity invariants

What Echidna falsifies, and who writes the properties

Echidna is a fuzzer aimed at Solidity contracts. The README describes it as a Haskell program for fuzzing and property-based testing of Ethereum smart contracts, using grammar-based campaigns built on the contract ABI. The output you get is not a coverage report or a lint list. It is a call sequence that makes one of your own predicates return false.

That framing decides the audience. If you cannot state what should always hold, Echidna has nothing to check. The README's own example is a balance that should never drop below 20, expressed as a function named with the echidna_ prefix, taking no arguments and returning a bool. Everything else in the tool is machinery for finding the sequence that violates it. Teams auditing DeFi contracts, or maintaining them across upgrades, are the natural users. Teams looking for a static analyzer should look elsewhere; Echidna runs the EVM, it does not reason about source text alone.

The fuzzing loop: ABI, Slither, corpus, minimization

The mechanism has four parts. First, crytic-compile invokes your existing build system (Foundry, Hardhat or Truffle) so Echidna does not need its own Solidity pipeline. Second, Slither extracts information from the compiled contract before the campaign starts, which the README lists as a feature. Third, the fuzzer generates random sequences of calls against the ABI and checks each predicate after every sequence. Fourth, when a predicate fails, Echidna minimizes the test case so the reported sequence is short enough to triage by hand.

Corpus collection is optional and, per the README, adds mutation and coverage guidance to reach deeper bugs. Coverage is written to a directory named coverage and to a plain-text file named covered.txt, which is a copy of your source with line markers. Those markers are worth knowing: * for a STOP, r for a REVERT, o for out-of-gas, and e for any other error such as zero division or an assertion failure. A line carrying r or e is usually where you start reading.

Test modes: property, assertion, foundry, verification, overflow, optimization, exploration

The default mode is property, which runs echidna_-prefixed functions returning bool. This is the mode the README's example uses, and the one most tutorials assume. It is also the mode with the least tooling overlap, because the prefix is a convention Echidna invented rather than something your test runner already understands.

The foundry mode is the pragmatic choice for repositories that already use Forge. It follows Foundry naming: test-prefixed unit and fuzz tests, testFail-prefixed tests that are expected to revert, and invariant- or statefulFuzz-prefixed stateful invariants. One caveat is stated plainly in the README: check- and prove-prefixed functions are symbolic entry points, but in foundry mode they are fuzzed like any other test function, so the name does not buy you symbolic execution. The verification mode does treat check and prove as entry points, but it verifies each function using a single transaction, which rules out multi-step state manipulation. The assertion mode catches assert() failures and Foundry assertX helpers. Overflow mode targets integer over and underflows on Solidity 0.8.0 and later. Optimization mode maximizes the return value of an echidna_ function returning int256, and exploration collects coverage without checking anything.

Installing Echidna and running a first campaign

The README does not give a package-manager install line. It points to the Building Secure Smart Contracts repository for a crash course, and the repository itself carries stack.yaml, package.yaml, flake.nix and default.nix, so the Haskell build route (Stack or Nix) and the Docker directory are the paths visible in the tree. Use whichever your environment already supports.

Once the binary is on your PATH, the smallest useful run is a single Solidity file. Start with the example shipped in the repository, which the README names explicitly:

echidna tests/solidity/basic/flags.sol

The README states the expected outcome: Echidna should find a call sequence that falsifies echidna_sometimesfalse, and should be unable to find a falsifying input for echidna_alwaystrue. If you see that split, the fuzzer and your compiler are talking to each other.

To add an invariant to your own contract, write a function with the echidna_ prefix, no arguments and a bool return. The README's example guards a balance:

function echidna_check_balance() public returns (bool) {
    return(balance >= 20);
}

For a compiled project, point Echidna at the directory rather than a file so crytic-compile can pick up the framework:

echidna .

Configuration can come from a file or from the CLI. The README shows both together, choosing a contract and loading a YAML config:

echidna contract.sol --contract TEST --config config.yaml

The same options are reachable as flags, for example --test-mode for the modes listed above. If your contract needs to call into other deployed contracts, set allContracts: true in the config, which the README says lets Echidna call any contract with a known ABI when the Solidity source is passed on the command line.

Where Echidna is the wrong tool

The single-transaction limit in verification mode is the sharpest constraint. A protocol whose bug requires deposit, then a price move, then a withdrawal cannot be proven safe by a mode that only ever executes one transaction. You can still fuzz it, but fuzzing gives you a found counterexample or nothing, not a proof.

The second constraint is that the tool only knows the properties you write. A contract with a correct-looking echidna_check_balance and a missing invariant on the withdrawal path will pass. Echidna's value is bounded by the specification, and the README does not claim otherwise.

The third is the build dependency. Testing goes through crytic-compile, so a project whose compilation is unusual, or which depends on a toolchain crytic-compile does not recognize, will spend its first hour on integration rather than on fuzzing. The README also does not document rollback or a way to undo a corpus directory once it is written, so treat corpusDir as an output directory you own and clean yourself.

Echidna against Foundry's built-in fuzzer

The obvious comparison is Foundry's own fuzzing, since Echidna now speaks Foundry's naming conventions in foundry mode. The difference is in the search strategy and the state model. Foundry's fuzzer is part of the test runner you already invoke with forge test; Echidna is a separate binary that drives the same contracts through crytic-compile, adds Slither analysis before the campaign, keeps a coverage-maximizing corpus across runs, and minimizes failing sequences for triage. If your invariants are already written as Foundry invariant tests and you never need corpus replay or minimization, the built-in runner is the shorter path. If you want coverage-guided campaigns with a persistent corpus and a minimized counterexample, Echidna is doing work the test runner does not.

Maintenance, licence and upgrade cost

The repository is not archived, and the last push was on 2026-09-16. Recent releases are v2.3.3 on 2026-07-27, v2.3.2 on 2026-03-27, and v2.3.2-agents-preview-1 on 2026-01-20. The CHANGELOG.md at the repository root is where release-level changes are recorded, and it is the file to read before moving a pinned version in CI.

The licence is AGPL-3.0. That matters more for a tool you ship or modify than for one you invoke locally in a CI job, but the boundary is a legal question, not a technical one, and this article does not give legal advice. What is technical is the upgrade cost: because testing depends on crytic-compile and on Slither, a version bump can change how your project compiles as well as how it fuzzes. Pin the version you run in CI and read CHANGELOG.md before unpinning it.

Editorial conclusion

Adopt Echidna when your contract has invariants you can state in Solidity and your build already goes through Foundry, Hardhat or Truffle, since crytic-compile handles the compilation step for you. Do not adopt it as a substitute for a symbolic executor or for a formal specification you have not written down: the property and assertion modes only test predicates you supply, and the verification mode is limited to single-transaction symbolic checks. Before committing, run echidna tests/solidity/basic/flags.sol from the repository to confirm the binary resolves your toolchain, then check whether your team can accept AGPL-3.0 terms for a tool you invoke in CI.

Frequently asked questions

Official sources

1. crytic/echidna on GitHub
2. License: AGPL-3.0
3. Project website
4. README
5. Releases