Static Analysis vs Fuzzing vs Formal Verification: What Each Finds

Smart contract security is not a solved problem. Billions in value flow through code that is immutable the moment it is deployed, making the cost of a missed vulnerability catastrophic and irreversible. Three classes of automated technique have emerged as the professional standard for comprehensive pre-deployment analysis: static analysis, dynamic analysis through fuzzing, and formal verification. Each operates on a different model of what “testing” means, each has a distinct vulnerability space it covers well, and each has blind spots the others compensate for. Understanding the boundaries of each technique—and knowing how to combine them—is the core competency that separates a thorough security review from a superficial one.

---

1. Static Analysis

How It Works

Static analysis evaluates the properties of a program without executing it. It operates on source code or an intermediate representation, building models of data flow and control flow, then checking those models against a library of known bug patterns. For Solidity, this means parsing the abstract syntax tree (AST), constructing call graphs, and propagating type and value constraints across the entire codebase in a single pass.

Slither, developed by Trail of Bits, is the dominant tool in this category. It compiles Solidity source into its own intermediate representation called SlithIR, then runs a suite of built-in detectors—over 90 of them—against the IR. Because it works on source code rather than bytecode, it can surface variable names, NatSpec comments, and inheritance hierarchies to give precise, human-readable findings. Slither is fast: a scan of a mid-sized codebase typically completes in seconds.

# Install
pip install slither-analyzer

# Run against a Foundry project
slither . --checklist --markdown-root https://github.com/myprotocol/contracts/blob/main/

Slither can output findings in Markdown, JSON, or a GitHub-style checklist, making it straightforward to embed in CI pipelines.

What Static Analysis Finds

Static analysis excels at identifying structural and syntactic vulnerability patterns:

• Reentrancy — checks-effects-interactions violations where an external call precedes a state update
• Unprotected function calls — public or external functions lacking access control modifiers
• Integer overflow/underflow — arithmetic operations on uint values without overflow guards (relevant on pre-0.8.x Solidity)
• Uninitialized storage variables — pointers that alias storage slot zero
• Dangerous delegatecall — patterns that allow callers to overwrite proxy implementation logic
• Incorrect inheritance — shadowed functions, missing override keywords, or incorrect linearization order
• Unused return values — calls to transfer-family functions whose return values are silently ignored
• Code quality smells — expensive operations in loops, constant state variables declared as storage

// Slither will flag: reentrancy-eth
// The external call happens BEFORE the balance update

contract Vulnerable {
    mapping(address => uint256) public balances;

    function withdraw() external {
        uint256 amount = balances[msg.sender];
        // ❌ external call before state change
        (bool ok, ) = msg.sender.call{value: amount}("");
        require(ok, "transfer failed");
        balances[msg.sender] = 0; // state update is too late
    }
}

Running slither . on this contract immediately flags a high-severity reentrancy finding with the precise line number and a recommended fix.

What Static Analysis Does Not Find

Static analysis is pattern-matching against a known catalogue. It cannot:

• Discover novel logic errors — if a bug doesn’t match a detector rule, it is invisible to the tool
• Model runtime state — it cannot reason about the concrete values stored in contract storage across multiple transactions
• Reason about multi-contract interactions — flash-loan attack surfaces that span three or four protocols in a single transaction are beyond its model
• Validate business logic — a liquidation threshold of 75% vs. 80% is semantically different, but both are valid syntax
• Eliminate false positives — because it never executes the code, Slither can flag issues that are unreachable in practice, generating noise that requires human triage

Static analysis is best understood as a fast, exhaustive scan of known vulnerability patterns. It finds the same class of issues a checklist-based manual review would find, but faster and at consistent quality.

---

2. Dynamic Analysis: Fuzzing

How It Works

Fuzzing executes the contract against many generated inputs and checks whether any input violates a user-specified invariant. Unlike unit tests, which verify behavior for a predetermined set of inputs, fuzz tests run for hundreds of thousands or millions of iterations, each time generating a new, potentially surprising input. The key insight is that the developer defines what must always be true; the fuzzer finds inputs that make it false.

This style—where the developer writes invariants rather than test cases—is called property-based testing and it is the model adopted by both major Solidity fuzzers.

Echidna, also from Trail of Bits, is the reference implementation of property-based fuzzing for Solidity. It is written in Haskell and uses grammar-based fuzzing campaigns derived from the contract’s ABI, which allows it to generate inputs that are type-valid but semantically unexpected. Echidna also integrates with Slither to extract useful information before the campaign begins, and provides detailed coverage reports to identify which lines remain untested.

