AllySec Forge

Appearance

Crypto/Blockchain Security Testing Tooling Ecosystem ​

Comprehensive Audit for AI-Powered Security Agent Construction ​

Date: 2026-06-05 ​

DOMAIN 1: Smart Contract Static Analysis and Fuzzing ​

Section 1A: Solidity/EVM Tools ​

Slither (crytic/slither) -- Trail of Bits ​

  • What: Static analysis framework for Solidity and Vyper. Runs a suite of vulnerability detectors (100+ detectors), data-flow analysis, taint tracking, and inheritance graph generation. Emits printer output and intermediate representations (SlithIR).
  • Target: Solidity (0.4.x--0.8.x), Vyper. EVM bytecode via slither-read-storage.
  • Language: Python 3.
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 6,282
  • Install: pip install slither-analyzer (requires solc binary, managed via crytic-compile / solc-select). Docker image: trailofbits/eth-security-toolbox.
  • CLI/API: First-class CLI (slither .). Also usable as a Python library (from slither import Slither). JSON output via --print and SARIF export via --sarif. Has a printer-to-JSON mode that returns structured findings. Strongly LLM-integrable -- the JSON output is machine-parseable and the Python API allows scripted invocation.
  • Primary Strength: Breadth of detectors, data-flow precision, and the SlithIR intermediate representation enables custom detectors. The de facto standard for Solidity static analysis.
  • Docs Quality: Excellent. Full documentation at crytic.io, GitHub wiki, and extensive Python API docs.

Mythril (ConsenSysDiligence/mythril) -- Consensys Diligence ​

  • What: Symbolic execution engine for EVM bytecode. Uses concolic analysis, taint tracking, and control-flow checking to detect security vulnerabilities. Explores execution paths symbolically to find states where security properties are violated.
  • Target: EVM bytecode (language-agnostic -- works on compiled Solidity and Vyper).
  • Language: Python 3.
  • Open Source: Yes, MIT.
  • GitHub Stars: 4,248
  • Install: pip install mythril (also through eth-security-toolbox Docker image). Historically available as a SaaS API called MythX (now deprecated/shuttered).
  • CLI/API: CLI: myth analyze <file.sol>. JSON output with --format json. Can be invoked as a library. LLM-integrable via CLI with JSON output.
  • Primary Strength: Symbolic execution finds deep, path-dependent bugs that pattern-matching static analysis misses. Good for reentrancy, integer overflow/underflow, and unchecked call return values.
  • Docs Quality: Decent -- GitHub README, wiki. Somewhat lagging behind Slither in maintenance frequency.
  • Note: Development pace has slowed. MythX SaaS was sunset. The open-source tool remains functional but receives fewer updates than Slither.

Echidna (crytic/echidna) -- Trail of Bits ​

  • What: Property-based fuzzer for EVM. The user writes invariants as Solidity functions with echidna_ prefix. Echidna generates random sequences of transactions and checks if invariants hold. Uses coverage-guided mutation to maximize code exploration.
  • Target: Solidity (via crytic-compile + solc). EVM bytecode.
  • Language: Haskell (compiled binary).
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 3,146
  • Install: Pre-built binaries from GitHub releases. Docker image trailofbits/echidna. Also via nix and Homebrew.
  • CLI/API: CLI: echidna test contract.sol. Outputs plain text. Configurable via echidna.config.yaml. JSON output limited -- the primary output is console text. Moderately LLM-integrable -- CLI works but parsing the textual output requires custom regex/adapter.
  • Primary Strength: Finds complex state-dependent bugs through randomized transaction sequences. Excellent for invariants around token balances, access control, and arithmetic properties.
  • Docs Quality: Good. Comprehensive wiki on GitHub. Trail of Bits blog posts with tutorials.
  • Note: Echidna's development has slowed as Medusa (its Go-based successor) is the preferred next-generation tool. However, Echidna remains the most battle-tested fuzzer in production.

Foundry / Forge (foundry-rs/foundry) ​

  • What: Blazing-fast Ethereum development toolkit written in Rust. forge is the test runner that includes built-in fuzzing (property-based and stateless), invariant testing, gas profiling, and differential fuzzing against live chains. cast is the RPC CLI. anvil is a local testnet node. chisel is a REPL.
  • Target: Solidity, Vyper. EVM.
  • Language: Rust (tooling), Solidity (tests).
  • Open Source: Yes, MIT/Apache-2.0 dual.
  • GitHub Stars: 10,380
  • Install: foundryup (official installer script). Pre-built binaries. cargo install foundry-cli (if building from source).
  • CLI/API: First-class CLI. forge test with -vvvv verbosity. forge test --fuzz-runs 10000. JSON output via --json. Invariant testing via forge test with handler contracts. forge coverage for code coverage. Strongly LLM-integrable -- JSON output, clean CLI design, standard Solidity test format means an AI agent can write test files and run them easily.
  • Primary Strength: Speed (Rust-based, compiled), all-in-one ecosystem, and the de facto standard for modern Solidity development. Fuzzing is seamlessly integrated into the test framework -- every parameterized test is automatically fuzzed. Invariant testing with handler contracts is powerful.
  • Docs Quality: Excellent. book.getfoundry.sh is comprehensive. Active community, Paradigm-funded.
  • Note: The forge invariant testing mode (invariant_ prefix) is a direct competitor to Echidna/Medusa but built into the mainstream dev workflow.

Hardhat (NomicFoundation/hardhat) ​

  • What: TypeScript-based Ethereum development environment. Compiles, deploys, tests, and debugs smart contracts. Massive plugin ecosystem. Includes hardhat-network for local forking.
  • Target: Solidity, Vyper. EVM.
  • Language: TypeScript/JavaScript.
  • Open Source: Yes, MIT.
  • GitHub Stars: 8,476
  • Install: npm install --save-dev hardhat. Version 3.8.0 (as of June 2026).
  • CLI/API: npx hardhat test. JSON output via --json in some plugins. Primarily programmatic API via JavaScript/TypeScript (hardhat.config.ts). Moderately LLM-integrable -- an AI agent can write Hardhat scripts in TypeScript and invoke them. The JS programmatic interface is flexible. Hardhat console (npx hardhat console) provides a REPL.
  • Primary Strength: Plugin ecosystem, mainnet forking, TypeScript ergonomics, and the largest user base in the ecosystem. Console.log() debugging in Solidity.
  • Docs Quality: Excellent. hardhat.org documentation is thorough. Active Nomic Foundation maintenance.
  • Note: Hardhat's fuzzing is limited compared to Foundry. Many projects use Hardhat for deployment/scripting and Foundry for testing. Hardhat v3 (released) adds significant improvements.

