Slither vs Mythril vs Echidna: What Each Tool Catches

Run Slither on a contract with a reentrancy bug, and you'll get a finding in under 5 seconds. Run Mythril on the same contract, and it'll find the same bug — plus a path to exploit it that Slither missed. Run Echidna, and it'll find a state sequence that neither of the other two considered.

Each tool uses a fundamentally different approach. Slither reads your code and matches patterns. Mythril executes your code symbolically, exploring every possible path. Echidna throws random inputs at your code and checks if anything breaks.

None of them is "the best." They catch different things. This article shows you exactly what each one does, how to run it, what its output looks like, and where it fails — so you can build a testing stack that covers your attack surface.

The 30-Second Version

Slither: The Pattern Matcher

Slither (by Trail of Bits) is a static analyzer. It reads your Solidity source, builds an intermediate representation called SlithIR, and runs detectors against it. It never executes your code.

How it works

Slither parses your contracts into a control flow graph and data flow graph, then checks those graphs against ~90 built-in detectors. Each detector looks for a specific pattern: like an external call before a state update (reentrancy), or an unchecked return value, or tx.origin used for authentication.

Running it

# Basic scan: runs all detectors
slither .

# Target specific vulnerabilities
slither . --detect reentrancy-eth,reentrancy-no-eth,unprotected-upgrade

# Output as JSON (for CI/CD integration)
slither . --json output.json

# Only show high/medium severity findings
slither . --filter-paths "node_modules" --exclude-informational --exclude-low

Real output on a vulnerable contract

Given this contract:

contract UnsafeVault {
    mapping(address => uint) public balances;

    function withdraw(uint _amount) external {
        require(balances[msg.sender] >= _amount);
        (bool ok, ) = msg.sender.call{value: _amount}("");
        require(ok);
        balances[msg.sender] -= _amount;
    }
}

Slither outputs:

Reentrancy in UnsafeVault.withdraw(uint256):
    External calls:
    - (ok) = msg.sender.call{value: _amount}()
    State variables written after the call(s):
    - balances[msg.sender] -= _amount

Reference: https://github.com/crytic/slither/wiki/Detector-Documentation#reentrancy-vulnerabilities

Found in 3 seconds. No compilation needed beyond the standard solc pass.

Where Slither falls short

Slither matches patterns. If your reentrancy vulnerability is hidden behind three layers of internal function calls, or if the external call is made through an interface that Slither can't resolve, it might miss it. It also can't reason about cross-contract interactions: if Contract A calls Contract B which calls back into Contract A, Slither sees the call in A but doesn't model B's behavior.

More concretely: Slither would not have caught the Nomad Bridge bug ($190M). That was a logic error in message validation — the code matched no known vulnerability pattern. Syntactically valid code that did the wrong thing.

Slither catches known vulnerability patterns. Novel bugs that match no existing detector go undetected.

Mythril: The Path Explorer

Mythril (by ConsenSys Diligence) takes a different approach entirely. Instead of reading patterns in source code, it compiles your contract to EVM bytecode and then symbolically executes it — meaning it explores every possible execution path with symbolic (not concrete) inputs.

How it works

For each function, Mythril asks: "What values could the inputs take, and where does each combination lead?" It tracks path constraints (conditions that must be true for each branch) and uses an SMT solver (Z3) to determine whether a path is reachable. When it finds a path that leads to a known vulnerability condition (like sending ETH to an attacker-controlled address before updating state), it generates a concrete input that triggers it.

This is why Mythril is slower than Slither: Mythril executes your code symbolically, exploring every possible path rather than reading patterns from source.

Running it

# Analyze a single file
myth analyze contracts/Vault.sol

# Set execution timeout (default can be slow)
myth analyze contracts/Vault.sol --execution-timeout 300

# Analyze deployed contract by address
myth analyze --address 0x1234...abcd --rpc infura

# Increase exploration depth for complex contracts
myth analyze contracts/Vault.sol --max-depth 50 --execution-timeout 600