Foundry’s forge test with the vm.assume and bound cheatcodes provides a stateless fuzzer built directly into the most popular Solidity development framework. For stateless properties—those that hold over a single function call—Foundry fuzzing has near-zero setup cost: prefix any test function with testFuzz_ and pass arguments to trigger randomized input generation.

// Foundry stateless fuzz test
// forge test will run this with thousands of random `amount` values

contract TokenFuzzTest is Test {
    MyToken token;

    function setUp() public {
        token = new MyToken(1_000_000e18);
    }

    function testFuzz_transferNeverMintsTokens(
        address from,
        address to,
        uint256 amount
    ) public {
        vm.assume(from != address(0) && to != address(0));
        vm.assume(from != to);
        uint256 totalBefore = token.totalSupply();
        deal(address(token), from, amount);

        vm.prank(from);
        token.transfer(to, amount);

        assertEq(token.totalSupply(), totalBefore, "supply changed");
    }
}

For stateful invariant testing—where the invariant must hold across arbitrary sequences of transactions—Foundry’s invariant_* test pattern and Echidna’s sequential mode both model multi-step attack scenarios. This is where fuzzing earns its place: real exploits are almost never single-transaction affairs.

// Echidna property for a lending protocol
// echidna . --contract LendingFuzz --config echidna.yaml

contract LendingFuzz is LendingProtocol {

    // This function is called by Echidna as an invariant.
    // If it ever returns false, Echidna found a bug.
    function echidna_solvency() public view returns (bool) {
        // Total collateral value must always exceed total debt
        return totalCollateralValue() >= totalDebtValue();
    }

    function echidna_no_free_borrow() public view returns (bool) {
        // No address can have debt without any collateral
        for (uint i = 0; i < users.length; i++) {
            if (debtOf(users[i]) > 0 && collateralOf(users[i]) == 0) {
                return false;
            }
        }
        return true;
    }
}

What Fuzzing Finds

• Unexpected state transitions — sequences of valid calls that leave the contract in an inconsistent state
• Arithmetic edge cases — overflow, underflow, division-by-zero, and precision loss under extreme but valid inputs
• Complex multi-transaction bugs — scenarios that require a specific ordering of several calls to trigger
• Invariant violations in DeFi math — accounting mismatches in vaults, AMMs, or lending markets that only manifest at extreme price ratios
• Missing bounds on parameters — functions that behave correctly for typical inputs but break at type(uint256).max

What Fuzzing Does Not Find

Fuzzing is probabilistic, not exhaustive. Its guarantees are statistical, not mathematical:

• It cannot prove the absence of a bug — a fuzzer that runs for 48 hours without finding a violation provides strong but not absolute confidence
• It is bounded by coverage — if the fuzzer never reaches a code path, it cannot find bugs there; coverage-guided fuzzers help but do not guarantee full coverage
• It requires well-specified invariants — a fuzzer without a meaningful property to falsify is just an expensive no-op; the quality of the test suite is directly proportional to the quality of the invariants written
• It struggles with oracle dependencies — properties that depend on external price feeds or off-chain state require careful mock setup

---

3. Formal Verification

How It Works

Formal verification uses mathematical proof to establish that a property holds for all possible inputs and all possible contract states—not just the ones a fuzzer happened to try. Rather than sampling the input space, it encodes the entire input space as symbolic constraints and delegates the proof obligation to a solver.

The two main tools in this category take different approaches to the same underlying idea.

Halmos, developed by a16z, is a symbolic bounded model checker that integrates directly into the Foundry testing workflow. Test functions prefixed with check_ are executed symbolically: every argument becomes an unconstrained symbolic variable, and the tool explores all execution paths simultaneously, looking for any assignment of values that triggers an assert violation. Halmos requires no separate specification language—it reuses Foundry test syntax—making adoption very low-friction for teams already using Forge.

// Halmos symbolic test — prefix with check_ instead of test_
// halmos --match-test check_

contract VaultSymTest is SymTest, Test {
    Vault vault;

    function setUp() public {
        vault = new Vault();
    }

    // Halmos will attempt to find any symbolic `amount` that breaks this
    function check_depositWithdrawRoundtrip(uint256 amount) public {
        vm.assume(amount > 0 && amount <= 1e30);
        address alice = address(0xA11CE);
        deal(address(this), amount);

        vault.deposit{value: amount}();
        uint256 shares = vault.sharesOf(alice);

        vault.withdraw(shares);
        uint256 received = alice.balance;

        // For all symbolic amounts: you get back at least what you put in
        assert(received >= amount);
    }
}

