A multi-lens field guide for crypto/DeFi engineers — five ways to read FV (forensics, epistemics, history, economics, AI) laid over a reference spine of four techniques and the tools that ship them
Compiled: 2026-07-02 · claims tagged [V] verified / [I] inferred
Formal verification went mainstream and cheap — the Certora Prover, the commercial gold standard for 7+ years, went fully open source on 2025-02-24 [V], and FV now ships as four distinct techniques (symbolic execution, SMT/Horn model checking, property fuzzing, deductive proof) that the 2026 audit workflow layers: fuzz broadly, prove the load-bearing invariants, then human-audit for the logic no tool can model.
Two layers. The five lenses below are arcs — pick one to understand FV from a chosen angle (what it catches, what a proof means, where it came from, who pays, where AI takes it). Under them sits the technique spine (Taxonomy onward): the reference material every lens points back into. Read a lens for the story; drop into the spine for the tool detail.
The blunt thesis: FV crushes the mechanical bug classes — reentrancy, overflow, access control, rounding — because each reduces to a state property a solver or fuzzer can falsify. FV is nearly useless against economic-design bugs — oracle trust, collateral sizing — because no in-contract invariant is violated: the contract does exactly what it was told, and the flaw is in what it was told [I].
Eight canonical failures, each mapped to the invariant that would block it and the technique that catches that invariant:
| Exploit | Loss | Bug class | Invariant (the spec) | Technique that catches it |
|---|---|---|---|---|
| The DAO (Jun 2016) | ~$60M [V] | Reentrancy | sum(balances)==balance(this); reentrancy lock | Symbolic / SMT / deductive — flagship yes |
| Parity freeze (Nov 2017) | ~$280M frozen [V] | Access control / uninit | initializer locked; selfdestruct unreachable by outsiders | Symbolic reachability / SMT — textbook yes |
| Integer overflow (BEC, 2018) | token collapse [I] | Arithmetic wrap | no op wraps; supply conserved | SMT bitvector / SMTChecker — trivial; solved by solc 0.8 |
| Read-only reentrancy (Sturdy, Jun 2023) | ~$770K [V] | Cross-contract reentrancy | views revert mid-callback | Composed symbolic / forked fuzzing — partial |
| ERC-4626 inflation (class) | millions [V] | Rounding / precision | assets>0 ⇒ shares>0; no round-trip profit | Property fuzzing / SMT — yes, if you write the >0 rule |
| Euler Finance (Mar 2023) | ~$197M [V] | Missing health-check | post-op solvency for every account | Deductive (Certora) / invariant fuzzing — strongest yes |
| Mango Markets (Oct 2022) | ~$116M [V] | Oracle / economic | (none in-contract) manipulation-resistant pricing | — no: design/trust failure, out of scope |
| Flash-loan price manip (bZx/Harvest, class) | ~$34M+ [I] | Oracle / economic | non-manipulable price source | forked invariant fuzzing (narrow) — mostly no |
FV's power tracks whether the failure is a violated in-contract invariant or a satisfied-but-wrong assumption. Mechanical bugs (DAO, Parity, overflow, 4626, Euler) are a state property false on some reachable path — a solver finds it. Composition bugs (read-only reentrancy) live across contracts or below the source (the Curve/Vyper case was a compiler codegen bug — source-level FV passes broken bytecode). Economic bugs (Mango, flash-loans) obey every invariant they were given; the flaw is which price source the designer chose. No solver tells you your economic assumptions are wrong.
Formal verification is a truth-machine for the properties you can state; it is silent on the properties you didn't know to state — and DeFi's most expensive losses were failures of what to state, not failures to check it.
FV does not eliminate trust. It moves trust — from code, to spec, to prover. A machine-checked proof says exactly one thing: the code satisfies the specification. It says nothing about whether the spec captures what you meant, nor whether the prover that checked it is itself correct. Every FV claim is a conditional: IF the spec is right AND the prover is sound AND the model matches the machine, THEN the code is correct [I].
| Tool class | Keeps | Sacrifices |
|---|---|---|
| Sound analyzers, model checkers, deductive provers (CompCert, seL4, Certora) | Soundness — no missed bugs vs spec | Completeness — spurious alarms, annotation burden, may not terminate |
| Bounded model checkers (CBMC), symbolic-exec fuzzers, most "practical" tools | Completeness within a bound | Soundness beyond the bound — a bug at loop-depth k+1 is invisible |
Rice's theorem makes sound + complete + terminating impossible for non-trivial properties, so every tool sacrifices something. "We formally verified X" is meaningless until you know which of soundness/completeness the tool guarantees, and over what domain [I]. A bounded checker that "verified" up to 3 loop iterations has proven nothing about iteration 4.
Certora's Mooly Sagiv calls "a formally verified program cannot go wrong" the biggest myth in the field [V]. Two failure modes:
x=5 ⇒ x>0 is a tautology — it holds regardless of the program, yet the green checkmark reads identically to a real proof. The Certora Prover ships vacuity checks precisely because this is common [V].totalSupply ≥ 0 — true, non-vacuous, and useless: it never catches an inflation bug. The property you needed was totalSupply == Σ balances. Defense: mutation testing — inject bugs, check the spec catches them [V].A wrong spec, proven perfectly, is a lie with a certificate.
Even with a perfect spec, you trust the machine that checked the proof — its trusted computing base [V]:
Never "this code is correct." Always: "this code provably satisfies this specification, assuming the prover is sound and the model matches the machine." FV is a trust-concentrator — it collapses "trust every line" into "trust the spec + a small audited kernel + the model." A real, large win. But a transfer, not an elimination — and it stops at the oracle boundary: garbage-in, proven-garbage-out.
FV spent forty years as an expensive last resort, reserved for domains where a bug killed people, grounded rockets, or triggered a nine-figure recall. Then in the 2020s it went mainstream in smart contracts — not because the math got easier, but because contracts recreated, in one artifact, every condition that historically justified FV [I].
Every prior domain had to argue itself into FV. Contracts arrive pre-loaded with all four justifications at once [I]:
The catalyzing event: 2016 The DAO — crypto's "Ariane 5 / FDIV" moment, an immutable, adversarial, money-holding artifact with a bug testing missed [V]. Smart-contract FV then borrowed the whole toolkit — SMT solving (Z3), abstract interpretation, formal execution semantics (KEVM is to the EVM what CompCert's semantics is to C). What's unique: the economic forcing function, the adversary as default (not tail) threat model, composability, and FV sold as a routine commercial audit product (Certora, RV) rather than an in-house safety practice [I].
FV is now the strongest automated security tool in Web3 and it is free — yet audits still eat most of the budget. Not technical inertia: FV sells proof of a specification, and writing the spec is the expensive, human-scarce, non-automatable part. Open-sourcing the prover collapsed tooling cost to zero and did nothing to the labor cost, which is where the money goes [I].
On 2025-02-24 Certora open-sourced the Prover under GPLv3; it targets EVM, Solana (sBPF), and Stellar (WASM) [V]. Track record at release: 7+ years, >$100B TVL secured, >70,000 rules written by users [V]. Marquee find: a core MakerDAO invariant (the "Fundamental Equation of DAI") was mathematically wrong since 2018, missed by a top audit firm and even mis-proven by the Maker team — caught only by the Prover [V]. The move commoditizes the engine and pushes Certora's business up the stack toward spec-writing and AI tooling [I].
| Layer | 2026 price | What it buys |
|---|---|---|
| Fuzzing (Foundry/Echidna/Medusa, Halmos) | ~free / OSS, engineer time [V] | Shallow-to-medium bugs in CI. The floor everyone pays. |
| Audit (base) | simple token ~$5K; DeFi $25K–$100K; bridge/ZK $250K–$500K+ [V] | Human, broad-scope; economic/logic/integration bugs a spec never encodes. |
| FV add-on | +$20K–$50K; enterprise+FV runs 6–12 weeks [V] | Mathematical proof of invariants. Zero tool cost; recurring spec-labor cost. |
~one-third of high-value 2025 engagements now ship with at least one Certora or Halmos invariant suite — the adoption inflection [V]. The open-source move flattened the tool axis to zero while leaving the labor axis (the dominant term) untouched.
FV concentrates at the top of the TVL distribution: you buy it when P(critical bug) × TVL-at-risk exceeds the fully-loaded cost of writing and maintaining the spec. Trivially true for a $2B lending market; false for a $30M fork-of-a-fork [I]. Audits persist because:
The rest of the stack is ordered by where in the bug lifecycle it acts: Immunefi bounties top $162M available (record single payout $10M, Wormhole 2022) [V]; Code4rena/Sherlock contests ran $100K–$500K pools but Code4rena wound down in 2026, absorbed by Immunefi [V]; Nexus Mutual has protected ~$6B cumulative [V]. FV doesn't shrink these markets — it narrows the class of bugs they must price [I].
FV has always had one dominant cost: writing the spec. The engines (Certora, Halmos, SMTChecker, K) are mature; what gates adoption is that someone must encode, in a DSL like Certora's CVL, what the contract is supposed to do. High-value engagements run past $200,000 [V]. The 2025–2026 bet: LLMs draft that spec layer, turning FV from a boutique service toward a linter. The evidence — LLMs accelerate spec drafting and are strongest at mechanical, shape-known properties, but do not yet remove the human who owns intent [I].
Retrieval-augmented property generation: GPT-4 + a vector DB of human-written properties retrieves reference specs, iterates on compilation feedback, then hands candidates to a prover [V]. ~80% recall vs ground-truth; detected 26 of 37 known CVEs; found 12 zero-days earning $8,256 in bounties [V]. Core insight: LLMs are good at transferring known property shapes — RAG makes it work, not raw generation [I].
Fine-tunes CodeLlama (PEFT) on ~100,000 contract examples to synthesize invariants; beats PropertyGPT on quantity and quality, catches real DeFi exploits [V]. Authors explicitly acknowledge the reliability ceiling — invariant hallucination and the need for validation [V].
The notable product move: an open-source "safe AI coding platform" that embeds the Certora Prover directly in the AI generation loop, so every AI-generated snippet adheres to mathematical safety rules before it runs [V]. Defaults to an Anthropic model (Sonnet); semi-automatic, human-in-the-loop [V]. The clearest signal of direction: not "LLM writes the spec alone" but "prover keeps the LLM honest in a tight loop."
AI is closing the bottleneck on the mechanical axis (drafting speed, known-pattern coverage, on-ramping non-experts) but not on the intent axis (deciding which economic invariant matters). The winning architecture is already visible and consistent across every serious effort: LLM proposes, verifier disposes, human owns intent. The failure modes that require the human are structural, not incidental — the same wall the epistemics lens names.
The lenses above point back into the sections below: the technique taxonomy, the tools that ship each one, the fuzz→prove→audit workflow, and a quick tool index. This is the material every arc references.
FV is no longer one thing. Understanding what class a tool belongs to matters more than the brand name — each class has a different soundness/completeness trade-off.
| Technique | Guarantee | Cost to write | Blind spots |
|---|---|---|---|
| Symbolic execution | Explores all paths up to a bound (loop / call depth). Bounded, not total. | Low — reuse existing tests | Unbounded loops; path explosion |
| SMT / Horn model checking | Reasons over unbounded transactions; proves or refutes safety properties | Medium — write rules/annotations | Solver timeouts; abstraction gaps |
| Property fuzzing | Finds counterexamples; never proves absence of bugs | Low — write invariants | Rare-state bugs; economic edge cases |
| Deductive proof | Strongest — machine-checked proof of full spec | High — spec + proof effort | Effort; specification bugs |
Fuzzing disproves, symbolic execution bounded-proves, model checking unbounded-proves under abstraction, deductive proof fully proves what you specified. None catches a wrong specification — that is what human audit is for.
Reasons over all inputs at once instead of concrete samples; a failing assertion yields a concrete counterexample. Bounded by the loop/call depth you set.
Runs your existing Foundry tests symbolically — instead of concrete fuzz values it reasons over all inputs at once [V].
--loop. Not total FV [V]Fast symbolic-execution framework operating directly on EVM bytecode — compiler-agnostic, works below Solidity [V].
Kontrol combines KEVM and Foundry so engineers verify Foundry tests symbolically without learning a new language [V]. KEVM is the complete formal semantics of the EVM in the K framework and passes the full Ethereum Test Suite [V].
Reasons over an unbounded number of transactions to prove or refute a safety property — the "does this hold forever?" tier.
Compares contract bytecode against CVL rules (a Solidity-like, open-source spec language) and checks all possible states and paths to prove correctness or produce a counterexample [V]. SMT-backed internally — the marketing page says "mathematical auditor" but does not name Z3/CVC5 [V/I].
That single move reshaped the economics of FV: the strongest automated prover is now free, undercutting the "FV is only for billion-dollar protocols" assumption [V].
Built into the Solidity compiler; an SMT + Horn-clause model checker that statically proves safety properties over an unbounded number of transactions at compile time [V].
asserts (treats require as assumptions) [V]solc [V]Move Prover also lives in this bucket — it lowers Move + specs to Boogie → SMT formulas checked by Z3 / CVC5 [V]. See Deductive proof.
The on-ramp: cheap to write, catches most exploitable bugs fast — but it never proves absence of bugs.
Unit, fuzz, invariant, and differential testing in one toolkit; invariant testing checks that fundamental properties hold across thousands of random call sequences [V]. The industry default test harness in 2026 — and the substrate every other tool reuses [V].
ToB says "our primary focus now shifts to Medusa's evolution" while "continuing to maintain Echidna for minor bug fixes." Note: ToB has not declared Medusa a drop-in default replacing Echidna — some practitioners still run both [V]. The Recon platform unifies Echidna + Medusa + Foundry [V].
Spec-instrumentation, not a solver: compiles annotations in the Scribble spec language into concrete Solidity asserts, so a fuzzer/tester can exercise the properties [V]. Pairs with fuzzers [V/I]. Free, open source [V].
The strongest tier — a machine-checked proof of the full spec. Highest effort, and it still only proves what you specified.
Verifies Move contracts against formal specs; translates spec + implementation to Boogie IVL → VCs as SMT formulas → Z3/CVC5 [V]. UX "like a type checker or linter" [V].
Deductive + executable-semantics hybrid: you define a language's meaning and get a prover / interpreter / symbolic engine for free [V]. KEVM (see Kontrol) is the EVM instance of this.
Real but younger — Solana FV tooling generally lags EVM/Move [gap].
Bit-precise model checker for Rust, operating on MIR; proves safety + correctness, supports function contracts [V].
The Solana-native analyzer in the MIR lineage — MIR-based, no annotations required [V]. Where Kani is general-Rust, VRust targets Solana programs directly.
No confirmed 2026 first-party Kani-on-Solana integration was found; the Solana-native path is VRust. Certora's Prover does target Solana + Stellar [V], so the SMT route reaches Solana even where the Rust model-checkers don't.
The 2026 consensus is layered, not either/or [V]. Property fuzzing is the on-ramp; FV is the depth.
Common split seen in practice: FV for core finance logic, fuzzing for integration/upgrade code (attributed to the ChainSecurity workflow) [V].
Fuzzing = cheap, finds bugs, never proves safety. Symbolic / model checking = proves a property (bounded or under abstraction). Deductive proof = proves full spec, expensive. Audit = finds the bugs in your spec and your assumptions.
| Shift | Why it matters |
|---|---|
| Certora open-sourcing (2025-02-24) [V] | The single largest economic shift — the strongest commercial prover is now free |
| Medusa becomes ToB's primary fuzzer focus [V] | Echidna still maintained; not a hard default swap |
| Halmos adds stateful invariant testing [V] | Narrows the gap between "just fuzzing" and "symbolic FV" using the same Foundry tests |