On this page
Ask whether formal verification or fuzzing is better for smart contracts and you will get a partisan answer from whichever camp you asked. The question is badly posed. The two techniques answer different questions, and each has a blind spot that happens to be roughly the other’s strength. What follows is a comparison that tries to be specific about what each one is actually doing when it runs, because that is what determines what it can find.
What each technique is claiming
A formal verification run takes a property, a statement about the contract that should always hold, and attempts to prove that no execution violates it. “The sum of balances equals total supply.” “Only the owner can call upgradeTo.” “This function never reverts on a valid input.” If the proof goes through, the property holds for every input and every state, not just the ones anyone tried. If it does not, the prover usually produces a counterexample: a concrete input that violates the property.
A fuzzing run takes the contract and throws inputs at it, guided by feedback about which code the inputs reached, looking for a crash, a revert that should not happen, a failed assertion, or a violated invariant. It never proves anything. What it produces is a stream of concrete executions, and if one of them breaks an invariant, that execution is a reproducible bug with the exact input attached.
The asymmetry is the whole story. Verification is universal but conditional on the property being the right one. Fuzzing is unconditional but only ever covers the inputs it happened to generate.
Where verification fails
The property is wrong or incomplete. A prover checks what you asked. If you asked “the owner check is present on upgradeTo” and the bug is that initialize can be called twice to change the owner, the proof goes through and the contract is still broken. Every verified contract that has been exploited was exploited through a property nobody wrote down. This is not a weakness of the tool; it is the definition of the tool. But it means the value of verification is bounded by the quality of the specification, and specifications are written by the same people who wrote the bug.
The model is not the chain. Verification works over a model of the EVM, and the model has to make choices about external calls, gas, block state and precompiles. A proof that holds when external calls are modelled as returning arbitrary values may not hold when a specific external contract can re-enter. Most tools handle reentrancy now; the point is that every modelling simplification is a place where the proof and the deployed contract can disagree.
It does not scale past the boundary. Proving a property of one contract is tractable. Proving a property of a protocol that spans six contracts, a price oracle, and a token whose transfer has a fee is usually not, and the practical response is to verify components in isolation with assumptions about the others. Those assumptions are, again, properties nobody proved.
Timeouts are not answers. For a hard property the solver may neither prove nor refute it in the time available. A timed-out proof is not evidence of safety, and it is easy to treat it as such when the alternative is another day of waiting.
Where fuzzing fails
It only sees what it reaches. A bug behind a specific 32-byte value, a specific storage state that takes a sequence of ten calls to set up, or a comparison against a hash will not be found by random or coverage-guided mutation in any practical time. Structured-input generation and dictionaries help; symbolic-assisted fuzzing helps more; but the fundamental limit is that the input space is astronomically larger than any run.
It needs an oracle. A fuzzer finds inputs that break an assertion or an invariant. If the bug does not break any assertion you wrote, the fuzzer runs through it and reports nothing. “Funds can be drained” is not an assertion until someone writes assert(vault.totalAssets() >= sumOfDeposits()), and writing that assertion is the same specification problem verification has, in a weaker form.
Sequences are hard. Most valuable smart-contract bugs need several calls in a particular order with particular state in between. Stateful fuzzers exist and are good, but the space of call sequences grows exponentially with length, and coverage feedback on sequence structure is much weaker than on branch structure.
Silence is ambiguous. A fuzzer that runs for an hour and finds nothing has told you that it found nothing in an hour. It has not told you the contract is safe, and the difference between “explored the relevant space” and “got stuck in the easy branches” is invisible from the outside without coverage reports, which most people do not read.
Where they meet
The pairing that works in practice uses each one to feed the other.
A failed proof produces a counterexample, and the counterexample is a concrete input. Hand it to a fuzzer as a seed and the fuzzer explores the neighbourhood of a known-interesting state rather than starting from zero. Conversely, a fuzzer’s coverage map tells you which branches it could not reach, and those branches are the ones worth writing a property for, because whatever guards them is exactly the kind of specific condition fuzzing is bad at and solving is good at.
Symbolic execution sits between the two and is often what people mean by “verification” in the smart-contract context. It explores paths with symbolic inputs and asks a solver for concrete values that reach each branch. It has the solver’s power to find specific values and the fuzzer’s habit of producing concrete executions, at the cost of path explosion on loops and external calls. Concolic execution, which alternates concrete runs with symbolic solving at the branches the concrete run did not take, is the practical compromise most modern tooling uses, including the fuzzers in this platform.
Static analysis, the third technique that usually gets left out of this argument, does something neither of the others does: it finds classes of bug without a specification or an input. A reentrancy detector does not need to be told the invariant that reentrancy breaks; it looks for the call-before-state-update shape. The cost is that it reasons about shape rather than behaviour, and shape-based reasoning has false positives that behaviour-based reasoning does not. Each of the three has one thing the others lack: verification has universality, fuzzing has concreteness, static analysis has specification-free coverage.
What this means for choosing
If you have a precise invariant and a contract small enough to model, prove it. Nothing else gives you the universal claim.
If you have a large system and no complete specification, which is nearly every real protocol, fuzz it with the strongest invariants you can write, and treat every branch the fuzzer cannot reach as a question.
Run static analysis regardless, because it costs nothing and it is the only one of the three that looks for bugs you did not think to look for.
And whichever you use, be honest about the claim. A proof is a claim about a property. A fuzzing campaign is a claim about a set of inputs. Neither is a claim that the contract is safe, and the incidents in which a “verified” or “extensively fuzzed” contract was drained are, almost without exception, incidents in which someone forgot which claim they were holding.