crytic/echidna v2.4.0

Echidna 2.4.0

on GitHub

Echidna 2.4.0 brings two major improvements: MCP support for interactive fuzzing and substantially improved symbolic execution. This release also improves Foundry compatibility, corpus reuse, and memory usage.

Experimental MCP support

Echidna now exposes a Model Context Protocol server that lets tools and AI assistants inspect and guide a running fuzzing campaign. Clients can inspect coverage and failing tests, prioritize transaction sequences, replay concrete calls, sample function behavior, and reload the corpus. This enables workflows where an assistant examines uncovered code, proposes targeted sequences, and checks whether they uncover new behavior. #1607

Start a campaign with:

echidna MyContract.sol --server 8080 --format text

Connect an HTTP MCP client to http://127.0.0.1:8080/mcp (e.g. use claude mcp add --transport http echidna http://127.0.0.1:3000/mcp). The repository includes an example agent that uses coverage feedback to guide fuzzing.

MCP support remains experimental. Its tool APIs and workflows are still subject to change. Feedback on integrations and practical use cases is welcome.

Substantially improved symbolic execution

The updated hevm backend brings better handling of arithmetic-heavy properties, mappings, packed storage, memory operations, and hashes. Arithmetic abstraction helps solvers prove properties involving multiplication and division that previously required expensive bitvector reasoning. Better simplification and sharing of symbolic expressions also reduce unnecessary work during exploration. These improvements benefit both dedicated verification and symbolic exploration alongside fuzzing.

One small integration regression illustrates the arithmetic improvement: a multiplication-monotonicity property verified in approximately 1.6 seconds with both Z3 and Bitwuzla, while native arithmetic reached the 30-second timeout. These measurements used solc 0.8.25 and include compilation; they describe this particular regression. #1639

Verification can be run directly with:

echidna MyTests.sol --test-mode verification

Functions prefixed with check or prove are recognized as verification entry points even when static analysis finds no assertion. Larger solver queries also get more headroom: the new symExecSolverMemory option defaults to 16384 MB per solver process, increased from 1024 MB. #1595, #1642

Some numbers on the resources need for FV and the capabilities are described in these blog post:
https://gustavo-grieco.github.io/blog/a-spark-is-born/ and https://gustavo-grieco.github.io/blog/spark-followup/

Additional improvements include:

• Better Foundry compatibility, including invariant naming, expected-revert tests, and stateless test selection.
• Better corpus reuse when seqLen: 1, consistent sequence lengths, and test limits that count executed transactions.
• Library auto-linking through crytic-compile.
• Lower memory usage in campaign event queues and coverage messages that identify the function responsible.

When upgrading, note these compatibility changes:

• --server now serves MCP instead of the previous SSE interface. Existing SSE integrations need to migrate.
• JSON transaction arguments now use structured values. Bytes are hexadecimal strings, while arrays and tuples are JSON arrays.
• A fixed seed can no longer be combined with a campaign timeout. Use testLimit or --test-limit to bound seeded runs.

See the full changelog for all changes.

This release was partially funded by the recent donation round on Giveth for Echidna; work like this is possible because of everyone who contributed.