Formal Verification Replacing Auditors?

Traditional smart contract security was forged under the shadow of catastrophic failure, yet its primary instrument, the heuristic manual code review, has always suffered from one structural flaw: human cognition cannot traverse a combinatorial state space. For the first decade of decentralized application development, audits were bespoke artisan inspections. Teams of specialists read Solidity line by line, ran pattern-matching linters, executed unit tests, and wrote adversarial scenarios by hand.

Nearly 10,000 audit reports were issued for protocols launched between January 2020 and January 2025, and DeFi has lost $8.2 billion to exploits since 2016 (Landsman et al., 2025). In many ways, DeFi is the proving grounds for the bleeding edge of security technology.

Advances in satisfiability modulo theories (SMT) solvers, bounded model checking (BMC), neuro-symbolic auto-formalization, and hybrid symbolic execution engines have made formal methods accessible and, for the first time, computationally tractable. That has not eliminated the auditor. It has obliterated the traditional role and elevated the job into a more critical one. When a solver can settle an invariant over every value a 256-bit state variable can take, the auditor's value no longer lies in discovering whether a state variable can overflow or whether a reentrancy guard was omitted.

The auditor's mandate is starting to shift to questions no automated engine can formulate on its own:

• Are these specifications compete and correct?
• Does this invariant capture economic solvency?
• What happens when our proven model interacts with an unverified external liquidity pool across multiple asynchronous transactions?

This post walks through the technological breakthroughs that made formal verification viable, the structural evolution of the auditor's workflow, and the mathematical machinery inside modern provers, and it marks the exact boundaries where automated proofs stop and human adversarial intuition has to take over.

01 The Heuristic Auditing Impasse

To understand why security auditing is transforming, start with the structural breakdown of the heuristic model.

The Illusion of the Auditor's Stamp

For years, the smart contract audit served as an insurance policy and a marketing asset. Protocols sought audits from prestigious firms to display a badge of security on their landing pages.

It's fair to say that the market frequently misunderstood the underlying deliverable. A security audit was never a guarantee of correctness; it was a snapshot of a team's best-effort attempt to identify known vulnerability patterns within a constrained time budget, typically two to four weeks (David et al., 2023; Chaliasos et al., 2023).

Auditing tools arrived two to four years after The DAO in 2016, and Euler Finance still lost $197 million in 2023. The incidents on the left of the axis and the tooling on the right are the decade in one picture.

The traditional manual review process suffers from three structural weaknesses:

• Temporal and cognitive fatigue. A human auditor reviewing 5,000 lines of complex, math-heavy DeFi code cannot maintain uniform cognitive vigilance. Attention wavers, edge cases are overlooked, and complex inter-function dependencies are abstracted away into mental shortcuts.
• Heuristic pattern matching. Auditors look for bugs they have seen before. When reentrancy emerged with The DAO hack in 2016, the industry pivoted to look for external calls preceding state updates. When flash loans emerged in 2020 (Qin et al., 2020), auditors hunted for unweighted spot-price oracle queries. But vulnerabilities in contemporary decentralized finance are rarely copies of past exploits; they are emergent systemic anomalies arising from complex interactions within the code.
• Absence of proof versus proof of absence. An audit report detailing twenty resolved issues provides no mathematical assurance about a twenty-first, lethal bug. As Edsger W. Dijkstra observed, testing can show the presence of bugs, never their absence. Manual auditing is dynamic testing run on biological hardware, and it shares the same theoretical limits.

The State Explosion Crisis

Smart contracts run on deterministic state machines like the Ethereum Virtual Machine (EVM). Individual contracts often look small next to enterprise software, yet their reachable state space is unbounded.

Consider a lending protocol vault with five core external functions: deposit(), withdraw(), borrow(), repay(), and liquidate(). Each accepts several 256-bit unsigned integers and arbitrary Ethereum addresses, and can be invoked in any order by any number of callers across an unbounded sequence of blocks. The contract's state comprises hundreds of storage slots, balances, interest rate accumulators, and dynamic mappings. A human auditor evaluating this system mentally computes transitions along a few hundred intuitive paths:

What happens when the sequence is this instead?

The reachable state space holds astronomically many execution permutations. An auditor examining code over two weeks explores perhaps several hundred transitions. Attackers, aided by algorithmic search, automated fuzzing scripts, and MEV searchers, need to find only one of the permutations the human missed.

The Limits of First-Generation Tooling

Recognizing the limits of manual review, the smart contract auditing industry deployed first-generation automated security tools between 2018 and 2020:

• Static pattern matchers and linters (Slither, Mythril). These engines analyze the control flow graph (CFG) and abstract syntax tree (AST) to flag suspicious patterns: state modifications after external calls, unindexed events, reentrancies (Feist et al., 2019; Mueller, 2018). Fast, but plagued by two opposing failure modes: massive false-positive rates that drown auditors in noise, and an inability to reason about protocol-specific business logic. A linter can tell that a function lacks an onlyOwner modifier. It cannot tell whether an automated market maker's equation $x·y=k$ can be manipulated through rounding errors in an internal pool.
• Property-based fuzzers (Echidna, Foundry fuzzing). Fuzzers construct randomized inputs to break assertions, and guided by code coverage they are good at shallow and medium-depth vulnerabilities (Grieco et al., 2020). But fuzzing remains probabilistic. If an exploit needs an attacker to satisfy a 256-bit cryptographic condition or hit an exact, narrow invariant along a 10-step transaction chain, a fuzzer may run billions of iterations without reaching the vulnerable state.

The fundamental deficit of both approaches is the absence of mathematical proof. Neither can guarantee that an invariant holds across every conceivable execution path. A symbolic executor paired with an expert system, run at chain scale, surfaced whole classes of greedy, prodigal, and suicidal contracts (Nikolić et al., 2018), yet the coverage question stayed open. The industry accepted that failure as a cost of doing business in decentralized finance.

The Same Gap in Zero-Knowledge Tooling

An adjacent area zero-knowledge auditing shows how far the gap runs even for dedicated tools. Kolozyan et al. (2026) ran every open-source Circom analyzer they could execute non-interactively against 70 real-world vulnerabilities. The same pattern holds beneath the tooling, in the implementations themselves: the systemization of knowledge "What don't we know? Understanding Security Vulnerabilities in SNARKs" catalogues 141 actual vulnerabilities in deployed systems and evaluates which defenses catch them (Chaliasos et al., 2024). The catalogues keep growing: zkBugs, zkSecurity's public database, indexes 139 ZK bugs from published audits by vulnerability, impact, and root cause, and the Ethereum Foundation has partially funded the work (zkBugs).

On code isolated in a minimal wrapper, at least one tool caught 45.7% of the bugs. On the original project codebases the figure fell to 19.6%, mostly through errors and timeouts, and none of the six bugs rooted in circuit design was detected in either mode. Tools that behave on a curated fragment often fail on the whole system.

02 Why Verification Scaled (2024–2026)

Formal verification is not a new discipline. Its foundations reach back to Robert Floyd's work on flowchart verification in 1967, Tony Hoare's axiomatic basis for computer programming in 1969, and Edsger Dijkstra's weakest precondition calculus in 1975. For decades it stayed confined to safety-critical hardware verification at companies like Intel and IBM, aerospace engineering at NASA, and microkernel projects like seL4. Applying it to general-purpose software was often considered economically and technically infeasible.