What Mythril finds that Slither misses

Mythril's strength is exploitable paths. Where Slither says "there's an external call before a state update," Mythril says "here's the exact sequence of transactions an attacker would execute to drain $X."

It also finds vulnerabilities that depend on specific input values. Integer overflows that only trigger when a balance exceeds a threshold. Delegatecall exploits that only fire when a specific storage slot contains a specific value. Transaction ordering issues where the outcome depends on which of two pending transactions executes first.

Where Mythril falls short

Path explosion. On a contract with many branches, Mythril's exploration space grows exponentially. A complex DeFi protocol with 30+ functions and multiple conditional paths can take hours to analyze — and still not reach full coverage. Increasing --max-depth helps but also increases runtime.

No business logic understanding. Mythril checks for known vulnerability classes (reentrancy, overflow, delegatecall abuse). It has no way to know that your lending protocol should never allow a user to borrow more than their collateral value. That kind of invariant requires Echidna.

This is exactly the gap Echidna fills.

Echidna: The Property Breaker

Echidna (also Trail of Bits) is a fuzzer. You tell it what should always be true about your contract (invariants), and it tries to prove you wrong by throwing thousands of random transaction sequences at it.

How it works

You write properties: Solidity functions that return true if the contract is in a valid state. Echidna then generates random sequences of function calls with random arguments and checks whether any sequence violates a property. When it finds one, it gives you the minimal sequence that breaks it.

This is fundamentally different from Slither and Mythril. They look for bugs they already know about. Echidna looks for any behavior that violates your specification — including bugs nobody has seen before.

Running it

# Run with default settings
echidna . --contract TestVault --test-mode assertion

# Run with more iterations for better coverage
echidna . --contract TestVault --test-mode assertion --test-limit 50000

# Run in property mode (checks functions starting with echidna_)
echidna . --contract TestVault --test-mode property

Writing properties: the part most teams skip

The power of Echidna is entirely dependent on the quality of your properties. Bad properties = bad coverage.

contract TestVault is UnsafeVault {
    
    // Property: no user can withdraw more than they deposited
    function echidna_no_excess_withdrawal() public view returns (bool) {
        return address(this).balance >= 0; 
        // Weak property: almost always true
    }
    
    // Better property: total balances must equal contract balance
    function echidna_balance_invariant() public view returns (bool) {
        // This catches reentrancy, overflow, and logic errors
        return totalTrackedBalances == address(this).balance;
    }
    
    // Property: withdrawing should reduce balance exactly by amount
    function echidna_withdraw_correctness() public returns (bool) {
        uint before = balances[msg.sender];
        uint amount = before / 2; // Withdraw half
        if (amount == 0) return true;
        
        withdraw(amount);
        return balances[msg.sender] == before - amount;
    }
}

When Echidna breaks echidna_balance_invariant, it outputs something like:

echidna_balance_invariant: failed!
  Call sequence:
    deposit() Value: 1000000000000000000
    withdraw(1000000000000000000)
    withdraw(1000000000000000000)  // Re-entrant call

That's a reproducible exploit path. Not a warning — a proof.

Where Echidna falls short

It only finds what you tell it to look for. If you don't write a property for a specific invariant, Echidna won't check it. Teams that define 3 weak properties and call it done get a false sense of security.

Echidna is also probabilistic: it might miss a violation that requires a very specific sequence of 15 transactions with exact parameter values. Increasing --test-limit helps but doesn't guarantee complete coverage.

📖 Related: Smart Contract Security: The Complete DeFi Guide

Head-to-Head: Same Bug, Three Tools

Let's run all three against our UnsafeVault reentrancy bug and see what each one reports.

That last row is the key insight. Slither and Mythril catch known vulnerability classes. Echidna catches violations of your specific business logic. You need both.

The Practical Stack: When to Use What

On every commit: Slither

