Echidna

Skill is based on Echidna (crytic/echidna), generated from source at the listed date.

Echidna is a property-based fuzzer for Ethereum smart contracts. It generates random sequences of contract calls to falsify invariants (Solidity functions named with a prefix like echidna_ that return bool) or to trigger Solidity assert failures. It supports coverage-guided fuzzing, corpus collection, multiple test modes, and integration with Foundry, Hardhat, and Truffle.

Core References

Features

Best practices

Advanced

Generation Info

• Source: sources/echidna
• Git SHA: f946d3638eab3fa3bcb75d7f6cf5e08a2f1c63b6
• Generated: 2026-02-24

Performance debugging

When Echidna is slow or uses a lot of memory, use profiling and known patterns to narrow the cause.

Profiling

Build with profiling and run with RTS options:

nix develop   # or nix-shell
cabal --enable-profiling run echidna -- contract.sol --config config.yaml +RTS -p -s
less echidna.prof

• `-p`: Produces echidna.prof with CPU and memory by function.
• `-s`: Summary to stderr (allocation, GC).

Inspect the .prof file to see which functions dominate CPU or allocation.

Common causes

From the Echidna README and development notes:

1. Costly functions in hot paths — Optimize or reduce calls in the main fuzzing loop. 2. Lazy data constructors accumulating thunks — Use force from Control.DeepSeq to force evaluation and avoid memory buildup. 3. Inefficient data structures in hot paths — Replace with structures better suited to the access pattern.

Reducing campaign cost

• Lower `testLimit` or `seqLen` for quicker iterations during development.
• Use `filterFunctions` to call fewer functions per sequence.
• Disable `coverage` or `corpusDir` temporarily to see if coverage/bookkeeping is the bottleneck.
• Set `workers` to 1 to avoid parallelism overhead when debugging.

Key points

• Profiling is most reliable when running a minimal repro (small contract, short testLimit).
• For advanced profiling (e.g. eventlog), see GHC documentation or Haskell profiling guides.
• When reporting performance issues, include contract size, config (testLimit, seqLen, workers), and profiler output.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/README.md
• sources/echidna/CLAUDE.md

-->

JSON output

