Static Analysis
Tools that analyze code without executing it.
Slither
The industry standard static analyzer from Trail of Bits. 80+ detectors covering common vulnerabilities, code quality, and optimization.
Aderyn
Rust-based static analyzer from Cyfrin. Fast analysis with growing detector library.
Solhint
Solidity linter for style and security. Catches common issues early.
Semgrep
Pattern-based code analysis. Write custom rules for project-specific issues.
Amarna
Static analyzer for Cairo/StarkNet contracts. Check the GitHub repo for documentation and examples.
Symbolic Execution
Tools that explore all possible program paths mathematically.
Mythril
Symbolic execution for detecting security vulnerabilities through constraint solving.
Halmos
Symbolic testing tool from a16z. Proves properties through symbolic execution.
HEVM
Symbolic execution engine from DappTools. Deep analysis of EVM bytecode.
Pyrometer
Abstract interpretation for finding numeric issues like overflows.
Manticore
Symbolic execution engine supporting EVM and native binaries.
Fuzzing
Tools that test contracts with random inputs to find edge cases.
Echidna
Property-based fuzzer from Trail of Bits. Tests invariants through random input generation.
Foundry Fuzz
Fast fuzzing built into Foundry. First-choice for most projects.
Medusa
Parallel fuzzer compatible with Echidna tests. Better performance on multi-core systems.
Chimera
Framework for building reusable fuzz tests across protocols.
Harvey
Greybox fuzzer that uses coverage to guide input generation.
Formal Verification
Tools that mathematically prove contract properties.
Certora Prover
Commercial formal verification platform. Industry standard for critical protocols.
Solidity SMTChecker
Built-in formal verification in Solidity compiler. Free and open-source.
Act
Specification language for formal verification of smart contracts.
K Framework
Formal semantics framework. Used for EVM formal semantics. Free and open-source.
Debugging and Analysis
Tools for understanding contract behavior.
Tenderly
Transaction simulation and debugging. Trace transactions step by step.
Foundry Debugger
Interactive debugger for stepping through transactions. Free and open-source.
Etherscan
Block explorer with verified source code, transaction traces, and decompilation.
Phalcon
Transaction explorer from BlockSec showing detailed execution traces.
Dedaub
Decompiler and contract analysis. See contract logic without source.
Code Review
Tools that aid manual code review.
VS Code Solidity
Essential VS Code extension with syntax highlighting and IntelliSense.
Solidity Visual Developer
VS Code extension with interactive graphs, metrics, and call trees.
Sol2UML
Generate UML diagrams from Solidity contracts. Check the GitHub repo for documentation and examples.
Surya
Utility for contract analysis including call graphs and function summaries.
Audit Workflow
Tools for managing the audit process.
Code4rena
Competitive audit platform. Participate in audits or submit protocols.
Sherlock
Audit marketplace with insurance component. Used by production teams across the ecosystem.
Immunefi
Bug bounty platform for Web3. Find vulnerabilities for rewards.
Notion/Obsidian
Note-taking tools for organizing findings and audit documentation.
Reference and Research
Resources for staying current and learning.
SWC Registry
Smart Contract Weakness Classification. Standard vulnerability taxonomy.
Rekt News
Post-mortems of DeFi hacks. Essential reading for auditors. Free and open-source.
DeFiHackLabs
Repository of exploit reproductions. Learn attack patterns hands-on.
Solodit
Database of audit findings from public reports. Free and open-source.
Key Recommendations
Run Slither first on every audit. It catches low-hanging fruit and gives you a codebase overview.
Combine static analysis with fuzzing. Static tools find code patterns; fuzzers find edge cases.
Reproduce past exploits to understand attack patterns. DeFiHackLabs is invaluable.
Use Tenderly to trace live transactions when investigating suspicious behavior.
Build your own checklist from audit reports. Solodit is a goldmine for this.