DeFi Security AllianceRequest an audit
Menu

DeFi Security Alliance · Tool directory

Web3 & smart contract security tools

Find tools for code review, fuzzing, formal verification, transaction analysis, wallet protection and security operations. Compare what each tool does, where it fits and what its results cannot establish.

Listed tools
156
Categories
21
Review date

Choose by security task

Search the directory

Find a tool for your security task

Browse 24 entries at a time, ordered by primary task and name. Search and filters cover all 156 tools. Confirm exact chain and version support at the source.

25-48 of 156 tools.Download CSV
  • EVMRepository

    Kontrol

    Apply K-based reasoning to Foundry-style Solidity tests when a property needs symbolic verification.

    Documentation reviewed

    Limitations & source status
    Before using
    Proof claims depend on harness assumptions, supported features and completed proof obligations.
    Source status
    Documentation reviewed
  • EVMRepository

    Manticore

    Script symbolic execution of smart contracts and binaries for research and legacy analysis.

    Legacy / unmaintained

    Limitations & source status
    Before using
    The repository is archived and the owner no longer maintains the project.
    Source status
    Legacy / unmaintained
  • EVMRepository

    Mythril

    Explore EVM bytecode with symbolic execution to find potential contract vulnerabilities.

    Documentation reviewed

    Limitations & source status
    Before using
    Path exploration and time bounds can leave relevant execution sequences unexplored.
    Source status
    Documentation reviewed
  • EVMRepository

    Act

    Write declarative specifications of contract behavior and use them in verification workflows.

    Documentation reviewed

    Limitations & source status
    Before using
    A specification must capture intended behavior. Omitted properties remain unchecked.
    Source status
    Documentation reviewed
  • EVMWeb app / service

    Certora Prover

    Express contract rules in CVL and check them with the Certora verification service.

    Documentation reviewed

    Limitations & source status
    Before using
    Specifications, summaries and environmental assumptions define what a successful proof establishes.
    Source status
    Documentation reviewed
  • RustRepository

    Creusot

    Write Rust specifications and discharge verification conditions through a deductive verification toolchain.

    Documentation reviewed

    Limitations & source status
    Before using
    Unmodeled dependencies and incomplete proofs limit the guarantee for the full application.
    Source status
    Documentation reviewed
  • RustRepository

    Kani

    Check Rust properties with bounded model checking and obtain counterexamples for failing assertions.

    Documentation reviewed

    Limitations & source status
    Before using
    Bounds and modeled Rust behavior limit coverage. Chain-specific account rules need separate properties.
    Source status
    Documentation reviewed
  • EVMRepository

    KEVM

    Use the K specification of EVM execution to support semantics-based contract analysis and verification.

    Documentation reviewed

    Limitations & source status
    Before using
    Requires familiarity with K and careful alignment with the relevant EVM revision.
    Source status
    Documentation reviewed
  • RustRepository

    Prusti

    Verify annotated Rust functions against contracts using the Viper verification infrastructure.

    Research / prototype notice

    Limitations & source status
    Before using
    Prototype constraints and supported language features may exclude parts of a production project.
    Source status
    Research / prototype notice
  • EVMDeveloper tool

    Solidity SMTChecker

    Use Solidity's built-in model checker to evaluate assertions and selected safety properties at compilation.

    Documentation reviewed

    Limitations & source status
    Before using
    Review unsupported features and solver results. An inconclusive result is not a proof.
    Source status
    Documentation reviewed
  • EVMRepository

    VeriSol

    Translate Solidity verification problems into a formal-analysis workflow for studying contract properties.

    Legacy / unmaintained

    Limitations & source status
    Before using
    The repository is archived. Retain it for compatible historical and research cases.
    Source status
    Legacy / unmaintained
  • RustRepository

    Verus

    Annotate Rust programs with specifications and prove properties using deductive verification.

    Documentation reviewed

    Limitations & source status
    Before using
    Proof annotations and supported Rust features require engineering effort.
    Source status
    Documentation reviewed
  • EVMRepository

    Ape Framework

    Use Python accounts, providers, compiler plugins and tests to investigate on-chain applications.

    Documentation reviewed

    Limitations & source status
    Before using
    Plugin and provider support determine the available networks and execution environment.
    Source status
    Documentation reviewed
  • EVMRepository

    Brownie

    Build Python-based deployment scripts and tests for contracts targeting the EVM.

    Documentation reviewed

    Limitations & source status
    Before using
    Pin compiler and dependency versions so another reviewer can reproduce results.
    Source status
    Documentation reviewed
  • EVMRepository

    crytic-compile

    Normalize supported smart contract build systems for analysis tools that need consistent compiler artifacts.

    Documentation reviewed

    Limitations & source status
    Before using
    An incorrect build selection can produce analysis of a different contract configuration.
    Source status
    Documentation reviewed
  • EVMRepository

    EVM Diff

    Compare published execution-level specifications of EVM-compatible chains in a structured view.

    Research / prototype notice

    Limitations & source status
    Before using
    The reviewed README describes early development and says the project should not yet be relied on.
    Source status
    Research / prototype notice
  • EVMRepository

    Hardhat

    Compile, test, deploy and debug EVM contracts in a JavaScript and TypeScript development environment.

    Documentation reviewed

    Limitations & source status
    Before using
    Testing validates the scenarios and assertions you write, not every possible execution.
    Source status
    Documentation reviewed
  • EVMRepository

    OpenZeppelin Contracts

    Build and review token, access-control, governance and utility contracts using a reusable Solidity library.

    Documentation reviewed

    Limitations & source status
    Before using
    Custom extensions and configuration still need review, even when the underlying component is audited.
    Source status
    Documentation reviewed
  • EVMRepository

    OpenZeppelin Upgrades

    Validate and manage upgradeable contracts with deployment plugins and storage-layout checks.

    Documentation reviewed

    Limitations & source status
    Before using
    Storage compatibility checks do not prove an upgrade preserves application behavior.
    Source status
    Documentation reviewed
  • EVMWeb app / service

    OpenZeppelin Wizard

    Generate a starting contract from OpenZeppelin components and selected features.

    Documentation reviewed

    Limitations & source status
    Before using
    Review generated permissions, upgrade choices and subsequent modifications before deployment.
    Source status
    Documentation reviewed
  • EVMDeveloper tool

    Remix IDE

    Inspect, compile and test Solidity contracts in a browser-based development environment.

    Documentation reviewed

    Limitations & source status
    Before using
    Use the intended compiler and execution environment when reproducing an audit finding.
    Source status
    Documentation reviewed
  • EVMRepository

    Solady

    Use optimized Solidity components as implementation references or dependencies in a contract project.

    Documentation reviewed

    Limitations & source status
    Before using
    Low-level optimizations require careful review of assumptions and integration behavior.
    Source status
    Documentation reviewed
  • EVMRepository

    solc-select

    Install and switch Solidity compiler versions when reproducing a specific contract build.

    Documentation reviewed

    Limitations & source status
    Before using
    Match the full build settings as well as the compiler version.
    Source status
    Documentation reviewed
  • EVMRepository

    solidity-coverage

    Measure which Solidity statements and branches a test suite exercises.

    Documentation reviewed

    Limitations & source status
    Before using
    High coverage can coexist with missing assertions and untested economic failure modes.
    Source status
    Documentation reviewed