Certora Prover is a more powerful but more demanding tool. It uses its own specification language, CVL (Certora Verification Language), to express properties that span the entire contract lifecycle. Rules and invariants written in CVL are compiled together with the contract bytecode into a verification condition—a logical formula—which is then discharged by an SMT solver. If the solver finds a satisfying assignment that violates the property, it returns a concrete counterexample. If no such assignment exists, the property is proven.

// CVL specification for an ERC-20 token
// File: token.spec

// Invariant: sum of all balances must equal totalSupply
invariant totalSupplyIsSum()
    totalSupply() == sumBalances
    {
        preserved transfer(address to, uint256 amount) with (env e) {
            requireInvariant totalSupplyIsSum();
        }
    }

// Rule: transferFrom must decrease allowance
rule transferFromDecreasesAllowance(
    env e,
    address sender,
    address recipient,
    uint256 amount
) {
    uint256 allowanceBefore = allowance(e.msg.sender, sender);
    transferFrom(e, sender, recipient, amount);
    uint256 allowanceAfter = allowance(e.msg.sender, sender);
    assert allowanceAfter == allowanceBefore - amount,
        "allowance not properly decremented";
}

What Formal Verification Finds

• Properties that hold for all inputs, not just sampled ones — particularly valuable for arithmetic properties where the bug is at an extreme boundary
• Deep invariant violations — properties over the entire state space, including reachability conditions that require long call chains
• Proven absence of vulnerability classes — once a rule is verified, you have a certificate, not just a test result
• Counterexamples with exact witness values — when a proof fails, the solver emits the precise transaction sequence and parameter values that trigger the violation

What Formal Verification Does Not Find

Formal verification is only as good as its specification:

• Unspecified properties — the prover only checks what you ask it to check; if you do not write a rule for reentrancy, reentrancy is not checked
• Business logic correctness — the prover cannot determine whether your liquidation formula is economically sound; it can only prove that the formula is computed consistently
• Scalability limits — large, complex contracts with deep call graphs and unbounded loops can cause the underlying SMT solver to time out; the Certora Prover handles loops by unrolling them a configurable number of times, which can hide bugs if the loop bound is set too low
• External contract behavior — the prover models external calls as unconstrained by default; proving cross-protocol properties requires careful harness design
• Spec bugs — a specification that does not capture the intended property produces a green result for a contract that still has bugs

---

4. How the Three Techniques Complement Each Other

No single technique dominates. Each has strengths that directly compensate for the weaknesses of the others:

Dimension	Static Analysis	Fuzzing	Formal Verification
Speed	Seconds	Minutes–Hours	Hours–Days
Coverage model	Pattern-matching	Statistical sampling	Exhaustive (bounded)
False positives	Medium–High	Low	Low (proof) / Medium (spec errors)
False negatives	High (no novel bugs)	Medium (probabilistic)	Low (within spec scope)
Setup cost	Minutes	Hours–Days	Days–Weeks
Bug classes	Known patterns	Edge-case state	Proven invariants
Output	Findings list	Counterexample trace	Proof / Counterexample

The relationship is also sequential in practice. Static analysis results inform fuzzing—Echidna already uses Slither under the hood to seed its analysis with type information and control-flow data. Fuzzer-discovered invariant violations, in turn, inform the formal verification specification: if a fuzzer breaks totalAssets >= totalDebt after a sequence of five transactions, the Certora engineer knows exactly which invariant to prove and which function transitions to constrain.

Fuzzing catches bugs. Formal verification proves their absence. Static analysis accelerates the discovery of low-hanging fruit so that human time is spent on harder problems.

---

5. Cost and Time Investment

Understanding the resource profile of each technique is essential for planning a security budget.

Static Analysis

• Setup time: Minutes. pip install slither-analyzer && slither .
• Run time: Seconds to low minutes for any codebase of realistic size
• Expertise required: Low. Findings are self-explanatory; triage requires Solidity familiarity but not deep security research skills
• Ongoing cost: Near-zero if embedded in CI/CD. Slither is open-source and free
• ROI: Very high. Catches a large class of known vulnerabilities essentially for free, letting human reviewers focus on logic

Fuzzing