The academic groundwork for smart contracts came earlier. Complete formal semantics of the EVM in K (Hildenbrandt et al., 2018), bytecode verification in Isabelle/HOL (Amani et al., 2018), a dedicated verification tool for EVM bytecode (Park et al., 2018), solc-verify (Hajdu and Jovanović, 2020), Securify (Tsankov et al., 2018), VeriSmart (So et al., 2020), ConCert in Coq (Annenkov et al., 2020), and an executable EVM semantics in Dafny (Cassez et al., 2023) all showed that verification was possible. The early F* work on Ethereum contracts made the same case (Bhargavan et al., 2016).

What they lacked was cost. Between 2024 and 2026, a series of structural breakthroughs lowered the barriers and moved formal verification into mainstream smart contract development.

The Inherent Determinism of Blockchain State Machines

Traditional software is notoriously hostile to formal methods. Operating systems, multithreaded cloud architectures, and web backends feature non-deterministic concurrency, asynchronous I/O, dynamic memory allocation, network latency, hardware interrupts, and opaque third-party runtime libraries. Proving properties about such systems means modeling vast environments, which leads straight to state explosion.

Smart contracts, by contrast, are uniquely well suited to formal methods:

• Deterministic execution. Given state σ and transaction T, the post-state σ′ is completely deterministic. There is no multithreading inside an EVM transaction.
• Constrained execution footprint. The EVM gas model limits computational depth, preventing infinite loops and unbounded resource consumption during execution.
• Explicit memory and storage semantics. State is strictly compartmentalized into transient memory, calldata, and a 256-bit-to-256-bit key-value persistent storage trie.
• Small code size. Protocols typically consist of a few thousand lines of code rather than millions.
• High economic density. Last, but certainly not least, smart contracts control billions of dollars in pure liquidity. The cost of formal verification, once tens of thousands of dollars in specialized engineering, is minor next to the cost of an exploit.

Advances in SMT Solvers and Intermediate Languages

The first barrier to practical formal verification was the solver bottleneck. When code is compiled into logical constraints, SMT solvers like Z3 and CVC5 determine whether the negation of a desired property is satisfiable. If it is, the solver outputs a concrete counterexample: the exact exploit payload.

Historically, EVM arithmetic made SMT solvers grind to a halt. The EVM operates natively on 256-bit words. Proving properties involving modular arithmetic, bitwise shifts, and hashing (Keccak-256) forced solvers to reason over non-linear integer arithmetic together with bit-vector theories. The bit-vector part is decidable; the non-linear arithmetic is not, and the two together are what exhaust a solver.

Solvers frequently timed out and left auditors with inconclusive results (Mota et al., 2023): eThor, a provably sound static analyzer for Ethereum bytecode built on Z3 (Schneidewind et al., 2020), spent several hours on a real-world vault without returning an answer. Recent developments have changed that:

• Three-address code (TAC) and bytecode simplification. Tools like the Certora Prover compile Solidity bytecode down to an intermediate three-address code representation (Certora, 2024). Static analysis then tracks variable lifetimes, prunes irrelevant storage variables, and inlines execution branches before constraint generation.
• Domain-specific constraint optimization. Modern provers abstract cryptographic hashes. Instead of unrolling the full Keccak permutation, solvers treat hashing as an uninterpreted function with an injectivity axiom (x ≠ y ⟹ H(x) ≠ H(y)), which prevents solver lockup at the cost of an assumption stronger than reality: Keccak-256 maps arbitrary-length input into 256 bits, so a proof discharged this way holds only for a collision-free model.
• Bit-precise bounded model checkers. Frameworks like Halmos (for the EVM) and Kani (for Rust/Solana) bypass complex theorem-proving setups. They symbolically execute tests written directly in Solidity or Rust and translate assertions into bounded SMT queries, without requiring developers to learn an exotic proof assistant language (OtterSec, 2024).

The Neuro-Symbolic Catalyst: Auto-Formalization

The final barrier was the formalization gap. Historically, verifying a protocol required a PhD in formal methods who knew how to translate Solidity into mathematical specifications in Coq, Isabelle/HOL, or CVL. That labor pool was minuscule, and it created an industry-wide bottleneck (CertiK, 2023a; Braghin et al., 2023).

Recent benchmark evaluations by Novak and Kovacs (2025) put numbers on the result. On a suite of 42 real-world exploit patterns, hybrid formal systems, which combine symbolic execution to isolate candidate paths with SMT checking to verify correctness, reached a Verification Quality Index (VQI) of 0.908. They detected 94.2% of real-world vulnerability patterns with a false-positive rate of just 3.8%.

Vendors are folding this loop into products. Certora's AutoProver, announced in July 2026 and in Solidity beta, reads a repository and its documentation, drafts properties, writes Foundry tests and CVL rules, runs the Prover, triages failures, and reports code bugs and design bugs separately (Certora, 2026a). Its announcement puts the motivation plainly: "writing specifications has always been the bottleneck." Its sibling, the AI Composer of November 2025, works at the other end: it embeds the Prover in AI code generation, so generated contracts are checked against safety invariants as they are written rather than afterwards (Certora, 2025).

Neither announcement publishes benchmarks or case studies, so they show where the tooling is heading rather than how well it works.

These numbers mark a turning point.

Formal verification is no longer an academic exercise; it is an active engineering layer with higher detection rates than fuzzing or abstract interpretation, at a false-positive rate in the low single digits.

Shift Towards Publishing Formal Audit Reports

Audit firms' own output shows the same shift. The table below lists 2026 formal-verification engagements that could be found online, keyed by the month the engagement concluded.

Each row links to the published report; where a Certora filename carries a date, that is the repository's publication date, one to four months after the month listed here. It is a sample rather than a census, and it leans toward Certora because that firm posts its reports in one public repository (Certora, 2026b).

Ten of the seventeen reports list at least one medium-severity or higher finding, and only the Aave V4 Libraries and StableVault reports found nothing. Several of these engagements pair a prover with manual review, the Monad and OpenVM reports examine proofs the client supplied, and in the Orchard report the auditors wrote the Lean proofs themselves, so the counts do not measure what the provers alone caught.

The table stops at July because the most recent formal-verification work from a major firm, Trail of Bits' September review of the Miden zkVM, came out as a blog post rather than a report with severity counts. Its Lean proofs cover 95 library procedures and turned up two bugs the unit tests had missed, and a later section returns to it (Trail of Bits, 2026).

Read the table with its composition in mind, because firms publish very different mixes. Counting the files and the labels each one carries in its own repository for 2026:

• Certora. Fifteen reports carry a formal-verification label against twenty-eight marked as manual reviews (Certora, 2026b), so verification is roughly a third of its output.
• Trail of Bits. Fifty-two security reviews, none labelled a formal-verification report, though the Anza engagement above reports Lean and Tamarin models.
• zkSecurity. Nine reports dated 2026 from its report site, two of them with Lean 4 work, and the site warns the list is not exhaustive.
• Spearbit. Three 2026 engagements in its public portfolio, all manual or competitive.
• Nethermind. Fifteen dated 2026 in its audit archive, among seventy-odd reviews, none a formal-verification report, though it also sells formal verification.

Certora is the outlier that files proof work in bulk in one public place, which is why twelve of the seventeen rows above are its.

The shift the numbers support is still an early phenomenon: formal-verification reports now exist in volume, dated, public, and carrying severity counts, but they have not displaced manual review, which remains the bulk of published audit output.