Manticore (trailofbits/manticore) ​

  • What: Symbolic execution engine supporting multiple platforms including Ethereum/EVM. Can symbolically execute smart contracts to find inputs that trigger specific code paths, detect assertion violations, and generate test cases.
  • Target: EVM bytecode, Linux ELF binaries, WASM.
  • Language: Python 3.
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 3,857
  • Install: pip install manticore. Docker: trailofbits/manticore.
  • CLI/API: CLI: manticore contract.sol. Python API is the primary interface. JSON output available. LLM-integrable via Python API (an AI agent can write Manticore analysis scripts).
  • Primary Strength: Multi-architecture symbolic execution. Can find extremely deep vulnerabilities that require specific input values. Generates concrete test cases from symbolic paths.
  • Docs Quality: Good. GitHub wiki and Trail of Bits blog. API documentation available.
  • Note: Development pace has slowed. Manticore requires significant computational resources for all but the simplest contracts. Good for deep analysis of critical contracts, not for batch scanning.

MedusaFuzz (crytic/medusa) -- Trail of Bits ​

  • What: Parallelized, coverage-guided, mutational Solidity smart contract fuzzer. The designated successor to Echidna. Written in Go for performance and parallelism. Supports multiple workers, corpus management, and advanced fuzzing strategies.
  • Target: Solidity. EVM bytecode.
  • Language: Go.
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 476
  • Install: Pre-built binaries from GitHub releases. go install github.com/crytic/medusa/cmd/medusa@latest.
  • CLI/API: CLI: medusa fuzz. Configuration via medusa.json. Output to console and test corpus directory. Moderately LLM-integrable -- CLI is clean but output parsing needs work.
  • Primary Strength: Parallel fuzzing with coverage guidance. Significantly faster than Echidna for multi-core machines. Designed for CI/CD integration. Active development.
  • Docs Quality: Good. GitHub repository docs. Still maturing relative to Echidna's decade of battle-testing.
  • Build vs Buy: BUY -- this is the future of EVM fuzzing. However, it's still proving itself. Echidna has more documented discoveries. For an AI agent, support both.

Aderyn (Cyfrin/aderyn) ​

  • What: Rust-based Solidity static analyzer designed for speed and IDE integration. Built by Cyfrin (Patrick Collins / Cyfrin Updraft). Detects common Solidity vulnerabilities and code quality issues.
  • Target: Solidity.
  • Language: Rust.
  • Open Source: Yes, MIT.
  • GitHub Stars: 776
  • Install: Pre-built binaries from GitHub releases. cargo install aderyn.
  • CLI/API: CLI: aderyn . (runs in a directory). JSON output via --output json. SARIF output for IDE integration. Strongly LLM-integrable -- clean JSON output, fast execution, designed for programmatic consumption.
  • Primary Strength: Speed (Rust -- orders of magnitude faster than Slither for large repos). IDE integration (VS Code, Neovim). Beginner-friendly output with fix suggestions.
  • Docs Quality: Good. Cyfrin documentation. Growing community around Cyfrin's educational ecosystem.
  • Note: Fewer detectors than Slither (~50 vs 100+), but rapidly growing. The Cyfrin team is well-funded and actively developing.

4nalyzer / 4naly3er ​

  • What: A Solidity report generator that produces structured markdown reports from Slither/Aderyn output or custom detector results. Used widely in Code4rena and competitive audit contexts. Can be run as a GitHub Action to auto-generate audit reports from PRs.
  • Target: Solidity (wraps Slither/other tools).
  • Language: TypeScript (likely).
  • Open Source: Yes (specific repo uncertain -- check for 4naly3er or solidity-analyzer-action).
  • GitHub Stars: N/A (multiple implementations exist).
  • Install: GitHub Action or npm package. Used as npx 4naly3er or via GitHub Actions workflow.
  • CLI/API: CLI wraps other tools. Outputs structured markdown reports. Moderately LLM-integrable -- useful as a report standardization layer. An AI agent could parse the markdown reports or invoke the GitHub Action.
  • Primary Strength: Standardized report format. Heavily used in competitive audits. Bridges the gap between raw tool output and human-readable findings.
  • Docs Quality: Varies by implementation. Generally minimal.

Halmos (a16z/halmos) ​

  • What: Symbolic testing tool for EVM smart contracts. Uses symbolic execution to find violations of assertions written as Foundry tests. Unlike Echidna (random fuzzing), Halmos reasons symbolically about all possible paths up to a bound.
  • Target: Solidity (Foundry test suite). EVM.
  • Language: Python 3.
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 1,011
  • Install: pip install halmos. Requires Foundry to be installed. Integrates with Foundry test suites.
  • CLI/API: CLI: halmos --function check_something. JSON output. Strongly LLM-integrable -- clean CLI, JSON output, integrates with existing Foundry test infrastructure.
  • Primary Strength: Finds bugs that require specific symbolic inputs where fuzzing would miss them. Complements Echidna/Medusa/Foundry fuzz: fuzzing finds shallow bugs fast, Halmos proves deep bugs with symbolic reasoning.
  • Docs Quality: Good. a16z Crypto blog posts. GitHub README.
  • Note: Resource-intensive. Best for targeted invariant analysis, not whole-project scanning.

HEVM (argotorg/hevm) ​

  • What: Symbolic and concrete EVM execution engine. Originally developed within the DappHub ecosystem (dapptools), now maintained by argotorg. Used for symbolic unit testing of Solidity contracts. The symbolic execution engine behind dapptools' testing capabilities.
  • Target: EVM bytecode. Solidity.
  • Language: Haskell.
  • Open Source: Yes. Code is open (AGPL-3.0).
  • GitHub Stars: 339
  • Install: Nix. nix build github:argotorg/hevm. Binary available.
  • CLI/API: CLI: hevm symbolic --code <bytecode>. SMT solver backend (Z3 by default). Moderately LLM-integrable -- CLI exists but Haskell tooling has a steep learning curve. Output format is not designed for machine parsing.
  • Primary Strength: Mature symbolic execution for EVM. SMT solver integration. The original symbolic EVM that inspired Halmos and others.
  • Docs Quality: Sparse. Largely driven by the dapptools ecosystem documentation.
  • Note: Foundry's symbolic testing (forge test --z3) is gradually absorbing HEVM's use cases. HEVM remains relevant for niche deep-symbolic analysis but Foundry has won the mainstream.

Certora Prover ​

  • What: Commercial formal verification tool for smart contracts. Users write specifications in CVL (Certora Verification Language). The prover mathematically proves that the contract satisfies the spec for all possible inputs and states, or produces a counterexample.
  • Target: Solidity (EVM).
  • Language: Proprietary (CVL spec language). Cloud service + CLI client.
  • Open Source: No. Proprietary commercial product. The CVL spec language and examples are open, but the prover engine is closed-source.
  • GitHub Stars: ~242 (Tutorials repo only). The prover itself is not on GitHub.
  • Install: pip install certora-cli. Requires a Certora Prover license key.
  • CLI/API: CLI: certoraRun contract.sol --spec spec.cvl. Outputs verification results (satisfied/violated + counterexample). Moderately LLM-integrable -- CLI is clean but the commercial license requirement limits automation scale. An AI agent could write CVL specs and invoke certoraRun.
  • Primary Strength: Mathematical proof of correctness. Finds bugs that no amount of fuzzing or static analysis could reliably catch. The gold standard for high-value contracts (lending protocols, bridges).
  • Docs Quality: Excellent. Certora documentation portal. Tutorials and example specs.
  • Build vs Buy: BUY for critical contracts. Cannot be self-hosted or open-source-replaced.

