What testing is for
Tests prove that the code does what the developer thought it would do, against the inputs the developer thought to test. Tests do not prove the absence of bugs; they prove the presence of the bugs the tests were written for.
A smart contract testing strategy worth anything covers four layers: unit tests, integration tests, property-based fuzzing, and (when warranted) symbolic or formal verification. The layers are not interchangeable. Each catches what the others do not.
This paper focuses on the EVM testing ecosystem (Foundry, Hardhat, Echidna, Medusa, Halmos, Certora). Each non-EVM ecosystem has its own testing stack: Anchor's
solana-program-testand Sec3 fuzzing on Solana, the Move Prover and unit-test framework on Move,protostar/starknet-pyon Cairo,cw-multi-testandcosmwasm-checkon CosmWasm, and the TON emulator on TON. The layered strategy is the same; the toolchain is per-ecosystem.
Unit tests
Unit tests exercise individual contract functions against handwritten inputs. The strength: every developer can write them, they run fast, they make refactoring safe, they document expected behavior.
The weakness: tests cover what the developer thought to test. The bugs that survive into production are the ones the developer did not think of.
Foundry is the current standard. Tests are written in Solidity, run in a local EVM, use vm cheatcodes for state manipulation. Test gas costs are visible. Fork tests against mainnet state are straightforward.
Hardhat is the prior generation. Tests are written in JavaScript or TypeScript, integration with the broader JS ecosystem is closer, mocking is more familiar to non-Solidity developers. Slower than Foundry; still in active use.
What unit tests catch: known patterns the developer can articulate, regression bugs after a refactor, expected-revert behavior on known bad inputs.
What unit tests miss: anything the developer did not think to write a test for, edge cases in arithmetic, state-dependent bugs that only appear under specific call orderings, interactions across multiple contracts.
Integration tests
Integration tests exercise multiple contracts together. They often run against a forked mainnet state, so the protocol's actual dependencies (DEX prices, lending pools, oracles) are real rather than mocked.
The strength: catches bugs that emerge from the composition of contracts rather than from any single contract. Most reentrancy across protocols is invisible at the unit-test layer.
Foundry's fork-test mode is the current standard. The test imports mainnet state at a specific block, deploys the protocol against it, and runs scenarios that involve real DEX trades, real oracle responses, real liquidations.
What integration tests catch: composition bugs, real-oracle behavior, real-MEV exposure on the testbed.
What integration tests miss: anything that depends on adversarial behavior the test does not script. The integration test still has a finite set of scenarios.
Property-based fuzzing
Fuzzing is the next layer. The developer states invariants. The fuzzer generates inputs that try to violate the invariants. Each generated input is a potential bug.
Echidna is mature and slow. Properties are written in Solidity alongside the contract under test; Echidna runs stateful fuzzing campaigns against them. Internally written in Haskell.
Medusa is the newer Foundry-aligned fuzzer from Trail of Bits. Faster, better integration with the Foundry ecosystem.
Foundry's built-in fuzzer runs property tests for simple invariants without a separate tool. Foundry's stateful invariant testing (added in 2023, matured through 2025) now competes with Echidna for many use cases; the choice depends on the team's existing test infrastructure and the complexity of the invariants.
The invariants come from the trust-boundary diagram and from the protocol's specification. If the protocol cannot state its invariants cleanly, the protocol has a specification problem before it has a security problem.
What fuzzing catches: corner cases the developer did not test, state combinations the integration tests did not script, arithmetic-precision bugs that only surface at the boundary.
What fuzzing misses: bugs that require specific external state (forked state plus adversarial oracle behavior plus particular MEV), bugs in invariants the developer did not state.
Symbolic execution and bounded symbolic testing
Symbolic execution generates abstract inputs and walks every code path. Every branch is a constraint; the solver finds inputs that violate a stated property.
Halmos is symbolic property checking integrated with Foundry tests. Halmos shipped multi-contract symbolic testing in 2025; the "small contracts only" framing of earlier symbolic tools no longer applies. Lightweight enough to run in CI on contracts of moderate size.
Mythril is general-purpose symbolic execution. More expensive than Halmos; used surgically.
Symbolic execution is expensive. It scales poorly to large contracts. The right use is on small contracts where the property must hold (key cryptographic primitives, signature verification, mathematical libraries) and on specific paths inside larger contracts where manual review has flagged a hypothesis.
What symbolic execution catches: violations of stated properties on paths the path-coverage reaches.
What symbolic execution misses: paths the solver does not reach in reasonable time, properties that were not stated.
Formal verification
Formal verification proves stated properties against the verified contract model and bytecode assumptions, not the full real-world deployment environment.
Certora Prover is the production-grade tool. The work involves writing a spec (in Certora's CVL language) that states the properties, then running the prover to confirm that the implementation satisfies the spec for all inputs.
The cost is real. A formal-verification engagement costs more than an audit because writing the spec is itself an engineering task that requires a separate reviewer.
The benefit: a proven property holds under all inputs the model represents. Bugs in the spec are still bugs, and the prover cannot help with them.
A proven property on the wrong spec is a load-bearing lie. We do not claim formal verification on engagements where the spec was not separately developed and reviewed.
What FV catches: violations of the stated spec, under the model assumptions.
What FV misses: anything outside the spec or the model. Deployment-time assumptions, off-chain integrations, external contracts the FV did not include.
Mutation testing
Mutation testing introduces deliberate bugs into the contract and runs the test suite. If the suite passes, the test suite is incomplete. If the suite fails, the test suite caught the mutation.
Tools include vertigo-rs (Crytic) and Gambit (Certora) for classical mutation testing, plus ad-hoc scripts that apply known mutations (replace < with <=, flip && to ||, etc.). The related tool necessist disables statements rather than mutating operators; it complements mutation testing rather than replacing it.
Mutation testing is most useful as a post-audit confidence measure: did the team's test suite actually catch the patterns we audited for?
The layered strategy
A protocol that takes testing seriously runs:
- Unit tests on every function, achieving full line coverage
- Integration tests against forked mainnet state for every protocol interaction
- Property-based fuzzing for every stated invariant
- Symbolic property checks on cryptographic primitives and high-stakes paths
- Formal verification on the components where the value at risk justifies the cost
- Mutation testing as a confidence check on the suite
- Mainnet-state regression tests against historical state snapshots, especially before upgrades
The audit overlays this strategy. We do not run a parallel suite; we point at gaps in the existing one and write tests where the audit hypothesis needs them.
The methodology is in our auditing methodology paper.
What clean means
A clean testing report means the protocol's stated properties survive the tests we ran. It does not mean the protocol survives properties that nobody stated. The catalog of properties is itself a deliverable.