Smart Contract Auditing Tools
Tools do not find bugs; auditors do. But the right tools, applied at the right point in the engagement, dramatically expand the surface area an auditor can cover in a fixed amount of time. This section catalogs the established tools by category, explains what each is good at, and shows how they fit together in a layered analysis pipeline.
A Taxonomy of Tools
Audit tooling falls into a handful of families. Each family answers a different question and has its own characteristic strengths and failure modes.
| Family | The question it answers | Typical tools |
|---|---|---|
| Static analysis | "What patterns in the source look suspicious?" | Slither, Aderyn, Wake, Semgrep, Solhint |
| Symbolic / concolic execution | "What inputs would make this assertion false?" | Mythril, Halmos, hevm, Manticore |
| Stateless fuzzing | "Does this function hold its invariants under random inputs?" | Foundry testFuzz_*, Echidna (assertion mode) |
| Stateful (invariant) fuzzing | "Does the system hold its invariants under random sequences of calls?" | Foundry invariant tests, Echidna, Medusa |
| Formal verification | "Can I prove that this invariant holds for all reachable states?" | Certora, Halmos, hevm symbolic, K Framework, SMTChecker |
| Differential testing | "Does the new implementation behave identically to the reference?" | Foundry fork tests, hevm equiv, custom harnesses |
| Mutation testing | "Does the test suite actually catch bugs?" | slither-mutate, vertigo-rs, Wake mutator |
| Decompilation / on-chain forensics | "What does this deployed bytecode actually do?" | Heimdall, Dedaub, Panoramix, Tenderly, Phalcon |
The right strategy is layered: cheap, fast tools first (static analysis, mutation tests), then expensive ones (fuzzing, symbolic execution, formal verification) focused on the areas the cheaper tools and the manual review flagged.
How the Sections in This Chapter Are Organized
The following subsections cover the most common tools in depth, in roughly the order an auditor encounters them on an engagement:
- Slither — first-pass static analysis; nearly always run on day one.
- Mythril — symbolic execution for path-sensitive checks.
- Echidna — property-based fuzzing.
- MythX — historically a SaaS analysis platform; current status and successors.
- Certora — commercial formal verification, used on the largest protocols in the space.
- Foundry — the integrated framework that ties most of the above together for day-to-day use.
Adjacent tools — Aderyn, Halmos, Medusa, Heimdall, hevm, Wake, Diligence Fuzzing — are described in the toolbox section (§4.5.1) and in the fuzzing and formal-verification chapters (§4.8, §4.9).
What Tools Are Not
A few cautions worth stating before diving into specific tools:
- A clean static-analyzer run does not mean the code is safe. It means the analyzer's detectors did not flag anything. There is no detector for "the business logic allows free withdrawals from anyone's balance" — only a reader can find that.
- A passing fuzz campaign does not mean the invariant holds. It means the fuzzer did not happen to find a violation in the time and call sequences it explored. Formal verification is the only technique that can prove an invariant; fuzzing strongly suggests but does not guarantee.
- A formal proof is only as good as its specification. A proof of the wrong property is worse than no proof — it provides false confidence. Auditors should review the spec at least as carefully as the implementation.
- Tool output must be triaged by a human. False positives are the norm in static analysis; false negatives are the norm everywhere. Reading tool output without skepticism produces either thousands of irrelevant findings or a thin report that misses the issue that mattered.
With those caveats in place, the subsections below cover each major tool in turn, with installation, basic usage, and typical role in an audit.