Scribble (ConsenSysDiligence/scribble) ​

  • What: Runtime verification and instrumentation tool for Solidity. Users annotate contracts with properties (pre/post-conditions, invariants) using a specification language. Scribble instruments the contract to check these properties at runtime during testing or fuzzing.
  • Target: Solidity.
  • Language: TypeScript.
  • Open Source: Yes, Apache-2.0.
  • GitHub Stars: 334
  • Install: npm install -g scribble-cfg-cli or pip install scribble.
  • CLI/API: CLI: scribble contract.sol --arm. Outputs an instrumented contract or runs checks. Moderately LLM-integrable -- CLI works but the annotation-first workflow requires human annotation of the codebase before tools run.
  • Primary Strength: Bridges static and dynamic analysis. Properties written once can be checked by Echidna, Mythril, and during testing. Property annotations also serve as inline documentation.
  • Docs Quality: Decent. Consensys Diligence docs. GitHub README.
  • Note: The annotation language is powerful but slows adoption -- teams must invest in writing specs. See also Certora for a more powerful (commercial) alternative.

Surya ​

  • What: Solidity visualization tool. Generates inheritance graphs, function call graphs, and contract dependency diagrams. Useful for understanding complex contract architectures during manual review.
  • Target: Solidity.
  • Language: JavaScript (Node.js).
  • Open Source: Yes (historically Consensys/surya, may have been moved or renamed).
  • GitHub Stars: ~1,000 (estimate, historical data).
  • Install: npm install -g surya.
  • CLI/API: CLI: surya graph contracts/**/*.sol. Outputs Graphviz DOT files. Weakly LLM-integrable -- generates visualizations for human consumption, not structured data for AI analysis. An AI agent could parse the DOT output though.
  • Primary Strength: Architecture visualization. Quickly reveals overly complex inheritance or unexpected dependencies.
  • Docs Quality: Sparse. README only.

solc-select (crytic/solc-select) ​

  • What: Solidity compiler version manager. Downloads, installs, and switches between solc versions. Essential infrastructure for any tool that needs to compile contracts with specific compiler versions.
  • Target: Solidity compiler binaries.
  • Language: Python 3.
  • Open Source: Yes, AGPL-3.0.
  • GitHub Stars: 810
  • Install: pip install solc-select. solc-select install 0.8.19. solc-select use 0.8.19.
  • CLI/API: CLI: solc-select use <version>. Essential infrastructure -- not a security tool per se, but required for running other tools. An AI agent automatically needs this.
  • Primary Strength: Reliable compiler version management. Used by Slither, Echidna, and virtually all Trail of Bits tooling.
  • Docs Quality: Good enough (README). Simple tool, simple docs.

Wake (Ackee-Blockchain/wake) ​

  • What: Python-based Solidity development and fuzz testing framework with built-in vulnerability detectors. An all-in-one alternative to Foundry/Hardhat. Includes compilation, testing, fuzzing, and a VS Code extension.
  • Target: Solidity. EVM.
  • Language: Python 3.
  • Open Source: Yes, ISC.
  • GitHub Stars: 366
  • Install: pip install wake (or pip install eth-wake). VS Code extension available.
  • CLI/API: CLI: wake init, wake test. Python API for scripting. LLM-integrable via Python API -- an AI agent can write Wake test scripts in Python, which is natural for Python-based agents.
  • Primary Strength: Python-native framework with built-in detectors. More accessible to Python developers than Foundry (Rust) or Hardhat (TypeScript). Growing ecosystem.
  • Docs Quality: Good. Documentation at docs.getwake.io.
  • Note: Smaller community than Foundry/Hardhat. Interesting as a Python-native option for AI agents.

Ape (ApeWorX/ape) ​

  • What: Python-based smart contract development framework. Plugin architecture. Integrates with multiple compilers, networks, and testing tools.
  • Target: Solidity, Vyper. EVM.
  • Language: Python 3.
  • Open Source: Yes, Apache-2.0.
  • GitHub Stars: 1,045
  • Install: pip install ape. Plugins via ape plugins install <name>.
  • CLI/API: CLI: ape compile, ape test. Python scripting API. Moderately LLM-integrable -- Python-native, so AI agents can write Ape scripts naturally.
  • Primary Strength: Plugin ecosystem and Python ergonomics. Supports multiple chains (Ethereum, Polygon, Avalanche, etc.).
  • Docs Quality: Good. docs.apeworx.io.
  • Note: Competes with Brownie (also Python-based). Brownie is more established but Ape is actively maintained by ApeWorX/Curve community.

Brownie (eth-brownie/brownie) ​

  • What: Python-based development and testing framework for Ethereum. Uses pytest. Includes built-in brownie test with coverage and fixtures.
  • Target: Solidity, Vyper. EVM.
  • Language: Python 3.
  • Open Source: Yes, MIT.
  • GitHub Stars: 2,728
  • Install: pip install eth-brownie.
  • CLI/API: CLI: brownie test. Python API: brownie module. Moderately LLM-integrable -- Python-native. An AI agent can write and run Brownie tests.
  • Primary Strength: Python-native with pytest integration. Large community. Well-documented.
  • Docs Quality: Good. eth-brownie.readthedocs.io.
  • Note: Brownie's development has slowed. Many teams have migrated to Foundry for testing speed. Still widely used for deployment scripts and integration testing. Watch: Brownie may be in maintenance mode.

Section 1B: Rust/Go/Move (Non-EVM) Tools ​

cargo-audit (RustSec/rustsec) ​

  • What: Audits Rust project dependencies (Cargo.lock) against the RustSec Advisory Database. Flags crates with known security vulnerabilities (CVEs, RUSTSEC advisories).
  • Target: Rust/Cargo projects. Not blockchain-specific but essential for any Rust-based blockchain project (Solana, Sui, Aptos, CosmWasm).
  • Language: Rust.
  • Open Source: Yes, Apache-2.0/MIT.
  • GitHub Stars: 1,896 (rustsec repo, which includes cargo-audit).
  • Install: cargo install cargo-audit. Or cargo audit (if bundled).
  • CLI/API: CLI: cargo audit. JSON output via --json. Strongly LLM-integrable -- clean CLI, JSON output, standard CI integration.
  • Primary Strength: Fast, accurate dependency vulnerability scanning. Essential CI step for any Rust blockchain project.
  • Docs Quality: Good. docs.rs/cargo-audit. RustSec documentation.
  • Note: Not a static analysis tool -- only checks known CVEs in dependencies. Use alongside cargo-deny for license and security policies.