• Setup time: Hours to days, depending on invariant complexity. Writing good invariants for a complex protocol is a skilled task
• Run time: Meaningful campaigns run for hours; large-scale parallel campaigns with echidna-parade can run continuously over days
• Expertise required: Medium-High. Writing invariants that actually cover the important protocol properties requires deep protocol understanding
• Hardware cost: CPU-intensive; cloud instances are typically used for long campaigns
• ROI: High. The property-writing exercise alone forces clarity about what the protocol must guarantee, independently of whether the fuzzer finds a bug

Formal Verification

• Setup time: Days to weeks. Writing CVL specifications for a non-trivial DeFi protocol is a specialized skill; learning the Certora Prover’s toolchain and its interaction with SMT solvers takes time
• Run time: Hours per verification job; iterating on a spec through multiple solve-debug-refine cycles can span days
• Expertise required: High. Effective use of Certora Prover or even Halmos for complex properties requires familiarity with logical reasoning, SMT constraints, and the tool’s own abstraction model
• Financial cost: Certora Prover is a commercial product; access to the cloud prover for production-scale verification involves a significant cost. Halmos is open-source and free, but covers a narrower property class
• ROI: Extremely high for critical protocol components. A formally verified solvency invariant on a lending protocol with $500M TVL costs a fraction of one exploit

---

6. Matching Technique to Protocol Type

Not every protocol warrants the same security investment. The appropriate technique mix varies with protocol complexity, TVL, and the nature of the invariants worth proving.

Minimal ERC-20 / ERC-721 Tokens

Recommended: Static analysis + light fuzzing

A simple token with a standard implementation has a small, well-understood state space. Slither catches the typical pitfalls (missing access control on mint, unchecked return values). A few Foundry fuzz tests asserting totalSupply consistency and allowance correctness are sufficient for most cases. Formal verification is overkill unless the token has unusual minting logic.

AMMs and Liquidity Protocols

Recommended: Static analysis + heavy fuzzing + targeted formal verification

AMMs have complex pricing invariants (the AMM invariant x * y = k or variants thereof) that are ideal fuzzing targets. The protocol must hold that invariant across all swap, add-liquidity, and remove-liquidity transactions. Property-based fuzzing with Echidna is the right tool for this—write the invariant, let the fuzzer run for 48+ hours, and examine every violation. For the core swap function—the highest-value attack surface—a Halmos or Certora proof that the pool invariant is maintained after every operation adds meaningful additional assurance.

// Invariant for a constant-product AMM
function echidna_invariant_xy_k() public view returns (bool) {
    uint256 x = reserveA;
    uint256 y = reserveB;
    uint256 k = constantProduct;
    // Allow for rounding: invariant must not decrease
    return x * y >= k;
}

Lending and Borrowing Protocols

Recommended: Static analysis + heavy stateful fuzzing + comprehensive formal verification

Lending protocols have the most complex invariant surfaces of any DeFi primitive: per-user solvency, global solvency, liquidation correctness, interest accrual accuracy, and oracle boundary conditions. Multi-step attack scenarios—where a sequence of deposit, borrow, price-manipulation, and liquidation calls violates solvency—are exactly what stateful Echidna campaigns are built for. For protocols above a meaningful TVL threshold, formal verification of core solvency properties is not optional—it is the responsible standard of care.

Governance and Upgrade Contracts

Recommended: Static analysis + formal verification

Governance contracts have a small set of very high-stakes properties: the admin address cannot change without a timelocked proposal, proposal execution cannot happen before the voting window closes, quorum cannot be manipulated. These properties are crisp, boolean, and amenable to formal proof. Fuzzing adds less value here because the bug is typically a logical property of the state machine, not a numerical edge case. Static analysis catches the structural issues; formal verification proves the governance invariants.

Bridges and Cross-Chain Protocols

Recommended: All three, with emphasis on formal verification of message-validation logic

Bridges are the highest-value attack surface in the ecosystem. The core invariant—that tokens locked on chain A precisely correspond to tokens minted on chain B—must hold under arbitrary message ordering, replay attempts, and byzantine relayer behavior. Static analysis finds the basic patterns; fuzzing explores the message-validation state space; formal verification is the only tool that can provide a proof-level guarantee about the absence of double-spend paths.

---

7. Integrating All Three in a Professional Audit

A professional security engagement does not run these techniques in isolation. It structures them as a layered pipeline where each phase informs and amplifies the next.

Phase 1 — Static Analysis Triage (Day 1)

The audit opens with a full Slither scan. The output is triaged: automated findings are classified as confirmed, false positive, or needs-manual-review. This takes a few hours and serves two purposes: it closes out the known-pattern vulnerability space, and it gives auditors a structural map of the codebase—inheritance hierarchies, external calls, storage layout—before they read a single line of business logic.

