Certora Formal Verification vs Manual Audit: Need Both?

Certora's prover can tell you, with mathematical certainty, that a lending contract's total borrowed amount never exceeds total collateral under every possible sequence of calls. No fuzzer, no human reviewer reading line by line, can make that same guarantee — they can only fail to find a counterexample. That distinction is the whole reason formal verification exists as a separate discipline from auditing, and it's also why teams keep asking whether one replaces the other. It doesn't. They check different things, and for anything holding real value, skipping either one leaves a gap the other was built to close.

What Certora actually proves

Certora Prover works against a specification you write in CVL (Certora Verification Language) — rules and invariants that describe properties the contract must hold, not test cases with expected outputs. The prover then attempts to mathematically verify the property holds across all reachable states, or produces a concrete counterexample transaction trace showing exactly how it breaks.

A typical invariant for a lending protocol:

invariant solvency()
    totalBorrowed() <= totalCollateral() * ltvRatio() / SCALE

rule noUnbackedMint(env e, uint256 amount) {
    uint256 collateralBefore = totalCollateral();

    mint(e, amount);

    assert totalSupply() <= collateralBefore * COLLATERAL_RATIO / SCALE,
        "minted supply exceeded backing collateral";
}

If this rule passes, it holds for every input, every caller, every block timestamp, every ordering of calls the prover can reach — not just the scenarios a test suite happened to script. That's the value proposition: exhaustive coverage of state-transition properties like solvency invariants, access-control boundaries, reentrancy-safety across arbitrary call graphs, and rounding-direction guarantees that fuzzers routinely miss because they need billions of random runs to stumble into the exact edge case a formal rule finds in seconds.

The catch is that formal verification only proves what you specified. Certora doesn't know what "correct" means for your protocol — you tell it, in CVL, and the prover checks your code against your spec. Write a weak or wrong spec and you get a green checkmark on a contract that's still exploitable. Writing good CVL for a nontrivial protocol is itself a specialized skill; a vague or incomplete rule set gives false confidence, which is arguably worse than no formal verification at all.

What manual audit still has to catch

A human auditor reading the code and the surrounding system catches things that have nothing to do with whether the state machine transitions correctly — because the exploit isn't a bug in the transition logic, it's a bug in the economic assumptions.

Classic examples that formal tools don't touch on their own:

• Oracle manipulation. The invariant "collateral value * LTV >= debt" can hold perfectly and still get drained if the price feed itself can be manipulated within a single transaction via a flash-loan-funded AMM swap. The formal spec trusted getPrice(); the exploit lives in what feeds that function.
• MEV and ordering-dependent economics. A liquidation function can be provably correct in isolation and still leak value to sandwich bots or let a searcher front-run liquidations at unfair discount rates.
• Governance and admin key concentration. A single multisig with a 2-of-3 threshold controlling an upgradeable proxy is a centralization risk no invariant will ever flag — it's a design and process judgment call.
• Cross-protocol composability. How your contract behaves when integrated with a rebasing token, a fee-on-transfer token, or a protocol that calls back into yours mid-transaction is often outside the scope of any spec written for your contract alone.
• Intent versus implementation. Sometimes the code does exactly what it was specified to do, and the specification itself encodes a bad business assumption — a fee calculation that's technically consistent but economically wrong for how the protocol is actually used in production.

This is the same gap we cover in more detail comparing manual review against automated scanners across Solana and EVM codebases — tooling finds pattern matches and, with formal methods, proven invariants; humans find intent mismatches and economic attack paths that no tool has a rule for yet.

Side-by-side

	Certora Formal Verification	Manual Audit
Proves	Mathematical guarantee that specified properties hold across all reachable states	Reasoned judgment that logic matches intent and known attack patterns
Finds	Reentrancy paths, invariant violations, access-control gaps, arithmetic edge cases	Oracle assumptions, economic exploits, governance risk, integration hazards
Coverage	Exhaustive for what's specified, silent on what isn't	Bounded by reviewer time and experience, but covers "unknown unknowns"
False confidence risk	High if spec is weak or incomplete	High if reviewer misses a subtle interaction
Cost/timeline	High upfront spec-writing cost, fast iteration after	Scales roughly with LOC and system complexity, typically 1-3 weeks
Best fit	Core invariants: solvency, supply caps, permissioning	Everything the invariants don't capture, plus sanity-checking the invariants

When you actually need both

Skip formal verification for a simple NFT mint contract or a straightforward token with no custom logic — the cost of writing CVL specs won't buy you much over a careful manual read plus a standard code review. It's overkill relative to the attack surface.

Formal verification earns its cost on contracts where a single broken invariant means insolvency at scale: lending markets, CDP/stablecoin systems, cross-chain bridges, anything managing pooled user funds with complex state transitions. On those, a manual-only audit is genuinely risky — invariant violations that only manifest after a specific 40-step call sequence are exactly what human reviewers, working against a deadline, are most likely to miss and fuzzers are least likely to hit by chance.

But formal verification alone on those same contracts is also risky, for the reason above: it proves your spec is internally consistent, not that your spec matches reality. The oracle can still be wrong. The governance threshold can still be too low. The token you integrate with can still break your fee-on-transfer assumption. Those require a human who has seen these failure modes before, ideally someone who has also read the CVL spec and can tell you where it's silent.

The pattern we use with clients: manual audit first to establish threat model and find the design-level issues, formal verification on the properties that matter most for solvency and access control, then a final manual pass focused specifically on what the formal spec didn't cover. That order matters — writing CVL specs against a system you haven't yet audited manually means you're formalizing assumptions nobody has stress-tested yet. We've written about this same escalation logic in the context of choosing between in-house review and third-party audit for TON contracts, and the same "know what each layer actually catches" reasoning applies when comparing FunC and Tact security tooling — different chains, same principle: no single method covers every failure mode.

If your contract is holding more than a few million dollars at steady state, or if a single invariant violation would mean protocol insolvency rather than a contained bug, budget for both. If you're still deciding where your contract sits on that spectrum, that's a conversation worth having before you write either the spec or the audit scope — a quick strategy consultation upfront usually saves more in re-audit costs than it costs.

Get a smart contract audit scoped to your actual risk profile, formal verification included where it earns its keep.