cargo-geiger ​

  • What: Scans Rust projects and reports unsafe code usage statistics. Counts unsafe blocks, functions, and dependencies. Generates a report with a "geiger counter" visualization showing radiation (unsafe code) levels.
  • Target: Rust/Cargo projects.
  • Language: Rust.
  • Open Source: Yes (available on crates.io, GitHub).
  • GitHub Stars: ~1,500 (estimated).
  • Install: cargo install cargo-geiger.
  • CLI/API: CLI: cargo geiger. Output to terminal. JSON output available. Moderately LLM-integrable -- an AI agent can run it and parse the report for projects with high unsafe code.
  • Primary Strength: Quick audit of unsafe Rust surface area. Useful during due diligence of Rust-based protocols (Solana programs, CosmWasm contracts).
  • Docs Quality: Adequate (README + help text).
  • Note: High unsafe count does not necessarily mean vulnerable -- it flags code that needs deeper manual review.

Move Prover (move-language/move) ​

  • What: Formal verification tool for Move smart contracts. Part of the Move language toolchain. Users write specifications in the Move specification language (MSL). The prover verifies that the Move bytecode satisfies the spec.
  • Target: Move bytecode (Aptos, Sui, Movement, and other Move-based chains).
  • Language: Rust (Move compiler and prover).
  • Open Source: Yes, Apache-2.0.
  • GitHub Stars: 2,334 (Move repo).
  • Install: cargo install move-prover (from move-language repo). Or via Aptos CLI (aptos move prove).
  • CLI/API: CLI: move prove or aptos move prove. Outputs verification results. Moderately LLM-integrable -- CLI works, but writing Move specs requires domain expertise. An AI agent could write specs and invoke the prover.
  • Primary Strength: Formal verification is deeply integrated into the Move language design. Much stronger guarantees than EVM tooling because Move was designed with verification in mind.
  • Docs Quality: Good. Move book documentation. Aptos developer docs.
  • Note: Only applies to Move-based chains. The Move ecosystem (Aptos, Sui) is growing but still a fraction of EVM's market.

Soteria -- Solana/Anchor Security Auditor ​

  • What: Security analysis tool for Solana programs (formerly by Sec3 / Shade Protocol). Detects common Solana-specific vulnerabilities: missing signer checks, account deserialization bugs, cross-program invocation (CPI) safety issues, and ownership validation errors.
  • Target: Solana programs (Rust, Anchor framework).
  • Language: Rust.
  • Open Source: Uncertain -- was historically open but commercial wrap may exist. Check sec3-sol/soteria or ShadeProtocol/soteria.
  • GitHub Stars: ~200 (estimated).
  • Install: cargo install soteria or via Docker.
  • CLI/API: CLI for scanning Solana programs. Moderately LLM-integrable if CLI is available.
  • Primary Strength: Solana-specific vulnerability patterns that general Rust tools miss (e.g., missing signer constraint on accounts that hold funds).
  • Docs Quality: Limited. Solana security tooling is less mature than EVM.
  • Note: The Solana security ecosystem is immature compared to EVM. Many Solana auditors rely on manual review + Anchor framework checks. The Anchor framework itself has built-in validations.

Anchor (coral-xyz/anchor) -- Solana Framework ​

  • What: The dominant development framework for Solana programs. While primarily a development framework, Anchor includes anchor test for testing and several built-in security checks (account validation, constraint verification).
  • Target: Solana programs (Rust).
  • Language: Rust.
  • Open Source: Yes, Apache-2.0.
  • GitHub Stars: ~3,500 (estimated -- repo name may differ).
  • Install: cargo install anchor-cli or via AVM (Anchor Version Manager, like solc-select for Solana).
  • CLI/API: anchor test. Moderately LLM-integrable -- an AI agent can write Anchor tests and invoke anchor test.
  • Primary Strength: Security through constraints. Anchor's #[account(constraint = ...)] annotations catch many vulnerabilities at compile time or test time.
  • Docs Quality: Excellent. anchor-lang.com and Solana developer docs.
  • Note: Not a security tool per se, but the security guarantees from Anchor's constraint system are the primary defense for Solana programs.

Section 1C: ZK Circuit Analysis Tools ​

Ecne (Veridise) ​

  • What: R1CS (Rank-1 Constraint System) constraint verification tool. Automatically verifies properties of ZK circuits expressed as R1CS constraints. Detects under-constrained circuits where private inputs can be chosen to forge proofs.
  • Target: Circom (and other R1CS-generating languages).
  • Language: Research tool from Veridise. Likely Rust or Python.
  • Open Source: Partially -- Veridise publishes research and tools but may have commercial extensions.
  • GitHub Stars: Research tool, limited public stars.
  • Install: Research artifact. May not have a clean package.
  • CLI/API: Research CLI. Weakly LLM-integrable -- research-grade tooling.
  • Primary Strength: Automated detection of under-constrained R1CS circuits -- the most critical ZK circuit vulnerability class.
  • Docs Quality: Academic paper + research code. Not production documentation.
  • Note: Veridise is the leading research firm for ZK circuit security. Their commercial audit service uses proprietary versions of these tools.

Circomspect ​

  • What: Static analysis tool for Circom circuits. Originally by QED (Trail of Bits spinoff). Detects common pitfalls in Circom code: signal shadowing, unconstrained signals, missing constraints, and template misuse.
  • Target: Circom (the dominant ZK circuit language for Groth16, PLONK).
  • Language: Rust (likely).
  • Open Source: Yes (historically).
  • GitHub Stars: ~100-200 (estimated).
  • Install: cargo install circomspect or pre-built binary.
  • CLI/API: CLI: circomspect circuit.circom. Outputs structured warnings. Moderately LLM-integrable -- clean CLI, an AI agent can parse the output.
  • Primary Strength: Catches easy-to-miss Circom mistakes that lead to under-constrained circuits. The equivalent of a Solidity linter for Circom.
  • Docs Quality: README + blog posts. Minimal.
  • Note: The Circom ecosystem is small. Tooling is sparse. Most serious ZK audits combine Circomspect + manual review + Veridise's research tools.

Picus (Veridise) ​

  • What: Automated verification of uniqueness (under-constrained circuit detection) for ZKP circuits. Symbolic evaluation of circuit constraints to find missing constraints where an attacker can generate multiple valid proofs for the same public inputs.
  • Target: Circom circuits. R1CS.
  • Language: Research tool from Veridise.
  • Open Source: Partially. Veridise maintains a public fork at Veridise/Picus (94 stars, fork).
  • GitHub Stars: 94 (Veridise fork).
  • Install: Research artifact.
  • CLI/API: Research CLI. Weakly LLM-integrable -- research-grade tooling.
  • Primary Strength: Finds the most dangerous class of ZK circuit bugs: under-constrained circuits that break soundness of the proof system.
  • Docs Quality: Academic paper (Usenix Security). Not production documentation.
  • Note: More advanced than Circomspect but harder to use. Likely requires Veridise expertise.