# Full audit-mode Slither run with JSON output for triage
slither . \
  --json slither-findings.json \
  --checklist \
  --print human-summary \
  --print contract-summary

Phase 2 — Manual Review and Invariant Extraction (Days 2–5)

Human auditors review business logic, economic design, and access-control architecture. This is also the phase where the invariant list is built: every protocol guarantee that must hold (“the total shares outstanding never exceed the deposited assets”, “a user cannot withdraw more than they deposited”) is written down explicitly. This list becomes the fuzzing specification and, for critical properties, the formal verification target.

Phase 3 — Fuzzing Campaign (Days 3–7, parallel)

While manual review continues, the fuzzing campaign runs in parallel. The invariants extracted in Phase 2 are coded as Echidna properties or Foundry invariant_* functions. Coverage is monitored and the harness is extended to reach uncovered branches. The fuzzer runs on cloud infrastructure overnight; findings from overnight runs are triaged in the morning.

// Foundry invariant test launched in parallel with manual review
contract ProtocolInvariantTest is StdInvariant, Test {
    Protocol protocol;
    Handler handler;

    function setUp() public {
        protocol = new Protocol();
        handler = new Handler(protocol);
        // Tell Foundry to only call handler functions
        targetContract(address(handler));
    }

    function invariant_globalSolvency() public view {
        assertGe(
            protocol.totalAssets(),
            protocol.totalLiabilities(),
            "protocol insolvent"
        );
    }
}

Phase 4 — Formal Verification of Critical Properties (Days 5–10)

For properties that the fuzzer could not definitively confirm or disprove—or for properties where the protocol’s TVL justifies a mathematical proof—formal verification is applied. Halmos is used first because the overhead of writing a check_ test from an existing testFuzz_ test is minimal. For properties that require CVL invariants (covering all state-changing functions in a single rule), the Certora Prover is engaged.

The deliverable here is not just a pass/fail result but a proof artifact. A formal proof that totalSupply() == sum(balances) holds for all addresses across all ERC-20 operations is a transferable, auditable artifact that end users and protocol governance can reference.

Phase 5 — Synthesis and Report

The audit report combines:

1. Static analysis findings — triaged Slither output, severity-rated and annotated with reachability assessment
2. Fuzzing counterexamples — any invariant violation found, with the minimized transaction sequence that reproduces it
3. Formal verification results — a list of properties that were proven, and any properties where verification failed or timed out (the latter is itself a finding: if a property cannot be proven, the protocol team should understand why)
4. Manual review findings — logic errors, economic design issues, and access-control gaps that no automated tool surfaced

This layered approach ensures that the easy patterns are caught cheaply, the unexpected state transitions are explored systematically, and the critical invariants are either proven or explicitly identified as unproven.

---

8. The Limits of Automation

All three techniques operate on a closed-world assumption: they analyze what the code does, not whether what the code does is correct. A liquidation function that correctly implements an economically unsound formula will pass every automated check. A governance mechanism that is formally verified to execute proposals correctly can still be exploited by a well-capitalized adversary who accumulates enough voting tokens.

Automated tools are force multipliers for human intelligence, not replacements for it. Static analysis gives auditors a structural map. Fuzzing generates adversarial scenarios that human imagination might miss. Formal verification provides certainty within a precisely stated scope. The human auditor synthesizes all three and asks the question that no tool can ask: is this the contract the protocol intends to deploy, and does the protocol’s economic design achieve what its users believe it achieves?

The right security posture is not to pick the most impressive-sounding technique and apply it in isolation. It is to understand what each technique finds, run all three, and treat any gap between them as a signal that more thought is needed.

---

Summary

Technique	Primary Tool(s)	Best For	Cannot Find
Static analysis	Slither	Known patterns, code quality, access control	Novel logic, runtime state, business logic
Fuzzing	Echidna, Foundry	Edge cases, multi-step exploits, invariant violations	Proven absence, unspecified invariants
Formal verification	Halmos, Certora	Proven invariants, arithmetic soundness	Unspecified properties, economic design flaws

The coverage question is not "which tool should I use?" It is "what parts of my vulnerability space remain unexplored?" Static analysis closes the known-pattern space in minutes. Fuzzing explores the reachable state space over hours. Formal verification proves invariants for all inputs, forever. Run in sequence, they leave progressively fewer places for a vulnerability to hide.