Use `format: "json" in config to get machine-readable campaign results. Useful for CI, regression checks, and custom reporting.

Campaign structure

{
  "success": bool,
  "error": "string or null",
  "tests": [ Test ],
  "seed": number,
  "coverage": { ... }
}

• success: Overall campaign success (e.g. no unresolved failure).
• error: Present if a global error occurred.
• tests: One entry per property/assertion test.
• seed: Random seed used (for reproducibility).
• coverage: Coverage-increasing call information (format may vary).

Test structure

{
  "contract": "string",
  "name": "string",
  "status": "string",
  "error": "string or null",
  "testType": "string",
  "transactions": [ Transaction ] or null
}

• contract: Contract name.
• name: Test name (e.g. invariant or assertion identifier).
• status: One of fuzzing, shrinking, solved, passed, error.
• testType: property or assertion.
• transactions: When status is solved, the shrinking call sequence that falsifies the test.

Transaction structure

{
  "contract": "string",
  "function": "string",
  "arguments": [ "string" ] or null,
  "gas": number,
  "gasprice": number
}

Use this to replay or minimize the failing scenario.

CI usage

1. Set format: "json" in config. 2. Run echidna and capture stdout to a file or pipe to jq. 3. Check success and iterate over tests; fail the job if any test has status: "solved". 4. Optionally archive tests[].transactions for regression or issue reports.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/README.md

-->

Invariant best practices

One concern per invariant

Each echidna_* function should check a single property. Split compound conditions into separate invariants so failing traces are easier to interpret.

Multi-sender tests

When logic depends on msg.sender, configure `sender` so multiple addresses can send transactions. Default sender includes several addresses; ensure the contract does not restrict to a single address unless that is what you are testing.

Example: three functions each require a different sender (0x1, 0x2, 0x3). Config:

sender: ["0x1", "0x2", "0x3"]

Invariant that at least one of the three state flags is still false (so all three roles have not been used yet in a bad way):

function echidna_all_sender() public returns (bool) {
  return (!state1 || !state2 || !state3);
}

Payable and value

• Use `maxValue` in config to cap wei sent to payable functions (default is large, e.g. 100 ether).
• Restrict which addresses can send value with `sender` and contract logic; use `balanceAddr` / `balanceContract` if you need specific balances.
• Example config to limit senders for payable tests: set sender and optionally a lower maxValue for faster exploration.

Gas and time

• `propMaxGas`: Property fails if a single call exceeds this gas (e.g. detect unbounded loops or expensive paths).
• `testMaxGas`: Hard cap per sequence; sequence is truncated, not necessarily failed.
• Use `maxTimeDelay` / `maxBlockDelay` when testing time- or block-dependent logic so generated sequences use bounded time/block deltas.

Assertions vs invariants

• Invariants (echidna_*): Check state after arbitrary sequences; good for “always” properties (e.g. balance >= 0, no double spend).
• Assertions (assert(...)): Use testMode: assertion to find any reachable assertion failure; good for internal consistency or safety checks already in the code.
• Use both when appropriate: invariants for high-level properties, assertions for low-level sanity checks.

Key points

• Name invariants clearly: echidna_balance_non_negative, echidna_only_owner_can_pause.
• Use filterFunctions to focus on relevant functions and avoid wasting effort on view/pure or setup-only functions.
• Set seed in config for reproducible campaigns when debugging or CI.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/tests/solidity/basic/multisender.sol
• sources/echidna/tests/solidity/basic/payable.yaml
• sources/echidna/tests/solidity/basic/propGasLimit.yaml
• sources/echidna/tests/solidity/basic/gasprice.sol

-->

Property invariants

Echidna falsifies user-defined predicates (invariants) by generating random sequences of contract calls. Use this to check that certain conditions always hold.

Defining invariants

Invariants are Solidity functions that:

• Are named with the configured prefix (default echidna_)
• Take no arguments
• Return bool (true = invariant holds)

Example: a balance that must never go below 20:

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

Change the prefix via config (e.g. prefix: "invariant_") if you need a different naming convention.

Running Echidna

echidna contract.sol
echidna contract.sol --contract MyTestContract --config config.yaml

Echidna generates call sequences, runs them, and checks each invariant. If it finds a sequence that makes an invariant return false, it reports the failing call sequence and shrinks it for triage.

Example contract

contract Test {
  bool private flag0 = true;
  bool private flag1 = true;

  function set0(int val) public {
    if (val % 100 == 0) flag0 = false;
  }
  function set1(int val) public {
    if (val % 10 == 0 && !flag0) flag1 = false;
  }

  function echidna_alwaystrue() public returns (bool) { return true; }
  function echidna_sometimesfalse() public returns (bool) { return flag1; }
}

Running echidna tests/solidity/basic/flags.sol: Echidna will find a sequence that falsifies echidna_sometimesfalse and will not falsify echidna_alwaystrue.

Key points

• One invariant per function; add multiple echidna_* functions to check several properties.
• Invariants are checked after each generated transaction sequence (or at sequence end depending on config).
• Use stopOnFail: true in config to stop the campaign as soon as one invariant is falsified and shrunk.
• Property tests use psender (default same as deployer) for who sends property-check transactions; sender list controls who can send the fuzzed transactions.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/README.md
• sources/echidna/tests/solidity/basic/flags.sol

-->

Build system support

Echidna uses crytic-compile and works with common Solidity project layouts. Use this to fuzz contracts that depend on libraries or other contracts.

Project root invocation

From the project root (where the build config lives):

echidna .

Echidna will use the existing compilation framework (Foundry, Hardhat, Truffle, etc.) to compile. No need to point at a single .sol file when you have dependencies.

Contract and config

When multiple contracts exist, select the test contract and optionally a config:

echidna . --contract MyFuzzTest --config echidna.yaml

Testing multiple contracts

Set `allContracts: true` in config so Echidna can call into any contract with a known ABI. Pass the corresponding Solidity sources on the CLI so ABIs are available. Use this when the contract under test interacts with other deployed contracts.

State forking

Echidna can start from an existing network state (e.g. mainnet fork) instead of an empty chain. Configure RPC and block so crytic-compile/Echidna can fetch contracts and state. See external docs (e.g. secure-contracts.com) for rpcUrl, rpcBlock, and forking setup.

Library linking

For solc library placeholders (e.g. unresolved libraries), use `solcLibs` in config:

solcLibs: ["path/to/file.sol:LibraryName"]

Example from tests: solcLibs: ["basic/library.sol:Test"].

Key points

• Prefer echidna . for Foundry/Hardhat projects so dependencies and remappings are correct.
• Ensure the project builds (e.g. forge build or npx hardhat compile) before running Echidna.
• Use allContracts: true only when you need to fuzz interactions across multiple contracts and have provided their sources.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/README.md
• sources/echidna/tests/solidity/basic/library.yaml

-->

FFI and cheatcodes

Echidna can use HEVM-style cheatcodes (e.g. FFI) when enabled. This allows tests to call out to the environment or manipulate VM state in ways useful for property tests.

Enabling FFI

In config:

allowFFI: true

Without this, FFI cheatcode usage typically causes a failure or is ignored (tool-dependent). Enable only when your invariants or test contract rely on FFI.

HEVM context

Echidna uses hevm for EVM execution. HEVM provides cheatcodes (e.g. for prank, warp, FFI) that some tests use. When allowFFI: true, the FFI cheatcode is allowed so contracts can invoke external binaries or scripts during fuzzing.

Use with care

• FFI can reduce reproducibility (external processes, filesystem) and may be slower or flaky.
• Use for tests that explicitly need to call out (e.g. oracles, cross-process checks). For standard invariants, leave allowFFI: false.
• Test configs that use FFI often pair with limited runs for debugging (e.g. testLimit: 1, seqLen: 1) in the repo examples; production fuzzing may keep FFI disabled.

Key points

• Set allowFFI: true only when the contract or invariants use the FFI cheatcode.
• Check Echidna/HEVM docs for the exact list of supported cheatcodes and signatures.
• Prefer pure Solidity invariants when possible to keep campaigns fast and reproducible.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/tests/solidity/cheat/ffi.yaml
• sources/echidna/tests/solidity/basic/default.yaml

-->

Function filtering

Control which functions Echidna may call using `filterFunctions` and `filterBlacklist`.

Options

Signatures use Solidity-style form: ContractName.functionName(type1,type2).

Blacklist (default)

Exclude specific functions from fuzzing:

filterBlacklist: true
filterFunctions: ["Test.set0(int256)"]

Only set0(int256) is excluded; all other public/external functions of the test contract can be called.

Whitelist

Restrict fuzzing to a subset of functions:

filterBlacklist: false
filterFunctions: ["Test.deposit(uint256)", "Test.withdraw(uint256)"]

Echidna will only call these two functions (and any invariants). Use when the contract has many entrypoints but you want to test a specific flow.

Key points

• Signatures must match exactly (e.g. int256 not int).
• Filtering applies to the contract under test; invariant (prefix) functions are still executed for checks.
• Useful to exclude view/pure or setup helpers and focus on state-changing functions, or to whitelist only the functions relevant to a property.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/tests/solidity/basic/whitelist.yaml
• sources/echidna/tests/solidity/basic/default.yaml

-->

Symbolic execution

Echidna can run an additional symbolic execution worker alongside fuzzing to explore paths that are hard to reach with random inputs. Enable it when you need deeper exploration (e.g. assertion mode or complex conditions).

Enabling

In config:

symExec: true

Optional tuning:

Example

From tests (assertion mode + symbolic):

testMode: assertion
symExec: true
symExecSMTSolver: z3
workers: 0
seqLen: 1
disableSlither: true

workers: 0 disables parallel fuzzing workers (sometimes used with symbolic to avoid resource contention). seqLen: 1 is a test choice, not required for symbolic.

When to use

• Assertion mode: Finding inputs that violate assert(...) in deep branches.
• Complex invariants: When fuzzing alone rarely hits a condition (e.g. specific value or ordering).
• Research / one-off: Symbolic execution is heavier; use when you need more completeness on a small target.

Key points

• Slither may be disabled when using symbolic (e.g. compatibility); set disableSlither: true if needed.
• SMT solver must be installed (Bitwuzla, Z3, or cvc5) for symbolic to work.
• Combine with testMode: assertion to target assertion failures with symbolic exploration.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/tests/solidity/symbolic/verify.yaml
• sources/echidna/tests/solidity/basic/default.yaml

-->

Test modes

Set `testMode` in config to choose what Echidna checks or optimizes.

Modes

Property mode

Default. Define functions like echidna_invariant_name() returning bool; Echidna tries to find call sequences that make them return false.

Assertion mode

No need for echidna_ functions. Echidna tries to reach any assert(...) and make it fail. Useful for finding assertion violations (e.g. internal invariants or safety checks).

Example config:

testMode: assertion

Exploration mode

Focus on covering as much code as possible. Use when you want to stress the contract or build a corpus without a specific property.

Optimization mode

Target a function that returns a numeric value; Echidna tries to maximize (or minimize) that value. Used for e.g. “find the maximum value achievable by this function.”

Key points

• Most use cases: property (invariants) or assertion (assert failures).
• In assertion mode, ensure the contract under test contains assert(...) in reachable code.
• Symbolic execution (see features-symbolic.md) can be combined with assertion mode for deeper exploration.

<!-- Source references:

• https://github.com/crytic/echidna (README.md)
• sources/echidna/README.md
• sources/echidna/tests/solidity/basic/default.yaml
• sources/echidna/tests/solidity/symbolic/verify.yaml

-->