From question to evidence

Choose a security tool workflow

These combinations are editorial starting points. Select the tools that match your artifact and threat model, then record enough context for another reviewer to reproduce the result.

Review a Solidity protocol

Start with
Pinned commit, compiler settings, deployment addresses and written invariants.
Expected evidence
Triaged detector findings, reproducible tests and failing invariant sequences.
Review boundary
Add roles, oracle states, upgrade paths and cross-contract assumptions that generic detectors cannot infer.
Design a contract fuzzing campaign

Check a critical property

Start with
A precise statement about balances, permissions or state transitions, plus environmental assumptions.
Expected evidence
A counterexample, a completed proof within the model or an explicitly inconclusive result.
Review boundary
Record loop bounds, external-call summaries, solver limits and proof obligations that remain open.
Define the wider audit scope

Review a Solana program

Start with
Program source, IDL where available, account constraints and the deployed program identifier.
Expected evidence
Account-state tests, fuzzing failures and a separate reproducible-build comparison.
Review boundary
Exercise signer, ownership, PDA, CPI, account-reuse and upgrade-authority assumptions.
Scope a Solana security review

Inspect an unverified EVM contract

Start with
Chain, address, runtime bytecode, implementation address where applicable and relevant transactions.
Expected evidence
Candidate functions, storage clues, reconstructed logic and traces to investigate.
Review boundary
Resolve proxies and corroborate inferred behavior. A selector lookup or decompiler cannot authenticate original source.
Investigate privileged contract behavior