The shift is funded as well as published. Through 2024 and 2025 the Ethereum Foundation ran a three-track formal verification program for zkEVMs, and its award record reads like a roster from earlier in this post: zkSecurity for circuit fuzzing and a Lean DSL for AIR circuits, Veridise for LLZK, Nethermind for Plonky3 in Lean, Certora on verifying autoprecompiles, Runtime Verification checking revm against KEVM, and a Lean backend for Sail so the official RISC-V specification can be reasoned about directly (Verified zkEVMs). Applications have since closed, which is its own datum: the funding arrived with the tooling and wound down with it.

03 From Bug Hunting to Specification

Once verification is cheap enough to run on every change, the scarce resource stops being the hours an auditor spends reading code. This section looks at what replaces that work and how the job is redefined around it.

The practical result is a change in what an auditor does all day. The comparison below sets the old toolkit beside the new one, and the subsections after it cover who now owns the specification and how properties are written in practice.

The Inversion of Responsibility

When an auditor acts as a manual bug hunter, they take on an impossible responsibility: certifying that thousands of lines of mutable, interactive code are safe. When they act as a specification engineer, they shift to a principled methodology grounded in formal methods:

• Deconstructing the protocol into state transitions. The auditor models the protocol as a transition system $M=(S,S_0,𝒯,ℐ)$, where S is the set of all possible EVM states, $S_0\subseteq S$ is the set of valid initial states (post-deployment), $𝒯:S\times \text{Tx}\to S$ is the state transition function enforced by the bytecode, and $ℐ:S\to \text{Prop}$ is the invariant the proof has to establish.
• Formulating inductive invariants. The auditor's primary creative contribution is defining inductive invariants. A property is inductive when it holds in every initial state and every transition preserves it; when it does not, the auditor strengthens it with auxiliary invariants until it does. The next section spells out the two obligations a prover discharges to establish that.
• Handing the invariants to a prover. Once the auditor expresses these invariants in a formal specification language like the Certora Verification Language (CVL), the prover handles the verification. If it succeeds, the property is proven for all inputs and states. If it fails, the prover generates a concrete trace showing the exact execution path that breaks the invariant.

The auditor no longer spends time finding execution paths. They spend it ensuring that no critical invariants were omitted.

The Mechanics of Specification Languages: Writing CVL Rules

To see the transformation in practice, consider how an auditor approaches an ERC-4626 tokenized vault. Under the heuristic model, the auditor reads the math, checks for division by zero, reviews rounding directions in convertToShares() and convertToAssets(), and examines the contract for inflation attack protections.

With formal verification, the auditor writes the mathematical properties that govern vault behavior. Using CVL, the auditor codifies the two properties a balance-based vault can actually break: a deposit must mint shares worth the assets paid in, and it must not degrade the share price for the depositors already in.

// Mathematical specification in Certora Verification Language (CVL)

methods {
    function convertToAssets(uint256) external returns (uint256) envfree;
}

/// @title Deposit fidelity: a deposit must mint shares worth the assets paid in
/// @notice Catches first-depositor inflation: a direct donation inflates the share price
///         until the next deposit rounds down to zero shares
rule deposit_mints_shares_worth_the_deposit(env e, uint256 assets, address receiver) {
    require e.msg.sender == receiver;
    require assets > 0;

    uint256 shares = deposit(e, assets, receiver);

    // Zero shares means the assets became a gift to whoever held the vault before
    assert shares > 0,
        "Economic exploit: the deposit minted nothing and gifted the assets away";
    assert convertToAssets(shares) >= assets - 1,
        "Rounding loss above one wei";
}

/// @title Anti-dilution rule: an external deposit must strictly increase or preserve the share value
/// @notice Prevents deposit-based inflation attacks and rounding exploitation
rule deposit_cannot_dilute_existing_shares(address user, uint256 assets) {
    env e;
    require e.msg.sender == user;
    require assets > 0;

    uint256 sharePriceBefore = convertToAssets(1e18);

    uint256 mintedShares = deposit(e, assets, user);

    uint256 sharePriceAfter = convertToAssets(1e18);

    // The share price for existing depositors must never degrade
    assert sharePriceAfter >= sharePriceBefore,
        "Economic exploit: deposit lowered share value for existing depositors";
}

The two rules are written for this vault; their shape follows Certora's ERC-4626 workshop, whose assetAndShareMonotonicity rule covers the related monotonicity property (Certora, 2023).

When this specification is fed to the verification engine alongside the Solidity source, the engine evaluates each rule against every function in the contract. The prover checks whether any public or external routine, whether deposit(), mint(), withdraw(), redeem(), or a low-level internal hook, can invalidate the condition. If an edge condition exists where an attacker can inflate the share price via a direct asset donation, the prover outputs a counterexample:

[FAIL] deposit_mints_shares_worth_the_deposit
Counterexample Found:
Initial State:
  totalSupply = 1
  totalAssets = 1
  underlyingToken.balanceOf(vault) = 1
Call Sequence:
  attacker.call -> underlyingToken.transfer(vault, 1000000e18)
  victim.call   -> vault.deposit(1000e18, victim)
Post State:
  sharesMinted = 0
  assetsDeposited = 1000e18
  Assertion Violation: convertToAssets(shares) >= assets - 1 fails (0 < 1000e18 - 1)

The trace shows the attack in four moves. A wei was enough to mint the vault's only share while it was empty. A direct token transfer then raises totalAssets without minting anything, so the victim's deposit is priced against the inflated balance and rounds down to zero shares. The assets stay in the vault with no shares claiming them, and the attacker redeems the sole share to take the whole balance, the victim's deposit included.

The prover generates the exploit sequence automatically. The auditor analyzes the mathematical violation and works with the engineering team to restructure the contract logic, for example by implementing virtual liquidity shares to neutralize first-depositor inflation attacks.

04 How Verification Engines Work

To work with these tools, auditors must understand the mathematics inside these engines. Modern formal verification tools are not monolithic. They rely on distinct formal methods with different trade-offs, on decidability and expressiveness as much as on automation.

Bounded Model Checking (BMC)

Bounded model checking unrolls loops and recursion up to a fixed depth k and encodes program execution as a propositional satisfiability problem. Let a system be defined by an initial state predicate $I\left(s_0\right)$, a transition relation $T(s_i,s_{i+1})$, and a safety property P(s). BMC determines whether an error state violating P can be reached within k steps:

If ${\Phi }_k$ is satisfiable, the solver outputs the variable assignments that yield the path to $\neg P\left(s_i\right)$. If it is unsatisfiable, the property holds for all executions up to depth k. In tools like Halmos and Kani, BMC applies directly to source code and compiled bytecode, and the auditor writes properties as standard code assertions:

// Rust bounded model checking with Kani for a Solana / Anchor program
#[kani::proof]
#[kani::unwind(4)] // Bound loop execution to 4 iterations
pub fn verify_vault_withdraw_integrity() {
    let mut vault: VaultAccount = kani::any();
    let withdraw_amount: u64 = kani::any();

    // Assume precondition: vault is initially solvent
    kani::assume(vault.total_deposits >= vault.reserved_liabilities);
    kani::assume(withdraw_amount <= vault.total_deposits);

    let pre_balance = vault.total_deposits;
    let result = vault.process_withdraw(withdraw_amount);

    if result.is_ok() {
        // Assert postcondition: solvency invariant preserved
        kani::assert(
            vault.total_deposits == pre_balance - withdraw_amount,
            "State corruption: deposit accounting mismatch"
        );
        kani::assert(
            vault.total_deposits >= vault.reserved_liabilities,
            "Insolvency: reserved liabilities exceed remaining balance"
        );
    }
}

The harness is written for this vault; its shape follows the approach in OtterSec's Solana case study, which applies Kani to an Anchor program (OtterSec, 2023).