QED ​

  • What: ZK circuit prover and verifier testing framework. Aims to provide a comprehensive testing environment for ZK circuits, including property-based testing and proof validation.
  • Target: ZK circuits (Circom, and others).
  • Language: Rust.
  • Open Source: Uncertain -- may be commercial. Related to the QED protocol and the team behind Trail of Bits' ZK practice.
  • GitHub Stars: N/A.
  • Install: Unknown.
  • Note: The ZK circuit security tooling space is extremely nascent. Most tools are research prototypes. The primary methodology for ZK audits is still manual review enhanced by Circomspect + academic tools.

Halo2 Analyzer / zcash/halo2 ​

  • What: The Halo2 proving system (zcash/halo2, 907 stars) is the primary ZK framework for Zcash and many projects. No dedicated security analyzer tool exists for Halo2. Security analysis is done through the Halo2 development framework itself + manual review.
  • Target: Halo2 circuits (Rust).
  • Language: Rust.
  • Open Source: Yes (halo2), Apache-2.0/MIT.
  • GitHub Stars: 907 (halo2 core).
  • Install: cargo add halo2 (as a dependency).
  • CLI/API: Library, not a CLI tool. Halo2 circuits are Rust code, so standard Rust testing (cargo test) is the primary verification method.
  • Primary Strength: Halo2 circuits are written in Rust, meaning all Rust tooling (cargo-audit, cargo-geiger, clippy, miri) applies.
  • Note: The Halo2 team at Zcash/Electric Coin Co. uses custom internal tooling for circuit analysis. None of this is public.

DOMAIN 2: Blockchain Protocol and P2P Security ​

Network/P2P Fuzzing ​

  1. DevP2P Fuzzing (Ethereum):

    • eth-fuzzer: Marius Van Der Wijden's (Ethereum Foundation) devp2p fuzzing framework. Written in Go. Fuzzes Ethereum's devp2p protocol at the wire level -- sends malformed discovery packets (v4, v5 disc), malformed RLPx handshakes, and malformed eth protocol messages. Found multiple critical consensus split bugs in Geth, Nethermind, and Erigon.
      • Install: go install github.com/MariusVanDerWijden/eth-fuzz@latest (approximately).
      • LLM Integration: CLI tool. An AI agent could orchestrate fuzzing sessions against Ethereum clients.
    • Ethereum Protocol Fuzzing (go-ethereum): Geth's internal fuzzing harnesses in go-ethereum/p2p/discover/ and go-ethereum/eth/protocols/. These are embedded in the client, not standalone tools.
    • GossipSub Fuzzing: libp2p GossipSub protocol is used by Ethereum consensus layer (CL). The libp2p/go-libp2p-pubsub includes internal fuzzing harnesses. Nadir Akhtar (Consensys) published research on GossipSub fuzzing in 2023.

  2. libp2p Fuzzing: libp2p has an internal fuzzing framework in libp2p/test-plans/. Not packaged as a standalone tool. For external fuzzing, tools like go-fuzz, libfuzzer, and AFL++ are used against libp2p implementations.

  3. Solana Turbine Fuzzing: Solana's Turbine (block propagation) protocol has no publicly available fuzzing tool. Solana Labs runs internal fuzzing. The Solana Foundation bug bounty program provides scope for Turbine attacks.

Consensus Fuzzing ​

  1. eth-fuzzer (consensus): The same eth-fuzzer can fuzz consensus by sending blocks with invalid state transitions. Marius Van Der Wijden also maintains tx-fuzz for transaction pool fuzzing.

  2. Antithesis: A deterministic simulation platform. Not open-source (commercial SaaS). Injects faults systematically and explores all possible orderings of concurrent events. Used by the Ethereum Foundation to test consensus clients in a controlled environment. Found bugs in Lighthouse, Prysm, and Teku.

    • Install: Commercial platform. Cloud-based.
    • LLM Integration: API-driven. An AI agent could trigger Antithesis test runs and parse results.
    • Note: Antithesis is the gold standard for distributed systems testing. Expensive ($10k+/month). The Ethereum Foundation has a partnership.

  3. Deterministic Simulation Testing (DST):

    • Foundry's forge test in multi-chain fork mode can simulate cross-contract interactions deterministically.
    • Kurtosis: Ethereum testnet orchestration platform. Can spin up multi-client testnets for consensus testing.
    • Helios: a16z's light client. Not a security tool per se.

  4. ethereum/consensus-specs tests: The official Ethereum consensus spec tests (ethereum/consensus-spec-tests) are a massive corpus of test vectors used by all consensus clients. These are the industry standard for consensus compliance.

Eclipse Attack Detection ​

  • Eclipse Attack Detection: No dedicated standalone tool. Researchers (Heilman, Kendler, Zohar, Goldberg) have published methodologies. In practice:
    • Monitor peer table diversity (distribution of peer /24 subnets, ASNs).
    • Geth's admin.peers RPC exposes peer metadata.
    • Custom monitoring dashboards at infrastructure level.

MEV Detection/Extraction ​

  1. Flashbots MEV-Boost / MEV-Inspect: The Flashbots MEV ecosystem. mev-inspect-py and mev-inspect-rs parse Ethereum blocks to extract MEV transactions (arbitrage, sandwich, liquidation).

    • Open Source: Yes (Flashbots).
    • LLM Integration: An AI agent can run MEV inspectors and analyze MEV extraction patterns.

  2. EigenPhi MEV Data: Commercial data provider for MEV analytics.

  3. libmev: Open-source MEV extraction library. For offensive testing (sandwich attack simulation).

Mempool (Transaction Pool) Analysis ​

  1. txpool / mempool sniffing: Geth exposes txpool_content RPC. Nethermind, Erigon have similar APIs. The mempool can be observed by running a full node.
  2. Blocknative: Commercial mempool monitoring service with API.
  3. Eden Network: Mempool streaming.
  4. Custom tools: Python scripts using web3.py + websocket subscriptions to pendingTransactions. Trivially LLM-integrable (an AI agent can write mempool monitoring scripts).

DOMAIN 3: Cryptographic and Key Management ​

Key Generation Audit Tools ​

  1. Project Wycheproof (Google): Test vectors for cryptographic libraries. Detects known weak implementations (biased nonces, invalid curve attacks, small subgroup attacks). Not blockchain-specific but essential for auditing cryptographic primitives used in wallets.

    • Install: git clone. Test vectors in JSON.
    • LLM Integration: An AI agent can run Wycheproof test vectors against wallet libraries.

  2. parity-ethereum/ethkey: Ethereum key generation and inspection (now archived). Reference implementation for key derivation.

  3. BIP39 Audit Tools:

    • bip39tool: CLI tool for BIP39 mnemonic generation and seed derivation. Can test entropy quality.
    • iancoleman/bip39: Web-based BIP39 tool. Not CLI-friendly but reference implementation.

  4. ECC Key Validation:

    • Check for keys in small subgroups.
    • Check for low-order public keys.
    • Verify that the private key is in the valid range [1, n-1].