Check a token before interaction

Start with
Exact chain and contract address, intended swap route and current allowance state.
Expected evidence
Dated risk signals covering permissions, trading behavior, liquidity, holders and approvals.
Review boundary
Use chain-appropriate tools. A clean scan cannot predict future owner actions or make a token an investment recommendation.
Understand honeypot-check limitations

Investigate and monitor a deployment

Start with
Contract inventory, transaction hashes, protocol invariants, alert recipients and response permissions.
Expected evidence
Reproducible traces, tested alert conditions and evidence attached to an owned incident workflow.
Review boundary
Distinguish detection from response. Test notification delivery and approval boundaries before enabling automation.
Plan on-chain monitoring

Review a zero-knowledge circuit

Start with
Circuit source, constraint artifacts, witness assumptions, public inputs and verifier integration.
Expected evidence
Constraint warnings, uniqueness results, witness tests and proof-verification artifacts.
Review boundary
Confirm the circuit encodes the intended statement, then review application binding and replay protection separately.
Review replay and domain boundaries

Check the code-to-deployment boundary

Start with
Dependency lockfiles, build configuration, artifacts, signing policy and the target deployment.
Expected evidence
Dependency findings, secret-scan results, an artifact inventory and signature-verification evidence.
Review boundary
Connect artifact identity to deployed bytecode and review the dapp frontend and administrative signing path.
Prepare an incident-response plan

Compare by the question answered

Common tool comparisons

How six common comparisons change the review workflow
ComparisonWhat differsSelection criterion
Slither vs Mythril

Slither analyzes source and compiler structures with detectors and inspection outputs.

Mythril explores EVM bytecode symbolically to seek vulnerability candidates.

Use source analysis for broad triage. Use symbolic exploration for additional execution evidence. Compare reproducible findings, not raw warning counts.
Foundry vs Echidna vs Medusa

Foundry combines development tests, invariant campaigns and fork-based workflows.

Echidna and Medusa focus on property-driven fuzzing campaigns and transaction sequences.

Run the same meaningful property and reachable-state setup before comparing campaign results. Preserve seeds, corpus, duration and tool versions.
Halmos vs Certora vs Kontrol

Halmos and Kontrol bring symbolic reasoning to Solidity-test-oriented workflows.

Certora uses CVL specifications and a verification service.

Choose based on the property, specification language, environment modeling and whether the proof completes within your resource budget.
Source verification vs security verification

Sourcify and solana-verify compare a build with a deployed artifact.

Formal tools reason about specified properties. Tests exercise selected behaviors.

Record these as separate evidence fields. A matching source build says nothing by itself about access control or economic safety.
Token scanner vs approval checker

Token scanners report selected contract, trading, holder and liquidity signals.

Approval checkers inspect permissions already granted by a wallet.