Inductive SMT-Based Proving

Inductive proving achieves unbounded, mathematical completeness over infinite state spaces. Instead of exploring paths up to depth k, it uses induction to prove that an invariant holds across every possible transition. To verify invariant ℐ over transition relation T, two obligations must discharge:

• Initiation: prove that $\forall s_0\in S_0.ℐ\left(s_0\right)$
• Consecution: prove that $\forall s,s^{\prime }.\left(ℐ\right(s)\wedge T(s,s^{\prime }\left)\right)⟹ℐ\left(s^{\prime }\right)$.

The main engineering challenge in inductive proving is that most domain-level invariants are not inductive on their own. The transition system may contain an intermediate, unreachable state s that satisfies ℐ(s) but transitions to an invalid state s′.

The auditor's task is to formulate auxiliary invariants, or strengthen the invariant, until the property becomes inductive. That takes a deep understanding of the contract's internal dependencies.

Interactive Theorem Proving (Lean 4, Coq)

Interactive theorem proving sits a tier above the SMT-based approaches in what it can certify. Systems like Lean 4, Coq, and Isabelle/HOL formalize the semantics of the underlying virtual machine, such as the EVM or SVM. In an interactive prover, proofs are terms in a dependent type theory, verified by a small, trusted logical kernel. The proof is a machine-checked mathematical object, not the output of a heuristic SMT solver.

Frameworks like EquiVM and EVMYulLean embed executable formal semantics of the EVM inside Lean 4 (Lazaropoulos and Paraskevopoulou, 2026; Nethermind Formal Verification Team, 2025). Verity, a research language from LFG Labs, puts the same idea inside one Lean EDSL: the contract, its specification, and the proof that they agree are checked together at compile time, on a compiler whose lowering to IR is proved generically rather than per contract.

Auditors can write foundational refinement proofs showing that an optimized, deployed bytecode contract matches a pure, high-level functional specification (Lazaropoulos and Paraskevopoulou, 2026):

-- Formal verification of state transition in Lean 4
import EVMYulLean.Semantics

structure VaultState where
  balances : Address → Nat
  totalSupply : Nat
  totalAssets : Nat

/-- 1:1 share accounting: the vault stays solvent while its assets cover the shares issued. -/
def SolvencyProperty (s : VaultState) : Prop :=
  s.totalAssets ≥ s.totalSupply

/-- A deposit credits the caller 1:1 and adds the same amount to the vault's assets. -/
def execute_deposit (s : VaultState) (caller : Address) (amount : Nat) : VaultState :=
  { s with
    balances := fun a => if a = caller then s.balances a + amount else s.balances a
    totalSupply := s.totalSupply + amount
    totalAssets := s.totalAssets + amount }

theorem deposit_preserves_solvency
    (s : VaultState) (caller : Address) (amount : Nat)
    (h_solv : SolvencyProperty s) :
    SolvencyProperty (execute_deposit s caller amount) := by
  dsimp [SolvencyProperty, execute_deposit]
  omega -- Automated Presburger arithmetic tactic discharges the linear proof

The model is written for this vault: it imports EVMYulLean's semantics, and because the 1:1 accounting keeps the obligation linear, the Presburger decision procedure omega closes it without a hand-written proof.

Interactive theorem proving offers the strongest assurance of the approaches benchmarked here, though not the best VQI. Its trusted computing base (TCB) consists solely of the proof kernel, which removes any reliance on massive SMT solver codebases, and what it produces is a machine-checked proof rather than a solver's verdict. The trade-off is cost: hours of expert time per contract and the lowest developer-usability score in the set, which is what pushes theorem proving to fifth place overall (Novak and Kovacs, 2025). Today, LLM-based tactical agents generate intermediate proof steps (intros, induction, simp, omega), which lets auditors focus on defining theorems, boundary constraints, and architectural invariants.

05 Outside the Prover's Reach

Every guarantee in the earlier sections comes with conditions. Where those conditions fail is where the attacks live, and every one of them reaches a system that already carries a machine-checked proof.

The claim that a proof secures a system is easy to overstate in both directions, so it helps to separate what a prover can discharge from what stays outside its reach. The comparison below draws that line, and the rest of this section takes the outside half case by case.

The Specification Problem: “Verifying the Wrong Thing”

The central challenge in formal methods is the specification problem: verifying that a program meets its specification does not guarantee the specification captures what the designer intended. When the specification is generated too, by agent loops building compilers and browsers from a prompt, the gap widens: the artifact can look finished while the statement it was built against goes unchecked. Stubbornly Under-Specified follows that gap through two generated systems.

In their benchmark of formal methods frameworks, Novak and Kovacs (2025) observed that out of 42 real-world exploits, interactive theorem proving detected 41. The single vulnerability it missed, governance manipulation via uncollateralized flash-borrowed voting tokens, is instructive:

• The code's perspective. The governance contract strictly upheld its specification: one token held at the snapshot block equals one vote; the address with the majority of valid votes wins the proposal.
• The verifier's perspective. The proof was checked and confirmed. Every invariant passed: unauthorized votes were impossible, balances were accurately updated, and voting timelines were preserved.
• The exploit. An attacker borrowed $50 million worth of governance tokens using a flash loan (Qin et al., 2020), created the proposal and cast a deciding vote to liquidate the treasury into their own wallet within the same block, and returned the borrowed tokens.

// Example: the vulnerability that passes formal verification
// The code satisfies the specification exactly: voting weight is the balance
// held at the snapshot block, and only that balance is tallied.

function castVote(uint256 proposalId, bool support) external {
    Proposal storage prop = proposals[proposalId];
    require(block.number >= prop.startBlock, "Voting not active");
    require(block.number <= prop.endBlock, "Voting ended");
    require(!prop.hasVoted[msg.sender], "Already voted");

    // FORMALLY VERIFIED: the balance at prop.snapshotBlock is read, never the live
    // balance, so a transfer after that block cannot change the tally. The snapshot
    // is recorded when the proposal is created, which is the one block in which a
    // flash loan has to be on the books for the attack to work.
    uint256 votes = governanceToken.balanceOfAt(msg.sender, prop.snapshotBlock);
    require(votes > 0, "No voting weight");

    prop.hasVoted[msg.sender] = true;
    if (support) {
        prop.forVotes += votes;
    } else {
        prop.againstVotes += votes;
    }
}

The contract is written for this post; its snapshot-vote shape is the one Compound's Governor contracts established, and the exploit it leaves open is the one that took Beanstalk Farms for $182 million in April 2022, when a single-block flash loan bought a majority of Stalk (Merkle Science).

An auditor evaluating this contract sees that the specification itself is missing an invariant: voting power must be locked or time-weighted (veTokens), so that weight assembled for a single block cannot decide a proposal. The remedy has a canonical implementation in Curve's vote escrow, which replaces one-token-one-vote with a weighting system built on locked tokens.

Two Cases from Zero-Knowledge Audits

The same gap appears in zero-knowledge systems, where the thing under verification is a circuit or a proof system rather than a Solidity contract.

The lessons here are blunter than the reports that carry them. A proof assistant certifies the step from a statement to its conclusion and nothing beyond it: a vacuous or misstated theorem passes the kernel while establishing nothing, so what was proven belongs in the trusted base right beside the machinery that checks it. A proof is tied to the code only through the interface between the theorems and the constraints extracted from it; without that tie, the proof holds for a model that differs from what runs.

Two recent cases show that boundary from the inside:

