Two Reviewers Walk Into the Same Codebase
You've just deployed an 800-line Solidity vault contract. Two firms are sitting in your inbox, both quoting serious money, both using the word "review." The first will spend three weeks reading the code, running Slither and Echidna, probing edge cases, and handing you a tiered finding report. The second will spend six weeks building a mathematical model of every state your contract can possibly enter, then asking a theorem prover to check whether any of those states breaks the rules.
Same codebase. Very different guarantees.
That distinction is not a marketing quibble. It changes what you actually know when the work is done.
What a Standard Security Audit Actually Does
A smart contract audit is expert code review, sharpened with tooling. Auditors read the logic manually, run static analyzers like Slither or Mythril, throw semi-random inputs at the contract with fuzzers like Echidna, and check the code against a taxonomy of known vulnerability classes: reentrancy, integer overflow, access-control mistakes, oracle manipulation, flash-loan attack surfaces.
The output is a tiered finding list. Critical, high, medium, informational.
But notice what the whole process depends on: the auditor's imagination. They test the paths they think to test. They pattern-match against vulnerabilities they have seen before. A novel attack vector, or a subtle interaction between two functions that looks harmless in isolation, can slip past. Not because the auditors are careless. Because the search space of all possible inputs and call sequences is, to put it plainly, enormous, and sampling it, however cleverly, is still sampling.
That is not a flaw in auditing. It is the honest limit of the method, and any firm that pretends otherwise is selling you something.
What Formal Verification Actually Proves
Formal verification starts somewhere different. Instead of asking "can we find a bug?", it asks whether we can prove no bug exists, relative to a specification.
Three steps. Order matters.
First, you write a formal specification: a precise, mathematical description of what the contract is supposed to do. Not prose like "users can't withdraw more than they deposited" but a logical predicate that holds over every reachable state. Ambiguous requirements, written in English, have to be translated into something a proof system can reason about. This step is harder than most teams expect.
Second, you encode the contract's behavior as a formal model. Tools like the Certora Prover work directly on EVM bytecode or Solidity; others like the K framework or Coq require more manual translation. The model captures every function, every storage variable, every branch.
Third, the prover attempts to verify that the model satisfies the specification across all possible inputs and all possible execution paths. Not a sample. All of them. If it succeeds, you have a proof. If it finds a counterexample, you get a concrete failing case, often one a human would never have constructed.
Consider a simple invariant: the total supply of a token must always equal the sum of all balances. A fuzzer might run ten million random calls and never trip this. A formal prover will either prove it holds for every sequence of calls an attacker could construct, or hand you the exact sequence that breaks it. It is, to borrow an image from structural engineering, the difference between stress-testing a bridge by driving trucks over it and solving the load equations from first principles.
That is a qualitatively different kind of guarantee.
A Concrete Scenario
Two DeFi protocols, call them Arbor and Finch, deploy lending contracts with identical core logic. Arbor commissions a four-week audit from a well-regarded firm. Finch runs the same audit and adds a formal verification engagement focused on two properties: solvency (the protocol can never owe more than it holds) and no unauthorized minting.
The audit on both surfaces and fixes three medium-severity issues. Standard result.
The formal verification on Finch, during the specification-writing phase, finds something else entirely. The spec reveals that the liquidation function carries an implicit assumption about price-feed ordering, an assumption the English-language design document never stated. The prover could not verify solvency until the assumption was made explicit, which forced the team to confront it. They patched it before deployment.
Arbor's auditors never tested that assumption because nothing in the code obviously flagged it. Not negligence on their part. The assumption was simply invisible until someone tried to state it with logical precision.
Finch paid roughly 2.5 times more and took six additional weeks. Whether that premium is rational depends entirely on how much value the contract holds and how catastrophic a failure would be.
The Honest Limits of Formal Verification
Formal verification is not a silver bullet, and the industry's occasional tendency to market it as one deserves some skepticism.
The proof is only as strong as the specification. If the spec is wrong, incomplete, or misses a property the attacker actually exploits, the proof is useless on that dimension. Specifications are written by humans carrying the same blind spots as auditors. A protocol verified against a solvency property that fails to account for a specific oracle manipulation path remains vulnerable to that path, full stop.
Verification also says nothing about the deployment environment. The contract may be proven correct in isolation and still behave unexpectedly when composed with another protocol it was never modeled against. Most formal verification work treats the contract as a closed system, which is a meaningful limitation in a composable ecosystem.
The tooling has limits too. The Certora Prover and comparable tools handle most EVM patterns well, but highly complex or unusual bytecode can exceed the prover's capacity, yielding inconclusive results rather than proofs.
Audits, for their part, remain better at catching implementation-level sloppiness, library misuse, and issues that don't resolve into clean formal properties. The two methods are genuinely complementary. Framing them as competitors misunderstands both.
When Each Approach Earns Its Cost
A standard audit is the correct baseline for almost any contract that will hold meaningful value. The tooling is mature, the firms are numerous, turnaround is faster, and cost is proportionate for contracts in the low-to-mid value range.
Formal verification earns its premium under a specific set of conditions: the contract holds very large amounts, the properties being protected are precisely definable (token invariants, access controls, arithmetic bounds), and a single exploit would be existential. Core protocol logic, bridges, and token contracts with complex minting rules are the natural candidates. Peripheral UI contracts or simple proxy wrappers are generally not.
So here is the real question worth sitting with: can you write down, unambiguously, what "correct" means for your contract? If you can state your invariants with logical precision, a prover can check them against every possible execution. If you cannot write them down, you have a specification problem that no volume of testing will resolve anyway, and that problem will follow your contract onto mainnet.
The extra six weeks stops feeling like overhead the moment the value locked crosses the threshold where a single exploit ends the protocol. At that point, a proof isn't a luxury. It's the only intellectually honest answer to the question of whether the thing is safe.