# .github/workflows/security.yml
name: Security Check
on: [push, pull_request]
jobs:
  slither:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v3
      - uses: crytic/slither-action@v0.3.0
        with:
          fail-on: high
          slither-args: --filter-paths "node_modules|test"

Fast enough to run on every push. Catches the obvious stuff before it reaches the PR review.

Before every release: Mythril + Echidna

Run Mythril with a generous timeout on your core contracts (the ones that hold or move funds). Run Echidna with properties covering your critical invariants — at minimum:

• Total balances track correctly
• Access control holds (no unauthorized state changes)
• No function can drain more than deposited
• Oracle-dependent logic handles extreme prices

Before audit: All three, with results documented

Hand your auditor the tool outputs alongside the code. A good audit firm will run their own tools, but giving them yours saves time and shows you've done the baseline work. This can reduce audit cost by 15-25% — auditors spend less time on the issues you've already found and fixed. 📖 Related: Smart Contract Audit Cost: 2026 Pricing Guide

What None of These Tools Catch

No automated tool will find:

Economic exploits. Flash loan attacks that manipulate prices across protocols require understanding the economic system as a whole. A lending protocol's code can pass every audit and still get drained if its oracle can be manipulated within a single block.

Governance attacks. Beanstalk lost $182M to a governance exploit. The code worked as designed — the problem was that the design allowed flash-loaned voting power.

Cross-contract composability bugs. When Protocol A calls Protocol B, and B's behavior changes in a way A didn't expect — neither Slither nor Mythril models the full multi-protocol interaction.

Off-chain dependencies. Keeper bots, frontend vulnerabilities, centralized API endpoints, key management. The smart contract can be perfect and the system still gets exploited.

Automated tools are the first layer of a security stack. They catch the 40-60% of vulnerabilities that follow known patterns. The rest requires manual review, economic analysis, and adversarial thinking.

At BugBlow, we use all three tools as the starting point for every audit — not the conclusion. Our manual review starts where the tools stop. See our methodology →

FAQ

Which tool should I start with if I've never used any?

Slither. Install it (pip3 install slither-analyzer), run slither . in your project directory, and read the output. It takes 5 minutes to set up and gives immediate results. From there, add Echidna for property testing and Mythril for deeper analysis.

Do these tools work with Vyper or other non-Solidity languages?

Slither is Solidity-only. Mythril works on EVM bytecode, so it can analyze any compiled contract regardless of source language. Echidna primarily targets Solidity but can test any EVM contract if you write the test harness in Solidity.

How many false positives should I expect?

From Slither: a lot. On a typical DeFi codebase, expect 30-50% of findings to be false positives or informational. Use --exclude-informational --exclude-low to focus on what matters. From Mythril: fewer, maybe 10-20%, because it generates concrete exploit paths. From Echidna: almost zero — if a property fails, something is genuinely wrong with your code or your property definition.

Can I use these tools on already-deployed contracts?

Slither needs source code (though you can pull verified source from Etherscan). Mythril can analyze on-chain bytecode directly: myth analyze --address 0x... --rpc infura. Echidna needs source code to run properties against.

Are there paid alternatives that are significantly better?

Certora Prover offers formal verification that's more powerful than any of these three tools for proving specific properties — but it requires writing formal specifications in CVL (Certora Verification Language), and the learning curve is steep. For most teams, the Slither + Mythril + Echidna stack covers 80-90% of what automated analysis can find. The remaining 10-20% is where formal verification and manual audits add value.

Your Next Step

If you're not running any of these tools, start with Slither today — it's free, it's fast, and it'll probably find something. If you're already running Slither, add Echidna and write properties for your critical invariants.

When you're ready for the layer that automated tools can't provide — adversarial manual review by auditors who've seen hundreds of codebases — that's what BugBlow does. Get a security assessment →

Protect Your Protocol Before It's Too Late

Smart contract exploits have caused over $4 billion in losses. Don't let your protocol be next.

Whether you're preparing for launch or already live — a professional security audit is the most important investment you can make.

👉 Request a Free Security Assessment