• The first is what a proof covers. Kolozyan et al. (2026) put the vacuity case on the record and add a second assumption of the same kind: OpenVM's constraint-correctness proofs take for granted the soundness of the lookup argument that ties its chips together.
• The second is zkSecurity's OpenVM 2.0 audit, run in four phases between March 27 and June 9, 2026 (zkSecurity, 2026). It produced four high-severity findings, eight medium, thirteen low, thirteen informational and one known issue. One high-severity example: the host verifier did not verify the deferral Merkle proofs when the deferral flag was zero. One informational finding is titled "Formal-Verification Theorems Do Not Assume a Uniform Extraction-Derived Constraint Interface," which names the interface gap outright. The report also records the opposite failure. In the multi-block SHA-2 circuit, a hash column is never constrained to equal final_hash. Several reviewers "each re-derived" this and "briefly read it as a soundness gap before seeing that final_hash is what is authenticated downstream." The report's lesson: "an unconstrained-looking column can be intentional communication slack rather than an under-constraint." A solver flags what looks unconstrained, but only someone who knows the design intent can say whether it matters.

One more incident landed on the same seam after those reports. On 24 September, an attacker drained $1.92 million from Payy's bridge with a burn proof that was invalid and that the deployed Noir/Barretenberg verifier accepted anyway. The circuit was fine; the verifier's zero-knowledge path carried a small-subgroup IPA soundness bug that Aztec had fixed in May and shipped in July without telling Payy, whose pinned build predated the fix. The settlement contract took the proof's word for note validity and never checked the burn hash itself, which made the failure payable straight from rollup reserves (Payy, 2026).

What makes the Payy case worth dwelling on is what the audits covered. The team commissioned three independent reviews of its core rollup as the system evolved: KALOS in February 2024, AuditOne in November 2024, and Spearbit/Cantina Managed in July 2025, which closed thirteen findings and left two acknowledged. All three examined Payy's circuits and rollup contracts, and the analysis of the exploit is itself Spearbit-supported. The failure was in neither: it sat one layer down, in a verifier written and maintained by someone else (Payy, 2026).

The same period shows the human path working. In June 2026 an independent researcher, loopghost, responsibly disclosed a separate critical bug in the agg_agg circuit, where the unused tail of the messages array went unchecked, letting a prover append a forged burn after a block's real messages and have the rollup pay it out (GHSA-fhxc-63vg-9gwr). The allowlisted prover kept an unprivileged caller off that route, and the advisory is explicit that this is a deployment gate rather than a repair: under the staked-prover model described in Payy's whitepaper the bug becomes permissionless, with $3.4 million of rollup USDC in reach. Payy patched it in v1.3.0, and loopghost followed the disclosure with an independent audit of the infrastructure, circuits, and Ethereum contracts (Payy, 2026).

The Broken Closed-World Assumption: Composability

Traditional formal verification relies on a closed-world assumption: the system's boundary encompasses the contract and a formalized model of its immediate environment. In decentralized finance, this assumption rarely holds. Smart contracts operate within an open, permissionless, composable financial layer:

• External calls to untrusted interfaces. An audited lending pool queries an automated market maker (AMM) pool for asset pricing.
• Unmodeled external state changes. While the lending pool's internal state machine remains valid, an external actor alters the AMM pool's reserves within the same transaction, modifying the returned price.
• Read-only reentrancy. A contract calls an external pool during a state transition. While the target pool prevents state mutation during the call, its transient view functions return out-of-sync values. A third, uninvolved protocol relies on that view function, reading compromised valuations.

When formal verification models the external call by havocking the callee's storage, as the Certora Prover does for unresolved calls (Certora, 2024), it faces an immediate trade-off:

1. If the tool assumes an external call can mutate any state in any contract, the solver loses all context, leading to invariant failures on valid code.
2. If the tool assumes external calls cannot modify specific variables, it misses reentrancy vulnerabilities and cross-contract state manipulations.

The auditor bridges this gap, constructing environment models and composability harnesses that represent external protocol dynamics accurately without causing solver timeouts.

Low-Level EVM Quirks and Compiler Vulnerabilities

Formal verification frequently abstracts low-level execution semantics to keep verification tractable, especially for small pieces of code such as smart contracts. In doing so, it can miss vulnerabilities rooted in the physical realities of the EVM:

• Dirty storage bits and memory packing. When types smaller than 256 bits (uint128, bool) are packed into a single storage slot, bitwise masks isolate each variable. High-level formal models treat variables as discrete mathematical values, missing bugs caused by dirty memory allocations, improper bit-masking, or assembly-level storage aliasing.
• Calldata decoding and ABI deserialization. The standard ABI decoder makes specific assumptions about padding, memory expansion, and trailing bytes. High-level verifiers typically assume that inputs to public functions match their high-level types. Exploits using calldata injection, non-standard zero-padding, or malformed dynamic arrays bypass high-level models entirely.
• Compiler miscompilations. Solidity's optimizing compiler (solc) is a complex program with a documented history of miscompilation bugs, particularly within the Yul IR-based optimizer pipeline; its own bug list records security-relevant defects back to version 0.3.0, rated by severity and tagged with the pipeline each one hits. Three years of differential fuzzing turned up 25 miscompilation bugs that had gone unnoticed, some for years, and the study's own account of the mechanism is blunt: "In our experience, miscompilations occur due to two main reasons: incorrect optimization and incorrect translation" (Shastry, 2026). If a formal tool verifies high-level Solidity source rather than deployed bytecode, it assumes the compiler is in its trusted computing base. If the optimizer introduces a flaw during assembly generation, the verification report is invalid.

Bytecode-level provers and decompilation pipelines mitigate these risks, but auditors must stay vigilant about discrepancies between high-level specifications and low-level bytecode execution.

The Prover's Own Stack

The kernel is where a proof assistant's chain of trust ends, and in August 2026 it moved. A model hunting soundness bugs in the official Lean kernel found several, exploited each one to make the kernel accept a proof of False, and then broke the runtime underneath, where a reference-counter overflow and a stale GMP build were each enough on their own. Lean shipped fixes in v4.33.1 (de Moura, 2026).

What makes the case worth its own heading is where the failures sat. The subsections above all fail above the tooling: a specification that says the wrong thing, a model that diverges from the code, an environment nobody modelled. This one fails inside the checker and the arithmetic library beneath it. A verified kernel is not immune to bugs in the runtime it sits on, and neither is any theorem proved with it. The Lean team's answer is a practice argument rather than a logic one, which is where the workflow section picks it up.

06 The Verification-Augmented Workflow

As formal verification tools have matured, the auditor's workflow has evolved from an ad-hoc review into an integrated, five-phase verification pipeline.

Phase 1: Architectural Deconstruction and Mathematical Modeling

The audit begins before reading Solidity code. The auditor's first deliverable is a formal model of the protocol's state machine:

• What are the core state variables that define protocol health?
• What are the valid initialization states ($S_0$)?
• What external dependencies exist (tokens, price feeds, AMMs, cross-chain bridges)?
• What are the access control permissions across each state transition?

The auditor produces state-transition diagrams and mathematical definitions of the protocol's mechanics, such as constant product invariants, liquidation curves, and debt accumulation ratios.

Phase 2: Formal Invariant Elicitation and Specification Engineering

Here the auditor translates abstract security guarantees into machine-verifiable specifications. This is the most demanding step of the audit, and the auditor organizes invariants into a multi-tiered hierarchy:

