Tooling: Slither, Echidna, Mythril, Manual Review

What you'll learn

• The Layered Defense
• Slither: Static Analysis (Trail of Bits)
• Echidna: Property-Based Fuzzing (Trail of Bits)
• Symbolic Execution: Mythril and Halmos
• Formal Verification: Certora Prover
• Why Manual Review Still Dominates

Key terms

Slither

Open-source static analyzer for Solidity from Trail of Bits (2018), the de facto baseline tool. Catches 80+ common bug patterns via SlithIR detectors. Runs in seconds; should be in CI on every PR.

Echidna

Property-based fuzzer for smart contracts from Trail of Bits. Coverage-guided; generates random transaction sequences to find one that violates a stated invariant. Catches sequence-dependent bugs that static analysis misses.

Foundry forge invariant

Foundry's built-in invariant fuzzer. Operates on the same conceptual model as Echidna but integrates with the rest of Foundry's testing tooling. Increasingly the first-pass fuzzer for most teams.

Mythril

Symbolic execution tool from ConsenSys Diligence (2017). Built on Z3. Identifies issues via the SWC registry: integer over/underflow, reentrancy, delegatecall misuse, unchecked external calls.

Halmos

Bounded-model-checking symbolic executor from a16z crypto (2023). Operates on Foundry-style tests, proving assertions hold for all inputs within bounded scope. Open-source middle path between pure fuzzing and full formal verification.

Certora Prover

Commercial formal verification platform for smart contracts. Uses the Certora Verification Language (CVL) to specify properties, mathematically proves them for the implementation. Used by Aave, MakerDAO, Compound, Lido, Balancer, and others.

SlithIR

Slither's intermediate representation of Solidity code. Detectors operate on SlithIR rather than raw Solidity, making pattern detection more reliable.

Property-based fuzzing

Testing methodology where developers state invariants ("total supply equals sum of balances") and a coverage-guided fuzzer searches for any execution sequence that violates them. The right primary tool for sequence-dependent bug classes.

Symbolic execution

Treats inputs as symbolic variables and explores all execution paths simultaneously, using an SMT solver (Z3) to find inputs that reach specific code or violate properties. Powerful but limited by path explosion in complex contracts.

Formal verification

Mathematically proves an implementation matches a specification for all possible inputs in the spec's scope. The strongest assurance available, but expensive (six-figure engagements) and reserved for highest-value primitives.