MPC/TSS Implementation Testing ​

  1. MP-SPDZ: Academic framework for secure multi-party computation. Can be used to benchmark and test MPC implementations.
  2. ZK-Garage/MPC audits: Research papers, not packaged tools. The MPC/TSS audit space relies heavily on manual cryptographic review.
  3. GG18 / GG20 TSS implementations: Binance tss-lib, ZenGo multi-party-ecdsa, Fireblocks. No commercial test suite -- manual review is the standard.
  4. Threshold Signature Testing: Test vectors and edge case testing largely ad hoc.

Entropy Assessment ​

  1. NIST SP 800-22 Test Suite: Statistical test suite for random number generators. Can be applied to wallet entropy sources.
  2. dieharder: Statistical RNG test suite.
  3. TestU01: Academic RNG test suite (more stringent than NIST).
  4. Wallet entropy testing: No dedicated wallet entropy audit tool. Requires custom testing pipeline combining the above with BIP39 generation replay.

Nonce Reuse Detection ​

  1. Sherlock / Nonce Reuse Detection: The classic ECDSA nonce reuse attack (recovering private key from two signatures with same k). Multiple implementations exist:
    • Python scripts: Open-source scripts scan blockchain transactions for nonce reuse. Private key recovery from reused (r, s) pairs.
    • ethereum-nonce-reuse-detector: Various GitHub repos (~50-200 stars each).
    • Blockchain ETL + Custom Scripts: An AI agent can trivially write nonce reuse detection scripts.
  2. Biased Nonce Detection: More sophisticated than outright reuse. Lattice-based attacks (Howgrave-Graham, Smart) can recover keys from biased nonces (e.g., nonces with 64 bits of entropy in a 256-bit field). Tools:
    • lattice-attack: Python implementations of lattice-based ECDSA key recovery.
    • ecdsa-nonce-bias-detector: Various academic implementations.

DOMAIN 4: Bridge and Interop Security ​

Cross-Chain Message Verification Testing ​

The bridge security space is dominated by manual review + formal verification. Few automated tools exist.

  1. Wormhole Security:

    • Wormhole Guardian Testing: Wormhole validators use a majority-vote scheme. Testing involves simulating validator set corruption.
    • Wormhole VAA (Validator Action Approval) Testing: Replay and forgery testing via custom scripts.
    • The Wormhole team runs internal testing infrastructure.

  2. LayerZero Security:

    • LayerZero DVN (Decentralized Verifier Networks): Security depends on Oracle + Relayer collusion resistance.
    • Forced message replay testing.
    • Config verification (UA/endpoint configuration, packet verification).
    • No public security testing suite. LayerZero received a Code4rena competitive audit and several Spearbit audits.

  3. Axelar Security:

    • Axelar uses threshold signatures (TSS) across validators for cross-chain messages.
    • Testing focuses on TSS implementation correctness and validator set key rotation.
    • No public testing suite.

Proof Validation (SPV, ZK, Oracle-Based Bridges) ​

  1. SPV Proof Validation:

    • SPV proofs for light client bridges (e.g., IBC, Rainbow Bridge).
    • Testing involves generating invalid SPV proofs and verifying the bridge rejects them.
    • Custom test harness per bridge -- no general tool.

  2. ZK Bridge Proof Testing:

    • ZK-based bridges (Polygon zkEVM bridge, zkSync bridge, Scroll bridge) require circuit-level testing (see Domain 1C tools) plus proof verification on-chain.
    • Proof forgery testing: Attempt to generate valid proofs for invalid state transitions.

  3. Oracle-Based Bridge Testing:

    • Chainlink CCIP uses DON (Decentralized Oracle Network) for cross-chain messaging.
    • Testing involves price oracle manipulation and cross-chain message forgery.

Generic Bridge Testing Methodology ​

  • Replay protection: Test cross-chain if messages can be replayed.
  • Message ordering: Test if message sequence numbers can be manipulated.
  • Upgradeability: Test if bridge proxy upgrades can be hijacked.
  • Validator set takeover: For PoS bridge validators, simulate stake-based attacks.
  • Relayer collusion: For relayer-based bridges, simulate relayer corruption.

DOMAIN 5: Methodology and Professional Practices ​

Trail of Bits (ToB) Blockchain Audit Methodology ​

  • Phases:
    1. Scoping and Kickoff: Define audit scope, timeline, and deliverables. Identify key invariants and threat model with the client.
    2. Documentation Review: Review whitepapers, technical specs, architecture diagrams. Identify assumptions and security properties.
    3. Automated Analysis: Run Slither, Echidna, Manticore, and custom tooling. Slither printers generate inheritance graphs, call graphs, and data dependency maps.
    4. Manual Review: Line-by-line code review. Focus on business logic, access control, and novel patterns that automated tools miss. Use SlithIR to trace data flow.
    5. Property-Based Testing: Write Echidna/Medusa invariants. Run fuzzing campaigns. Symbolic execution with Manticore for critical functions.
    6. Report Writing: Findings classified by severity (Critical, High, Medium, Low, Informational). Each finding includes: description, impact, proof of concept, and remediation.
    7. Fix Review: Review client's patches. Verify fixes don't introduce new issues.
  • Deliverables: Detailed audit report (PDF), raw tool output, test suites (Echidna properties, Manticore scripts).
  • Manual vs Automated Ratio: ~70% manual, ~30% automated. Trail of Bits invests heavily in proprietary tooling but emphasizes that tools find ~20-30% of bugs. The rest require human reasoning.
  • Tooling: Heavy use of Slither, Echidna, Manticore, Crytic-compile, solc-select. Their entire stack is open-source (crytic GitHub org).

