An attacker does not care how many tests your contracts pass. Tests check the inputs the developer imagined; the attacker's whole craft is finding the input nobody imagined. A test suite with full line coverage says that every line has been executed at least once under conditions the team chose. It says nothing about the path through those lines that empties the vault when a rounding error, a reentrant call and a particular token balance line up. Formal verification is the only technique that can say something about every path, which is why it keeps being proposed, and the only technique whose guarantee depends entirely on a document that most teams write badly, which is why it keeps disappointing.

The question is not whether formal verification works. It does, within its terms. The question is when its cost buys something that cheaper methods do not, and how to avoid the failure mode in which a team holds a proof that a property is true and loses funds because the property was the wrong one.

This article is for engineering leads deciding whether to spend on it and for auditors asked to recommend.

What it actually does

Formal verification establishes, by mathematical argument checked by a machine, that a model of the program satisfies a stated property for all inputs and all reachable states. Three words in that sentence carry the weight: model, stated, and reachable.

The model is not the program. It is a translation of the program into a logic the tool understands, and it is only as accurate as the translation. Verifying Solidity source means trusting the compiler; verifying bytecode avoids that but makes the specification harder to write.

The property is only what someone stated. A proof that a vault's total shares always equal the sum of user balances is a proof of exactly that and nothing more. If the vault can also be drained by a path that keeps that sum intact, the proof holds and the funds are gone.

Reachable states are those the tool's environment model allows. If the model assumes external calls return without side effects, reentrancy is unreachable by construction and will never be found. Every verification result should be read as: under these assumptions, about this model, this property holds. The assumptions are where auditors spend their time.

The spectrum of assurance

Verification is one end of a range of techniques, each buying more confidence at more cost. Choosing among them is the real decision.

  • Unit tests execute specific inputs and check specific outputs. Cheap, fast, essential, and blind to anything the author did not think of.
  • Property-based fuzzing generates many random or guided inputs and checks that stated properties hold after each sequence of calls. It finds inputs the author did not think of, and tools such as Foundry's invariant testing and Echidna make it a standard part of a Solidity workflow. It cannot prove absence; it can only fail to find.
  • Symbolic execution treats inputs as symbols rather than values and explores paths with a constraint solver, reaching branches that random inputs rarely hit. It is strong on arithmetic edge cases and weak where paths explode, such as loops and deep call chains.
  • Model checking exhaustively explores the state space of a bounded model, proving properties up to that bound. Useful for protocols whose interesting behaviour is a state machine with a small number of distinguishable states.
  • Full proofs establish a property for unbounded executions, either through a specialised prover for smart contracts or through an interactive theorem prover with a human guiding the argument. This is the strongest guarantee available and the most expensive to obtain and maintain.

Most teams should climb this ladder in order and stop before the top. Each rung is justified only when the one below has stopped finding bugs and the remaining risk warrants the step.

Where it earns its cost

Verification pays for itself in a narrow set of situations, and they share a shape: a small, stable core whose correctness everything else depends on, with properties that can be stated precisely.

Token and vault accounting is the clearest case. The claim that no sequence of deposits, withdrawals, transfers and fee accruals can create or destroy value, or let one user's balance exceed what they put in plus what they earned, is exactly the kind of property a prover can handle, and exactly the kind that fuzzing reaches only approximately.

Access control is another. A statement that a privileged function cannot be reached by any call path unless the caller holds a role, across every entry point including delegatecalls and fallbacks, is a closed question that a tool can answer definitively.

Arithmetic libraries and pricing curves benefit because a rounding edge that costs a little on every call compounds across millions of them. Bridges and anything with a large immutable deployment benefit because the code cannot be patched afterwards, so certainty before deployment is unusually valuable.

Verification earns less where the risk lives: in economic assumptions, oracle trust, governance and key custody. A perfectly verified lending protocol can still be drained by a manipulated price, because the prover accepted the oracle's output as truth. Those risks are covered by the items in our audit checklist and by threat modelling, not by proofs.

Invariants worth proving

The properties that have historically mattered fall into a few families, and a verification effort that covers them well is already most of the way to useful.

Solvency: the protocol can always meet its obligations. Total assets held are at least total claims against them, under every sequence of operations. For a lending market this becomes a statement about collateral, debt and the liquidation path; for a vault it is a statement about shares and underlying.

Conservation of value: operations move value but never create or destroy it, except through explicitly modelled minting, burning and fees. The sum of balances before an operation equals the sum after, adjusted only by the amounts the operation is defined to add or remove.

Access control: every state change that should be restricted is restricted on every path, and roles cannot be granted or escalated except through the intended mechanism.

Monotonicity and bounds: values that should only increase do so, caps are never exceeded, and a user cannot withdraw more than they deposited plus accrued yield.

Rounding direction: the protocol rounds in its own favour, so repeated small operations cannot accumulate into a drain. This one is often stated informally in audits and is far more convincing as a proof.

Each is worth stating even if only fuzzed, because writing it forces the team to say what the protocol promises.

The specification is the hard part, and the risk

