Slither
by Trail of BitsThe de-facto-standard static analyzer for Solidity — around 90 built-in vulnerability detectors plus a powerful API for custom analyses. Fast, battle-tested, and the backbone of most automated smart-contract reviews.
The toolchain
Six engines. One verdict.
Audit Forge doesn't reinvent analysis — it orchestrates the best open-source security tools in the ecosystem and reconciles their findings by consensus. Full credit goes to their authors; each runs in an isolated, network-disabled sandbox under its own license.
Static analysis
Mythril
by Consensys DiligenceSymbolically executes EVM bytecode and uses SMT solving to reason about many reachable program states at once — surfacing reentrancy, integer bugs and unprotected operations that pure pattern-matchers miss.
Aderyn
by CyfrinA fast, modern Rust-based AST analyzer. It walks the Solidity abstract syntax tree to surface vulnerabilities and code-quality issues with clean, readable output — a superb newer addition to the ecosystem.
Semgrep
by Semgrep, Inc.A language-aware, semantic pattern scanner. Audit Forge runs the community smart-contract ruleset (p/smart-contracts) to catch known anti-patterns by code structure rather than raw text.
Solhint
by ProtofireThe most widely used Solidity linter, covering both security best-practices and style conventions. Audit Forge treats its purely-stylistic rules as informational and weights its findings conservatively.
Echidna
by Trail of BitsA sophisticated property-based fuzzer for the EVM. You declare invariants; Echidna generates transaction sequences to try to break them — a counterexample is a proof of a violation, not a heuristic. Opt-in (slower).
Why combine static analysis, symbolic execution and fuzzing?
No single technique finds every class of smart-contract bug. Audit Forge runs three complementary families of analysis and reconciles them — a finding confirmed by independent methods is far more trustworthy than one raised by a lone tool.
Static & AST analysis
Slither and Aderyn read your Solidity (and its abstract syntax tree) without executing it — fast, broad coverage of known vulnerability patterns, access-control mistakes and code-quality issues.
Symbolic execution
Mythril explores many reachable program states at once with an SMT solver, reasoning about what inputs could trigger reentrancy, overflow or unprotected operations — depth that pattern matching can't reach.
Property fuzzing
Echidna generates transaction sequences to actively try to violate invariants you declare. A counterexample is a concrete proof of a bug, not a heuristic guess.
Audit Forge is an orchestration + consensus layer over these tools, and is itself open source (AGPL-3.0). The tools are independent projects; no affiliation or endorsement is implied.