Spearbit / Code4rena Competitive Audit Approach ​

  1. Spearbit:

    • Model: Boutique audit firm. Hand-picked security researchers (many ex-ToB, OpenZeppelin).
    • Phases:
      1. Pre-audit Review: Researchers self-study the codebase for 1-2 weeks.
      2. Collaborative Review: Group sessions with the client. Walkthrough of architecture and key risks.
      3. Individual Auditing: Solo deep-dive by each researcher.
      4. Triaging and Report: Spearbit lead triages findings. Report delivered.
      5. Fix Review: Lead reviewers verify fixes.
    • Ratio: ~80% manual, ~20% automated. Spearbit researchers bring their own toolchains.
    • Deliverables: Audit report (findings + severity), sometimes interactive review sessions.
    • Pricing: $50k-$200k per engagement. Premium positioning.

  2. Code4rena (C4):

    • Model: Competitive audit platform. Sponsors put up a prize pool. Wardens (auditors) compete to find bugs. Findings are submitted, judged, and ranked. Prizes distributed by leaderboard position.
    • Phases:
      1. Sponsor Onboarding: Codebase, documentation, scope, and prize pool set.
      2. Warden Review Period: Typically 4-21 days. Wardens submit findings privately.
      3. Judging: C4 judges triage and validate findings. Severity classification. Leaderboard published.
      4. Sponsor Fix Period: Sponsor fixes bugs. Wardens may verify fixes.
      5. Post-Audit Report: Findings published. Prize pool distributed.
    • Ratio: ~90% manual (warden-driven), ~10% automated. Wardens use static analysis tools for initial triage (Slither, Aderyn, 4nalyzer) but most finding depth comes from manual review.
    • Deliverables: Public audit report on the C4 website, GitHub issues per finding.
    • Community: 1000+ registered wardens. Findings tend to identify more bugs than traditional audits due to the competitive dynamic.

OpenZeppelin Audit Process ​

  • Phases:
    1. Scoping: Define audit scope, timeline, and risk parameters.
    2. Initial Review: Team of 2-4 auditors reviews documentation and code. Architectural analysis.
    3. Line-by-Line Review: Manual code review using OpenZeppelin's extensive internal checklist and playbook. Focus on:
      • Access control correctness.
      • Token standard compliance (ERC-20, ERC-721, ERC-1155).
      • Upgrade safety (UUPS, transparent proxies, beacon proxies).
      • Governance attack vectors (flash loan governance attacks, vote delegation bugs).
      • Reentrancy, front-running, DoS, oracle manipulation.
    4. Automated Analysis: Run Slither, internal tooling. Use OpenZeppelin test suite extensions.
    5. Report: Findings with severity, description, and fix recommendations.
    6. Remediation Review: Verify fixes, re-test.
  • Ratio: ~75% manual, ~25% automated.
  • Deliverables: Professional audit report (PDF), test artifacts.
  • Tooling: Slither, internal Zeppelin-specific detectors, OpenZeppelin Defender for monitoring.
  • Pricing: $50k-$500k depending on scope.

Consensys Diligence ​

  • Phases: Similar to OpenZeppelin:
    1. Scoping and quote.
    2. Automated analysis (Mythril, Scribble, internal tools).
    3. Manual review (pair or solo auditor).
    4. Report and fix review.
  • Tooling: Mythril, Scribble, VS Code audit extensions. Legacy of the Consensys tooling ecosystem.
  • Note: Consensys Diligence has shifted focus. MythX (SaaS) was sunset. The audit practice continues but with reduced tooling investment compared to ToB.
  • Ratio: ~70% manual, ~30% automated.

Guardian Audits / Zellic / Veridise ​

  1. Zellic:

    • Boutique firm. Known for creative attack discovery.
    • Process: Triage (2 auditors, 2-3 days) -> Deep Review (1-2 auditors, 1-2 weeks) -> Report.
    • Heavy on manual creative attacks. Light on automated tooling reliance.
    • Deliverables: Report with PoC, occasionally exploit scripts.

  2. Veridise:

    • Specializes in ZK circuit audits and formal verification.
    • Process: Run Picus, Ecne, and proprietary internal tools (not publicly available). Then manual review of circuit and on-chain verification logic.
    • Deliverables: Report with formal verification results (for ZK circuits, "proved not under-constrained" for each signal).
    • Most advanced ZK audit methodology in the industry.

  3. Guardian Audits:

    • Smaller firm. Competitive audit-style engagement (borrows from C4 model).
    • Process: Time-boxed review period, collaborative triage, report.

Cross-Firm Patterns ​

PhaseTypical DurationTool Involvement
Scoping/Quoting3-7 daysNone
Documentation Review2-5 daysNone
Automated Analysis1-3 daysHigh (Slither, Echidna, Certora, etc.)
Manual Review5-15 daysLow (code navigation, custom scripts)
Property/Spec Writing2-5 daysMedium (Echidna invariants, Certora specs)
Reporting2-5 daysLow (LaTeX/Word/C4 format)
Fix Review2-5 daysLow (diff review, re-test)

Manual vs Automated: Industry consensus is that automated tools find 20-35% of vulnerabilities. The remaining 65-80% require human reasoning about business logic, access control, and protocol-specific invariants. This is the primary opportunity for AI-assisted auditing -- closing the gap between what tools find and what humans find.

DOMAIN 6: AI-Assisted Crypto Auditing ​

Current State (June 2026) ​

The AI-assisted crypto audit space is nascent but moving fast. The primary model is LLM as augmented auditor -- the AI doesn't replace the human but dramatically accelerates the human's workflow.

Anthropic's Claude for Vulnerability Research ​

  1. "Glasswing" / "Claude Mythos": Anthropic has not publicly released a product called "Glasswing" or "Claude Mythos." These appear to be speculative or internal-only project names. What is known:

    • Anthropic has invested in vulnerability research capabilities for Claude.
    • Claude 4 (Opus, Sonnet) has improved code analysis capabilities, including understanding of Solidity/Rust and the ability to reason about security properties.
    • Claude can review Solidity code and identify common vulnerability patterns (reentrancy, access control issues, arithmetic bugs).
    • Anthropic has not released crypto-audit-specific tooling. Claude can be used as a code reviewer via the standard API, but has no special crypto-mode.

  2. Known Limitations of LLM-Only Auditing:

    • Hallucination: LLMs confidently assert bugs that don't exist.
    • Context window: Large contracts exceed token limits.
    • Tool integration: LLMs cannot natively run Slither/Foundry -- they need an agent harness.
    • Novel patterns: LLMs struggle with protocol-specific invariant violations that don't match known patterns.

AI-Assisted Crypto Audit Tools ​

  1. (Project Name Unknown) -- Cyfrin/AI Auditor: Cyfrin has explored AI-assisted auditing as part of their educational platform (Cyfrin Updraft). They use AI for:

    • Automated code explanation (explaining what a contract does).
    • Initial vulnerability triage.
    • No fully automated AI auditor product yet.

  2. Slither + GPT Integration: Community experiments combining Slither output with GPT-4 for enhanced finding descriptions:

    • Feed Slither findings to LLM to generate human-readable descriptions.
    • Feed SlithIR (intermediate representation) to LLM to ask questions about data flow.
    • Several open-source prototypes on GitHub.

  3. ChatGPT + Codebase RAG: Retrieval Augmented Generation (RAG) approaches:

    • Index the entire smart contract codebase.
    • Query: "Find all places where owner can drain funds."
    • The LLM retrieves relevant code sections and reasons about them.
    • This is the most promising near-term approach.

Claroty Team82's Ghidra MCP Server Approach ​

