Formal Verification vs Fuzzing vs Audit: Which Do You Need?
Quick answer. Start with a manual audit: it finds logic and design flaws no tool is told to look for. Add invariant fuzzing for accounting-heavy code, and formal verification for a few critical properties in stable, high-value code.
Video transcript
Audits, fuzzing and formal verification answer different questions. For most protocols, the answer starts with a manual audit.
An audit finds what nobody thought to write down. Fuzzing hunts for call sequences that break a property you wrote. Formal verification checks whether it holds for every input.
Tools struggle with that first job. In a study of 127 major attacks, automated tools could have prevented only 8 percent.
Fuzzing and formal verification only check properties someone wrote down. A clean fuzz run is some assurance, not proof. And if a solver times out, no guarantee can be provided.
Most tools are open source, so you pay for expert time. Aave's 2024 Certora renewal cost 1.7 million dollars for a year, covering reviews, proofs and incident response.
In Guardian's view, all new or changed code that handles value gets an audit. Accounting-heavy code adds an invariant suite. Formal verification fits small, stable, critical code.
Guardian's smart contract audit runs three passes: a design review, an invariant suite and a senior manual audit. The suite stays on as a regression harness.
Vanguard puts two independent teams on one scope. Team A pairs expert manual review with fuzzing. Team B directs Helix, Guardian's AI auditor. Only human-verified findings reach the report.
Read the full article for the decision matrix, or talk to Guardian about Vanguard at guardian.security.
The three are often sold as alternatives. They answer different questions:
- Audit: what is wrong that nobody thought to write down?
- Fuzzing: can any sequence of calls break a property you wrote?
- Formal verification: does that property hold for every possible input?
Fuzzing and formal verification check only the properties you give them. An audit is where missing properties get found.
What Each Method Covers
| Method | Finds | Misses |
|---|---|---|
| Manual audit | Logic, design, economic and integration flaws | Whatever time and scope do not reach |
| Fuzzing | Call sequences that break a written invariant | Unwritten properties; states never reached |
| Formal verification | A proof that a property holds, or a counterexample | Unwritten properties; cases past loop bounds or timeouts |
Manual audit
Reviewers read the code at a commit and reason about intent, design and economics.
Existing automated tools struggle here. In a study of 127 major attacks worth $2.3B, Chaliasos and co-authors found the tools could have prevented only 8%, worth $149M.
The developers and auditors they surveyed rated logic bugs and protocol-layer flaws as major threats that tools do not address well.
Fuzzing
A fuzzer generates inputs and call sequences, then checks properties after each step. Foundry "runs random sequences of function calls and checks invariants after each call."
Echidna, Trail of Bits' fuzzer, builds its inputs from the contract ABI. Medusa, inspired by Echidna and built on go-ethereum, runs parallel, coverage-guided campaigns.
A fuzzer can only break a property you wrote, in a state it reached. Echidna's own README calls a clean run "some assurance the contract is safe," not proof.
Formal verification
A prover turns code and a specification into logic, then asks a solver whether any input breaks it. If one does, the Certora Prover returns a concrete counterexample.
Proofs have edges. Certora unrolls loops a fixed number of times, once by default, and its optimistic loop mode "may hide bugs."
A rule whose assumptions exclude every case passes without checking anything; Certora calls it vacuous. And as Trail of Bits notes, "If the solver times out, no guarantee can be provided."
Halmos, from a16z, runs Foundry-style tests symbolically, for all inputs. It bounds loops and, in its author's words, "prioritizes automation over completeness."
Cost and Time
Most of the tools are open source. The cost is the expert time around them.
| Method | Tools | Main cost |
|---|---|---|
| Manual audit | Reviewers' own tooling | Auditor-weeks, set by scope |
| Fuzzing | Foundry, Echidna, Medusa (open source) | Writing good invariants |
| Formal verification | Certora Prover, Halmos (open source) | Specialists writing specs |
Audits are priced in auditor-weeks. Our cost estimator turns a codebase's size into a range.
For fuzzing, Trail of Bits says "Writing good invariants is 80% of the work." In its own test, Echidna found two bugs first found by formal verification, in minutes on a laptop.
Formal verification needs "significant engineering efforts," per Trail of Bits, and code may need rewriting to suit the prover.
One public price: Aave's 2024 renewal with Certora cost $1.7M for a year. That retainer covered manual reviews, formal verification, governance proposal reviews and 24/7 incident response.
For other retainers, see what top auditors charge.
Matching Method to Risk
Trail of Bits recommends starting with fuzzing and using formal verification "only when appropriate."
It suggests waiting until you have fuzzed many invariants and know which components would benefit from a proof.
In our view, each method has a natural home:
- Audit: all new or changed code that holds or moves value.
- Invariant fuzzing: accounting, rounding, solvency and multi-step state.
- Formal verification: small, stable, critical code where a proof repays the spec work.
Whatever you choose, measure the suite. Mutation testing shows which planted bugs your tests miss.
To try proofs yourself, start with formal verification of smart contracts using Solidity's built-in SMTChecker.
Combined Programs
Mature programs combine methods, each where it is strongest.
Aave's 2023 proposal with Certora says "new code is formally verified and manually reviewed."
Its formal rules also run in Aave's CI "to continuously check changes introduced into the code."
An invariant suite works the same way. Written once, it reruns on every fix and upgrade.
Decision Matrix
Our view, built on the sources above:
| Situation | Audit | Fuzzing | Formal verification |
|---|---|---|---|
| Simple token or vault | Yes | Foundry fuzz tests | Rarely worth it |
| New lending, AMM or stablecoin | Yes | Full invariant suite | For core solvency rules |
| Math library or pricing core | Yes | Yes | Strong fit |
| Frequent upgrades | Review each diff | Rerun the suite in CI | Rerun rules in CI |
| Fork of audited code | The diff and the code it touches | Reuse and extend upstream tests | Rarely worth it |
How Guardian Combines Them
Guardian's smart contract audit runs three passes: a design review, an invariant suite and a senior manual audit.
Vanguard puts two independent teams on one scope. Team A uses expert manual review and gets the most out of the fuzzing suite.
Team B directs Helix, Guardian's AI auditor, across the codebase. Only human-verified findings become the final result.
The invariant suite covers accounting, rounding, solvency, math formulas and edge states. It outlives the audit as a regression harness for later changes.
Some of Guardian's public reports list their invariants. The Nashpoint protocol review lists 113, each run 10M+ times.
Frequently Asked Questions
Is formal verification better than fuzzing?
Not by default. Formal verification can prove a property for every input, within its bounds; fuzzing tests only the states it reaches. Trail of Bits argues fuzzing gives similar results for less skill and time, so it recommends fuzzing first.
Can fuzzing or formal verification replace an audit?
No. Both check only the properties someone wrote down. An audit looks for design, logic and integration flaws nobody specified, and it often surfaces the properties worth fuzzing or proving.
How much does formal verification cost?
The Certora Prover and Halmos are open source, so the cost is specialist time. One public price point: Aave's 2024 renewal with Certora, covering manual review, formal verification and more, was $1.7M for a year.
What is invariant fuzzing?
It runs random sequences of function calls against a contract and checks, after each call, properties that must always hold, such as solvency or correct accounting. Foundry, Echidna and Medusa all support it.
Sources
- Trail of Bits: Why fuzzing over formal verification? (March 22, 2024)
- Chaliasos et al.: Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?, arXiv (revised January 22, 2024)
- Foundry docs: Invariant testing (accessed November 5, 2026)
- crytic (GitHub): Echidna, by Trail of Bits (accessed November 5, 2026)
- crytic (GitHub): Medusa (accessed November 5, 2026)
- Certora docs: User guide (accessed November 5, 2026)
- Certora docs: Loop unrolling (accessed November 5, 2026)
- Certora docs: Rule sanity checks and vacuity (accessed November 5, 2026)
- Certora: Certora goes open source (February 24, 2025)
- a16z: Symbolic testing with Halmos, leveraging existing tests for formal verification (February 2, 2023)
- a16z (GitHub): Halmos (accessed November 5, 2026)
- Aave governance forum: [ARFC] Continuous Security Proposal Aave and Certora (December 2023)
- Aave governance forum: [ARFC] Aave and Certora Continuous Security Services (October 1, 2024)
- Guardian: Nashpoint Protocol Review report (December 2025)
- Guardian: Smart Contract Audit
- Guardian: Vanguard
Get manual review and fuzzing on one scope
Vanguard pairs two independent audit teams with an invariant suite that keeps testing every change you ship.