1. State invariants (safety properties). Conditions that must hold across all execution states, for example $\forall s\in S_{\text{reachable}},\Sigma \text{balances}\left[i\right]\le \text{totalAssets}$.
2. Transactional transitions (pre- and postconditions). Guarantees governing individual function calls, for example $\left\{\text{balanceOf}\right(u)=b\}\text{withdraw}\left(a\right)\left\{\text{balanceOf}\right(u)=b-a\}$.
3. Access-control boundaries. Mathematical guarantees that sensitive transitions cannot be triggered by unauthorized actors, regardless of caller arguments.
4. Economic invariants. Resistance to arbitrage exploits, price-manipulation resilience, and solvency bounds under liquidation cascades.

The auditor codifies these properties in formal specification frameworks like CVL, Halmos, or Kani.

Phase 3: Automated Verification Triage and Counterexample Analysis

With specifications defined, the auditor runs automated verification engines against the target contracts. A run yields one of three outcomes:

• The proof discharges successfully. The property holds across all execution paths within the configured bounds. The auditor documents the verified invariant and its environmental assumptions.
• The engine times out. The contract logic triggered a solver bottleneck (non-linear arithmetic, complex loops). The auditor refactors the specification, supplies intermediate auxiliary invariants, or abstracts computationally intractable operations, such as substituting uninterpreted functions for hash operations, which buys speed with the soundness caveat noted earlier.
• The engine generates a counterexample. The engine identifies a path that breaks the invariant.

When a counterexample turns up, the auditor analyzes the execution trace:

====================== SMT SOLVER COUNTEREXAMPLE ======================
Violated Invariant: seized_collateral_le_borrower_collateral
Function: liquidateBorrow(address borrower, address collateralAsset)
Call Sequence:
  Step 0: Initial State
    borrower.collateral = 100 ether
    borrower.borrowedDebt = 80 ether
    oracle.getPrice(collateralAsset) = 1.0 ether
    (Health Factor: 1.25 -> Solvent)
  Step 1: Environment Change
    oracle.setReportedPrice(0.79 ether)
    (Health Factor: 0.9875 -> Eligible for Liquidation)
  Step 2: Attacker Action -> liquidateBorrow(...)
    liquidator.repayAmount = 80 ether
    seizedCollateral = 105 ether  <-- EXPLOIT: the seizure exceeds the borrower's collateral
Post-State:
    borrower.collateral = 0 ether (unchecked subtraction saturates at zero, no revert)
    liquidator.receivedCollateral = 105 ether
    Assertion Violation: seizedCollateral (105 ether) > collateralOf(borrower) (100 ether)
    Protocol Incurred Bad Debt = 5 ether
=======================================================================

The trace is written for this post; it takes the shape a prover's counterexample report has, a numbered call sequence, the state each step leaves behind, and the assertion that fails, as in the Certora Prover's call-trace reports.

The auditor isolates the vulnerability: the liquidation routine let the liquidator seize collateral exceeding the borrower's deposit, with no upper-bound check against borrower.collateral. The auditor drafts the mitigation and verifies that the patch resolves the counterexample without introducing regressions.

Phase 4: Adversarial Red-Teaming and Composability Auditing

Once all internal invariants are verified, the auditor turns to the areas where automated tools cannot operate effectively:

• Cross-contract composability modeling. Simulating interactions between the protocol and third-party DeFi infrastructure such as Uniswap pools, Aave lending markets, and Curve swaps.
• Oracle manipulation stress-testing. Evaluating how the system handles stale prices, L2 sequencer downtime, low-liquidity spikes, and multi-block MEV price manipulation.
• Flash-loan attack scenarios. Simulating single-block borrowing attacks against governance mechanisms, liquidation logic, and reward distribution formulas (Qin et al., 2020).
• Privileged roles and key management. Auditing timelocks, multisig configurations, and upgradeability patterns to identify administrative centralization risks.

Protocol teams have started to buy this work competitively. Aave ran a formal verification contest over GHO with a $40,000 pool split roughly 55/35/10 across real bugs, injected bugs, and participation, and sharing in the participation pool required a CVL specification that passed on the original code and failed on the published mutants (Certora). Uniswap's v4 periphery contest set aside $100,000 for the verification half of its pool, weighted 70% toward properties that caught private mutants, 20% to real bugs, 10% to participation. The metric is coverage rather than bug count, which is the point: mutants measure whether a property is strong enough to be worth keeping.

Certora runs the adversarial half on its own account. Capture the Funds paid contestants to extract value from a six-protocol DeFi ecosystem rather than to write properties, and scored exploits in ETH, so a clean chain of them and a lucky one landed at different heights; the Endless CTF relaunch keeps a standing prize for anyone who beats its target score by 25 ETH (Certora). The formats price different things: the contests pay for properties nobody thought to write, the CTF pays for assumptions nobody thought to attack.

Phase 5: Continuous Assurance and Runtime Invariant Monitoring

In modern security practice, the audit report is not the end of the engagement. The auditor delivers the verification suite as a permanent component of the protocol's development infrastructure:

• CI/CD verification suites. Proof harnesses run automatically alongside unit tests on every pull request, preventing regressions as new code is introduced.
• Proof-carrying code. For immutable protocols, mathematical proof certificates are published alongside contract source code and bytecode, letting users and institutional allocators independently verify protocol correctness.
• Runtime invariant monitoring. Invariants developed during formal verification are compiled into active on-chain monitors using frameworks like Forta, Drosera, or OpenZeppelin Defender. If an unexpected state occurs on mainnet, these detection bots pause contracts or initiate defensive withdrawals before exploits can finalize.

The reason to keep proofs in CI is that they decay otherwise. Kolozyan et al. (2026) note that verification is often done by external contractors while zkVMs ship several releases a year, so several published efforts now target deprecated code. Their summary: "Guarantees not checked on every commit silently decay," and AI-generated proofs remain a poor fit for CI. They add that specifications should be reusable, versioned, machine-checkable, and co-owned by those defining protocol intent and those assessing security.

The Lean project's answer to the same problem is worth copying. After a model-driven hunt found soundness bugs in its kernel and runtime, the remedy was not a better kernel but redundant checking: proofs are exported and rechecked by independent kernels (nanoda, ind-models, lean4lean) and by comparator, with lake check folding that into the build and a paranoid mode running every checker the distribution ships. Its author is explicit that the threat model includes the tooling: "We consider AI-generated proofs a potential source of malicious proofs," which is the assumption such a pipeline is built for (de Moura, 2026).

Set against the four-pillar stack that Zero-Day Defense traces — harden, watch, contain, patch — a verification suite lands squarely on hardening, and the artifacts it leaves in production reach into the pillars beside it: the monitors are the watching, and the pause-and-withdraw actions they trigger are the containment.

07 The Auditor's Role and Economics

With the technology in place, the remaining question is what happens to the people and the business around it. What follows compares the old and new audit models, then turns to what practitioners say, how engagements are priced, what skills the work now demands, and who carries liability when a verified protocol still fails.

The business is real, though hard to size. Vendor forecasts put the audit-services market near $1.5 billion in 2025 and $5 billion by 2035 (WiseGuyReports); the counts coming out of academic work are firmer, and the largest study of the market tracks nearly 10,000 audit reports from more than a hundred firms and bounty programs across protocols launched between 2020 and 2025, a field that grew from a handful of auditors in 2020 to over a hundred by August 2025 (Landsman et al., 2025).

Traditional Versus Verification-Augmented Auditing

The table below contrasts the historic manual audit model (2016–2022) with the verification-augmented methodology (2024–2026) across these dimensions.

How Practitioners See the Gap