Every verification engagement spends most of its time on the specification, and the specification is where verification fails.

A specification is a formal statement of intent, and intent lives in people's heads. A property can be too weak, holding trivially because it omits the case that matters; a conservation property that ignores fees will pass on a contract whose fee logic drains users. It can be too strong, failing on intended behaviour, and the temptation is to weaken it until it passes rather than ask why it failed. And it can differ subtly from the intent in a way nobody notices, because reading formal specifications is harder than writing them.

The gap between specification and intent is the risk. A team that holds a proof tends to stop looking, and a proof about the wrong property is more dangerous than no proof, because it converts uncertainty into misplaced confidence. The mitigations are procedural: the specification is written by someone other than the contract author, reviewed by an auditor who has done a manual review of the same code, and tested by deliberately introducing bugs to confirm the properties catch them. A property that passes on the buggy version is not a property; it is a comment.

Environment assumptions belong in the specification and should be written out. What external calls can do, what tokens are allowed to do, whether the prover models reentrancy, and what the tool's loop and call-depth bounds are all define what the proof covers. Our reports restate them in plain language, because a proof read without its assumptions is read wrongly.

When fuzzing gives most of the value

For a majority of protocols, a well-built invariant fuzzing suite delivers most of what verification would, at a fraction of the cost and with the advantage that it runs on every commit.

The same invariants can be written as fuzz properties in the project's existing test framework. A fuzzer running for hours will find most of the arithmetic edges, sequencing bugs and accounting drift that a prover would. What it cannot do is show that nothing remains, and for most protocols that residual uncertainty is acceptable relative to the economic and operational risks beside it.

The signs that fuzzing has stopped being enough are specific: the fuzzer has run long campaigns without a finding while the team still has low confidence in a core invariant; the state space has structure that random exploration rarely reaches, such as a precise sequence of ten calls; or the code is immutable and high-value enough that a residual risk of any size is unacceptable. At that point verification is the next step, and the fuzz properties become the first draft of the specification.

Cost and timeline realities

A meaningful verification effort for a protocol's core, covering a handful of properties over the central contracts, takes weeks of specialist time, not days, and the elapsed time is usually longer because the specification needs the protocol team's attention at several points. The cost scales with the number of properties, the complexity of the code under proof, and above all with how much of the surrounding system must be modelled for the proof to go through.

The ongoing cost is what teams underestimate. A specification is coupled to the code; every material change requires re-running the proofs and often rewriting parts of the specification. Verification suits code that will not change, and punishes code that will. A protocol in active development can keep a verification suite only if the team commits to maintaining it as part of the engineering process, which means engineers who can read the specification language.

Tool limitations add time. Loops need manual bounds, external calls need summaries, and some constructs must be refactored or excluded. Expect part of the work to be reshaping the code into something the prover can reason about, and treat that as a benefit; code that is hard to verify is usually hard to review.

Verifying the deployed bytecode versus the source

Most verification works on source, or on an intermediate representation close to it, and trusts the compiler to preserve meaning. The compiler is a large, actively developed program with its own history of bugs, and optimiser settings change the generated code. A proof about the source is a proof about what the compiler should have produced.

Verifying the deployed bytecode closes that gap: the proof is about the exact code that executes. It is harder, because the specification must be stated in terms of storage slots and stack behaviour rather than named variables, and the tooling is less mature. It is worth doing for the highest-value immutable components, and worth approximating everywhere by confirming that the deployed bytecode matches a reproducible build of the verified source at the same compiler version and settings. A verified source that does not correspond to the chain is a verified document.

Use it as one layer

Verification works best as one layer among several, and we treat it that way on engagements.

Manual review comes first, because it is where intent is discovered. Our auditors read the code, build the threat model, and write down what the protocol promises; the invariants that fall out of that process are the candidates for formal treatment. A property written before anyone has understood the code is a guess.

Fuzzing follows, encoding those invariants as properties in the project's test framework so that they are checked continuously. Most findings arrive at this stage, and the fuzz suite stays with the team after we leave.

Verification is applied selectively to the properties that survive: the ones where fuzzing has found nothing, the stakes justify certainty, and the code is stable enough to make the proof durable. We write or review the specification independently of the contract author, mutate the code to confirm the properties detect known bugs, and restate the assumptions in the report. Where we do not recommend verification, we say so and explain what covers the gap instead.

The result is not a certificate. It is a set of statements about what has been proven, what has been fuzzed, what has been reviewed by hand, and what remains an assumption.

Practical next steps

  • Write down the invariants your protocol promises, in plain language, before choosing any tool.
  • Encode them as fuzz properties in your existing framework and run long campaigns; most teams should start and often stop here.
  • Verify selectively: stable, high-value core logic with properties that can be stated precisely, and accept that economic and operational risks need other methods.
  • Have the specification written and reviewed by people who did not write the code, and confirm it catches deliberately introduced bugs.
  • Tie proofs to the deployed bytecode, at least by reproducible build, and budget for maintaining the specification as the code changes.

Our verification and fuzzing scope is described on the services page, and you can reach the team on Telegram.