Use both for their respective questions. Revoking an allowance does not change a token contract or recover stolen assets.
Transaction simulator vs live monitor

A simulator evaluates a proposed transaction against a chosen state.

A monitor evaluates observed activity or state against configured detection rules.

Preserve the simulation inputs, then define the conditions that should trigger alerts after deployment. Neither replaces an incident owner.

Evidence & review scope

How this directory was assembled

DeFiSec reviewed 172 candidate tools and retained 156 entries across 21 categories. The September 5, 2026 source review excluded 16 candidates because of duplicate destinations or insufficient current product evidence. It retained 11 entries with legacy or maintenance notices, 5 with research or prototype notices and five supported only by provider-page evidence.

  1. Identify a concrete task. Include scanners, analyzers, testing frameworks, verification tools, investigation interfaces and supporting security infrastructure. A compiler or reporting tool is labeled by its actual role.
  2. Check a primary destination. Inspect official documentation, a project repository or the provider page; record the check date, response, redirects and content hash where available.
  3. Separate purpose from assurance. Describe the documented function and its review boundary. Documentation review does not establish runtime availability, active maintenance, license rights, price or detection quality.
  4. Preserve negative evidence. Record excluded candidates and visible maintenance notices. Count a suite once unless a separately named component has a distinct workflow.

Tools were not installed or benchmarked. Paid plans and transaction execution were not tested. Entries are not ranked by quality; inclusion is not an audit endorsement. Audit Builder is a DeFi Security Alliance product and is identified in its description.

For the wider review process, consult Ethereum's contract-testing guide, Trail of Bits' secure-contract guidanceand the OWASP Smart Contract Security Verification Standard. Product-specific evidence is linked from every card.

Practical questions

Web3 security tools FAQ

Which Web3 security tool should I start with?

Start with the artifact and question you have: source code for static analysis, a testable invariant for fuzzing, bytecode for reverse engineering or a deployed address for monitoring. Use the workflow table to assemble a small set of complementary tools, then check the source-linked requirements for your chain and build.

Are the listed tools free or open source?

The directory includes repositories, developer tools and hosted services. A public repository does not by itself establish license permissions and an accessible product page does not establish a free plan. Pricing and license terms were not audited in this review. Confirm both at the linked source.

Can a scanner or AI tool replace a smart contract audit?

A scanner can surface specific patterns or candidate findings. It cannot establish that the system meets every business rule, trust assumption or economic invariant. Require reproducible evidence for findings and review missing scenarios, integrations, privileges and deployment controls.

Which tools work for Solana, Move, Cairo, TON and CosmWasm?

Use the ecosystem filter and the dedicated categories. Solana account execution, Sui objects, Aptos resources, Starknet account contracts, TON messages and CosmWasm host behavior require different harnesses. A language label is not a promise of support for every chain or compiler version.

Does a honeypot check prove a token is safe?

It provides evidence about selected checks at a particular time. Trading routes, fees, permissions, liquidity and contract implementation can change. Record the exact chain and address and inspect individual signals instead of treating a score as a guarantee.

Why are archived and prototype tools included?

They help readers reproduce historical reports, understand older workflows and identify replacements. Legacy and research notices are visible in each affected card and can be selected with the status filter. Inclusion is not a recommendation to deploy a deprecated or experimental implementation.

What did DeFiSec actually verify?

The review checked primary repository, documentation and provider URLs, recorded response status and redirects and inspected the stated purpose and relevant maintenance notices. Five entries have only provider-page evidence and are labeled accordingly. Tools were not installed or benchmarked, paid access was not tested and detection quality was not measured.

How can I reproduce or reuse the directory review?

Download the catalog as CSV or JSON and the dated source-review CSV. Each listed tool has a source URL and check date. The source review also records exclusions, response status and a content hash where a response was obtained. These files preserve the review snapshot. They do not promise that a destination remains unchanged.