The comparison above is about tools. Practitioners describe the same gap from experience: in a survey of 48 zero-knowledge developers and auditors, 72% named underconstrained circuits as hard to detect manually, yet 70% considered them adequately covered by current tools. Proof-system bugs scored 60% on difficulty and 15% on tool coverage (Kolozyan et al., 2026). Respondents rated LLMs highly for bounded tasks such as validating findings and writing proofs of concept, and trusted them far less for circuit- and proof-system-level reasoning. The authors' reading is that LLMs can propose specifications, invariants and proof scripts, while independent analyzers, proof kernels and expert review decide which outputs count as assurance evidence.

The audit firms that sell verification describe the same division of labor. Sherlock frames the shift as one of evidence.

Formal verification "shifts the security dialogue from 'we did not find vulnerabilities' to 'we have proven that these specific vulnerabilities cannot exist within the defined parameters'" (Sherlock, 2026).

Sherlock adds that formal verification "is not a replacement for other audit techniques but a complementary, deep-analysis phase" (Sherlock, 2026). Certora's white paper puts the handoff in terms of specifications.

"Manual audits can help specify or identify missing rules in formal verification while formal verification can identify corner cases missed by manual audits, especially when code is continuously modified over time" (Certora, n.d.).

Nethermind Security draws the line the same way, and names what falls on its side of it.

Nethermind Security applies formal verification to zero-knowledge circuits, cryptographic components, protocol logic, and execution infrastructure, providing machine-checked assurance for critical properties that testing and audits alone cannot exhaustively cover (Nethermind Security, 2026).

All three, in other words, keep the auditor on the specification side of the proof.

The Collapse of the "Per-Line-of-Code" Billing Model

The wide availability of formal verification is restructuring the security industry, and the first thing to give is how audits are priced. For years, security firms billed clients by lines of code and duration (David et al., 2023; Chaliasos et al., 2023): a protocol with 2,000 lines of Solidity was quoted for two auditors over two weeks. Pricing by the line and the week is disintegrating:

• Automated auditing tools. Advanced AI scanners and automated formal tools can analyze simple smart contracts in minutes, finding basic implementation bugs faster and more cheaply than human auditors.
• Value realignment. Charging for manual inspections of standard ERC-20, ERC-721, or standard vault patterns is no longer viable. Clients expect automated verification of standard components out of the box.
• Shift to retainers and proof engineering. High-value security firms now operate as assurance partners. Engagements center on specification authoring, proof maintenance, complex DeFi composability modeling, and economic security architecture.

Read as a stylized picture, the effect on an engagement budget looks like this:

The New Profile of the Security Auditor

The shift from inspection to specification changes the skills firms look for in a researcher:

• From syntax reviewer to applied mathematician. In addition to understanding EVM opcodes and Solidity quirks, modern auditors must be comfortable with formal logic: propositional calculus, first-order logic, Hoare triples, weakest precondition calculus, and temporal logic (LTL/CTL).
• Fluency in specification languages. Top auditors write fluent CVL (Certora), Lean 4, Dafny, and Rust verification harnesses (Kani/Verus).
• Economic mechanism modeling. Because automation increasingly catches implementation bugs, the most valuable human skill is identifying economic exploits: game-theoretic incentives, oracle manipulation dynamics, MEV vulnerabilities, and governance attack vectors.

Firms that rely entirely on manual review look set to lose on coverage and cost, while teams that combine formal methods with deep adversarial intuition are where the standard is heading. The pressure is visible in Trail of Bits' own accounting of the Miden engagement: the LSP server, decompiler, static analysis engine and Lean model were all work it says it "wouldn't have been able to dedicate time or resources to just one or two years ago," and agents changed that calculus: "a failed side project only costs tokens" (Trail of Bits, 2026).

The Legal and Liability Reconfiguration

The maturation of formal verification is also changing the legal dynamics of Web3 security in three ways:

• The erosion of "as-is" disclaimers. Traditional audit reports carried sweeping liability disclaimers stating that an audit does not guarantee security or code correctness. Formal verification cannot prevent unmodeled economic flaws, but it provides reproducible, mathematically checkable proof certificates.
• Institutional due diligence standards. We're starting to see institutional allocators, liquidity providers, and insurance underwriters ask for formal verification of core protocol invariants before deployment, though it is not yet standard practice. Where they do, a PDF audit report is not enough on its own: the ask is a machine-checked proof repository wired into the protocol codebase.
• The legal definition of software due care. Where a protocol loses capital to an access-control flaw or rounding bug that a standard SMT-based bounded model checker would have caught, the gap between what was checkable and what was checked is the kind of question that eventually reaches a court. No one has litigated it yet, but the direction looks one way: verification is drifting from an optional luxury toward an operational baseline.

None of this has arrived yet, and the timetable is not the one the tooling keeps. Protocols are still judged by audit reports, liability still turns on the disclaimers those reports carry, and the changes above will be litigated, legislated and priced over years rather than releases.

Read this section as the direction of travel, not the current rulebook.

08 Conclusions

The emergence of practical formal verification does not mark the end of the smart contract auditor. It marks the end of their historical role as a manual, fallible bug hunter, and it changes what a clean audit means: from "reviewers found nothing" to "these properties hold in every reachable state, and here is the specification they were checked against."

The previous era of blockchain security was defined by an unavoidable mismatch: human developers wrote complex, high-value code, and human auditors spent brief windows of time guessing where that code might fail. The inevitable result was billions of dollars in losses from overlooked bugs.

Formal verification changes the foundation of smart contract security. Automated engines can now prove that, within a modeled state space, specific classes of implementation flaws are mathematically impossible. They explore millions of execution paths, discharge thousands of verification obligations, and generate concrete exploit sequences whenever a property is broken.

That foundation frees the auditor to focus on the most valuable work. Freed from hunting for integer overflows and syntax errors, auditors can concentrate on systemic architecture, economic mechanisms, and the boundary where human intent is translated into formal mathematics.

Three practical consequences follow from the argument of this post:

• Ask for the specification, not the stamp. An audit report should ship the invariants, the proofs, and the assumptions each proof rests on, so a reader can see what was covered and what was not.
• Price specification effort, not lines. Proof engineering scales with the complexity of the properties, which is why the per-line billing model no longer tracks the effort involved.
• Keep people on the boundaries. The governance exploit, the composability failures, and the low-level EVM quirks covered earlier all sit outside what a prover checks, and that is where auditor hours now buy the most.

Euler Finance shows the shift. A missing collateral check in a donation routine is the kind of flaw an invariant on account health is built to catch, so the next Euler is more likely to sit in a property nobody thought to write down. Finding that property is the job that remains.

The future of decentralized finance will be secured by neither manual code review alone nor automated proof engines operating without human context, but by a new equilibrium: mathematically rigorous verification engines confirming invariants across every possible state, guided by adversarial security architects who ensure those invariants reflect the messy, composable, and adversarial reality of decentralized systems.

DeFi is a microcosm, and in some respects a leading indicator. It put large sums behind immutable code, exposed every function to a global adversary, and made the cost of a missed assumption visible within minutes, so pressures that reach other software as slow regulatory complaints arrive here as drained pools. What holds up under that pressure should travel: proofs where the property can be modelled, adversarial reasoning where it cannot, and disclosure that says what was checked rather than what was reviewed. Software security is drifting toward the same stakes, and the sequence this field is running is the part to watch: tooling first, then process, then liability.

References