Claroty Team82 (ICS/SCADA security researchers) pioneered an influential pattern for AI-assisted vulnerability research:

  1. Architecture:

    • Ghidra MCP Server: A Model Context Protocol (MCP) server that wraps Ghidra's (NSA's reverse engineering tool) capabilities.
    • An AI agent (e.g., Claude via MCP) can interact with the Ghidra MCP server to:
      • Decompile binary functions.
      • Search for cross-references.
      • Analyze control flow.
      • Rename variables.
      • Run Ghidra scripts.
    • The AI agent becomes a "pair-programmer" for the reverse engineer, handling repetitive analysis tasks.

  2. Relevance to Crypto Auditing:

    • The MCP pattern maps directly: Slither MCP Server, Foundry MCP Server, Echidna MCP Server.
    • An AI agent with access to these MCP servers could:
      • Run slither . and receive structured findings.
      • Query "show me the data flow from msg.sender to selfdestruct" via SlithIR.
      • Write an Echidna invariant and run echidna test to verify.
      • Deploy to a local fork and execute attack sequences via cast + forge.
      • Generate a 4nalyzer-report from the combined tool output.

  3. Build Decision: Building MCP servers for Slither, Foundry, Hardhat, and Echidna is the single highest-leverage activity for an AI-powered crypto audit agent. This is the Claroty pattern applied to smart contracts.

LLM Integration with Foundry/Slither ​

Foundry LLM Integration:

  • Foundry has a clean CLI with JSON output (--json). An AI agent can:
    • Run forge build --json to get compilation artifacts.
    • Run forge test --json to get test results.
    • Run forge snapshot for gas analysis.
    • Run forge inspect <contract> storage --pretty to read storage layout.
    • Write Foundry scripts in Solidity and execute them via forge script.
  • Integration Method: CLI invocation with JSON parsing. No MCP server needed initially -- a thin wrapper is sufficient.

Slither LLM Integration:

  • Slither provides a Python API (from slither import Slither). An AI agent can:
    • Load a contract via Slither("contract.sol").
    • Iterate through detectors: slither.run_detectors().
    • Query data dependencies: variable.data_dependences.
    • Generate call graphs as DOT/JSON.
    • Export SARIF for standardized vulnerability format.
  • Integration Method: Python library import. For JavaScript agents, invoke via python3 -c or build a Slither JSON-RPC server.

Recommendations for AI-Powered Crypto Audit Agent ​

  1. Phase 1 (Minimum Viable Agent):

    • Integrate: Slither, Foundry/forge, solc-select, Aderyn.
    • Capability: Run tools, parse JSON output, produce a structured findings report.
    • Pattern: Simple CLI wrappers -- parse stdout/stderr. No MCP needed.

  2. Phase 2 (Interactive Agent):

    • Build MCP servers: Slither MCP, Foundry MCP, Echidna MCP.
    • Capability: The AI agent can query contract structure, write and run fuzz tests, modify invariants, and iteratively explore the codebase.
    • Pattern: Follow Claroty Team82's Ghidra MCP architecture. Use Anthropic's MCP protocol.

  3. Phase 3 (Full Audit Agent):

    • Add: Certora Prover integration (write CVL specs), Halmos symbolic testing, Medusa fuzzing.
    • Add: ZK circuit analysis (Circomspect, Picus integration).
    • Add: Attack simulation (deploy to anvil fork, execute attack sequences, verify profit).
    • Add: Report generation with 4nalyzer-style structured output.
    • Pattern: Orchestrator agent dispatches sub-agents for static analysis, dynamic analysis, and formal verification. Results are correlated and a final report is generated.

Summary: Build vs Buy Decision Matrix ​

ToolStatusPriority for AI AgentRationale
SlitherOpen Source, 6.3k starsPHASE 1 -- MUST INTEGRATEDe facto standard. Python API. JSON output.
Foundry/forgeOpen Source, 10.4k starsPHASE 1 -- MUST INTEGRATEDominant framework. JSON output. Fuzzing + symbolic.
solc-selectOpen Source, 810 starsPHASE 1 -- MUST INTEGRATEDependency for Slither/Foundry.
AderynOpen Source, 776 starsPHASE 1 -- SHOULD INTEGRATEFast, complementary to Slither.
HardhatOpen Source, 8.5k starsPHASE 2 -- SHOULD INTEGRATELarge user base. Plugin ecosystem.
EchidnaOpen Source, 3.1k starsPHASE 2 -- SHOULD INTEGRATEBattle-tested fuzzer. Still the reference.
MedusaOpen Source, 476 starsPHASE 3 -- WATCH/INTEGRATEEchidna successor. Active development.
Certora ProverCommercialPHASE 3 -- WATCHRequires license. Gold standard for formal verification.
HalmosOpen Source, 1k starsPHASE 2 -- SHOULD INTEGRATESymbolic testing for Foundry.
ManticoreOpen Source, 3.9k starsPHASE 3 -- NICE TO HAVEResource-intensive. Deep symbolic.
MythrilOpen Source, 4.2k starsPHASE 2 -- SHOULD INTEGRATESymbolic execution. Complement to Slither.
ScribbleOpen Source, 334 starsPHASE 3 -- NICE TO HAVERequires annotation. Powerful when used.
cargo-auditOpen Source, 1.9k starsPHASE 2 -- MUST INTEGRATEEssential for Rust-based protocols.
Move ProverOpen Source (Move)PHASE 3 -- INTEGRATE IF MOVE TARGETSOnly for Move-based chains.
ZK Tools (Circomspect, Picus, Ecne)Research/AcademicPHASE 3 -- INTEGRATE FOR ZK TARGETSImmature. Research-grade.
Ghidra MCP PatternOpen patternPHASE 2 -- BUILDThe Claroty Team82 architecture. Highest-leverage build.

Key Takeaways ​

  1. The EVM tooling ecosystem is mature but fragmented. Slither + Foundry + Echidna cover ~80% of automated analysis needs. No single platform integrates them all well.

  2. The non-EVM ecosystem is immature. Solana has Soteria + Anchor. Move has Move Prover. Rust has cargo-audit. ZK circuits have research prototypes. This is a gap and an opportunity.

  3. Formal verification (Certora, Move Prover) is the high end. For critical contracts (bridges, lending protocols), formal verification finds bugs that no amount of fuzzing can find. Certora requires a commercial license.

  4. AI-assisted auditing is the frontier. The Ghidra MCP pattern (Claroty Team82) is the most promising architecture. Building MCP servers for Slither, Foundry, and Echidna is the highest-leverage build activity.

  5. Competitive audit platforms (Code4rena) produce the most findings per dollar. The competitive model consistently finds 2-5x more bugs than traditional audits. An AI agent should emulate the competitive auditor workflow: rapid scanning with tools, then deep manual (AI-assisted) review of flagged areas.

Released under the MIT License.

Copyright 2026 AllySecLabs — The Allied Security Research Guild