• Amani, S., Bégel, M., Bortin, M., & Staples, M. (2018). "Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL." Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 66–77.
• Annenkov, D., Milo, M., & Spitters, B. (2020). "ConCert: A Smart Contract Certification Framework in Coq." Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 215–228.
• Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., & Zanella-Béguelin, S. (2016). "Formal Verification of Smart Contracts: Short Paper." Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS 2016), pp. 91–96.
• Cassez, F., Fuller, J., Ghale, M. K., Pearce, D. J., & Anton Quiles, H. M. (2023). "Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny." Formal Methods (FM 2023), Lecture Notes in Computer Science, Vol. 14000, Springer, pp. 571–583.
• Certora (n.d.). "Certora Technology White Paper." Available at: docs.certora.com/en/latest/docs/whitepaper
• Certora (2023). "ERC4626 Workshop: Specifications for the Certora Workshop on ERC4626 at TrustX Istanbul." Available at: github.com/Certora/ERC4626_Workshop
• Certora (2024). "Certora Prover Documentation and CVL Reference Guide." Available at: docs.certora.com
• Certora (2025). "Certora AI Composer: The First Safe AI Coding Platform." Certora Blog. Available at: certora.com/blog/certora-ai-composer-first-safe-ai-coding-platform
• Certora (2026a). "AutoProver: Agentic Formal Verification for Every Developer." Certora Blog. Available at: certora.com/blog/autoprover-agentic-formal-verification
• Hajdu, Á., & Jovanović, D. (2020). "solc-verify: A Modular Verifier for Solidity Smart Contracts." Verified Software: Theories, Tools, and Experiments (VSTTE 2019), Springer, pp. 161–179.
• Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Yi, S., Denisiuk, C., & Roşu, G. (2018). "KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine." IEEE 31st Computer Security Foundations Symposium (CSF 2018), pp. 204–217.
• Nethermind Formal Verification Team (2025). "EVMYulLean: Executable Formal Model of the EVM and Yul in Lean 4." Nethermind Security Research.
• Park, D., Zhang, Y., Saxena, M., Daian, P., & Roşu, G. (2018). "A Formal Verification Tool for Ethereum VM Bytecode." Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2018), pp. 912–915.
• Schneidewind, C., Grishchenko, I., Scherer, M., & Maffei, M. (2020). "eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts." Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS 2020). Available at: arxiv.org/abs/2005.06227
• So, S., Lee, M., Park, J., Lee, H., & Oh, H. (2020). "VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts." 2020 IEEE Symposium on Security and Privacy (S&P 2020), pp. 1678–1694.
• Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Buenzli, F., & Vechev, M. (2018). "Securify: Practical Security Analysis of Smart Contracts." Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 67–82.

• Chaliasos, S., Charalambous, M. A., Zhou, L., Galanopoulou, R., Gervais, A., Mitropoulos, D., & Livshits, B. (2023). "Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?" arXiv:2304.02981. Available at: arxiv.org/abs/2304.02981
• Chaliasos, S., Ernstberger, J., Theodore, D., Wong, D., Jahanara, M., & Livshits, B. (2024). "SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs." arXiv:2402.15293. Available at: arxiv.org/abs/2402.15293
• David, I., Zhou, L., Qin, K., Song, D., Cavallaro, L., & Gervais, A. (2023). "Do You Still Need a Manual Smart Contract Audit?" arXiv:2306.12338. Available at: arxiv.org/abs/2306.12338
• Feist, J., Grieco, G., & Groce, A. (2019). "Slither: A Static Analysis Framework for Smart Contracts." IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB 2019), pp. 8–15.
• Grieco, G., Song, W., Cygan, A., Feist, J., & Groce, A. (2020). "Echidna: Effective, Usable, and Fast Fuzzing for Smart Contracts." Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2020), pp. 557–560.
• Kolozyan, A., Sorger, T., Hicks, A., & Chaliasos, S. (2026). "ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges." arXiv:2607.23752. Available at: arxiv.org/abs/2607.23752
• Landsman, W., Lyandres, E., Maydew, E., Rabetti, D., & Zhang, C. (2025). "Auditing Smart Contracts." Working paper, University of North Carolina, Tel Aviv University, National University of Singapore, and Tsinghua University. Available at: accounting.wharton.upenn.edu/uploads/LandsmanLyandresMaydewRabettiZhang.pdf
• Mueller, B. (2018). "Smashing Ethereum Smart Contracts for Fun and Real Profit (Mythril)." Black Hat USA.
• Nikolić, I., Kolluri, A., Sergey, I., Saxena, P., & Hobor, A. (2018). "Finding the Greedy, Prodigal, and Suicidal Contracts at Scale." Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 653–667.
• Novak, S., & Kovacs, N. (2025). "Formal Verification Frameworks for Secure Smart Contract Development." Blockchain, Web3 & Digital Trust Journal, 2(1), pp. 37–44. Available at: galaxiauniverse.com/index.php/BWDTJ/article/view/446
• Qin, K., Zhou, L., Livshits, B., & Gervais, A. (2020). "Attacking the DeFi Ecosystem with Flash Loans for Fun and Profit." arXiv:2003.03810. Available at: arxiv.org/abs/2003.03810
• Shastry, B. (2026). "Finding and Understanding Miscompilation Bugs in the Solidity Compiler." arXiv:2607.07217. Available at: arxiv.org/abs/2607.07217

• Braghin, C., Riccobene, E., & Valentini, S. (2023). "Towards the Automated Verification of Smart Contracts." Università degli Studi di Milano Research Report.
• CertiK (2023a). "What is Formal Verification in Smart Contract Auditing?" CertiK Technical Insights.
• CertiK (2023b). "Euler Finance Incident Analysis." CertiK Blog. Available at: certik.com/blog/euler-finance-incident-analysis
• Certora (2026b). "Security Reports." GitHub repository of public audit and formal verification reports. Available at: github.com/Certora/SecurityReports
• Lazaropoulos, L., & Paraskevopoulou, Z. (2026). "Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens." Argot Collective & National Technical University of Athens. Available at: arxiv.org/abs/2607.26306
• de Moura, L. (2026). "Postmortem for the Kernel Soundness Bug Hunt." Available at: leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt
• Mota, A., Yang, F., & Teixeira, C. (2023). "Formally Verifying a Real World Smart Contract." arXiv:2307.02325. Available at: arxiv.org/abs/2307.02325
• Nethermind Security (2026). "Formal Verification for High-Stakes Blockchain and Zero-Knowledge Systems." Available at: nethermind.io/formal-verification
• OtterSec (2023). "Solana Formal Verification: A Case Study." Available at: osec.io/blog/formally-verifying-solana-programs
• Payy (2026). "Payy USDC Withdrawal Exploit Postmortem." Available at: polybase.notion.site/Payy-USDC-withdrawal-exploit-postmortem
• Pusceddu, D., & Bartoletti, M. (2024). "Formalizing Automated Market Makers in the Lean 4 Theorem Prover." 5th International Workshop on Formal Methods for Blockchains (FMBC 2024), OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl. Available at: drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.5
• Sherlock (2026). "What is Formal Verification?" Sherlock Blog. Available at: sherlock.xyz/post/what-is-formal-verification
• Trail of Bits (2026). "Auditing in the Age of (Good Enough) AI." The Trail of Bits Blog, September 18. Available at: blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai
• Zhang, B., Liu, H., Tian, Q., Chen, S., Wang, Z., & Qi, Q. (2026). "Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification." Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (ACL 2026), pp. 39548–39582. Available at: aclanthology.org/2026.acl-long.1836
• zkSecurity (2026). "OpenVM 2.0 Audit Report." Audit of Axiom's OpenVM 2.0, March 27–June 9, 2026. Available at: reports.zksecurity.xyz/reports/openvm