.svg){kind=icon}
Now hiring!
Formal verification is usually framed as a security methodology, which obscures the decision actually facing the teams that fund it. The question is economic: at what point does proving a system correct cost less than carrying the uncertainty of not having done so?
For most software the honest answer is that it does not. Formal verification is valuable in fewer places than its advocates assume, and in more than its critics allow. The more interesting question is where the economics change.
We build machine-checked proofs for zero-knowledge (ZK) systems, so our view is not disinterested. It is also shaped by where Ethereum is heading. As execution moves to rollups and the base layer increasingly records only succinct validity proofs of state transitions, a growing share of what matters sits at the infrastructure layer, where formal verification has always been most defensible.
Balancer was exploited for roughly $128 million on November 3, 2025, despite formal verification work on parts of the protocol. Around 80% of last year's losses originated in offchain components, such as compromised keys and social engineering, that no code-level proof would address. Fuzzing finds large numbers of bugs quickly and at a fraction of the cost, and rigorous smart contract auditing, manual review combined with AI-assisted detection, catches the issues that matter in most application code. The strongest auditors reach for formal methods selectively, where the stakes justify the effort. Read together, those observations point to a narrower conclusion than the usual one: formal verification is not the right default everywhere, but the places where it earns its cost reach well past infrastructure, into the high-value contracts and invariants that secure the most capital.
Yet those observations do not describe every layer of the stack equally well. Formal verification is not a general security mechanism, and it is not economical in most contexts. It becomes increasingly attractive at the infrastructure layer, where the consequences of failure are larger and correctness assumptions propagate outward through the systems that depend on them. Those conditions increasingly describe the proving systems, virtual machines, and cryptographic primitives that the rest of the ecosystem treats as trusted.
When we formally verify a system, we prove that its implementation satisfies a specification, a precise mathematical description of the intended behavior. The guarantee is bounded by that specification and nothing more. A program can be verified against a trivial specification, one so weak that it permits every possible behavior, correct and incorrect alike, in which case the proof holds and tells you nothing. The difficult and consequential work is specification engineering: determining which properties actually matter and stating them precisely enough to reason about. The methodology relocates bugs from the implementation to the specification rather than removing the need for judgment.
A claim of "formally verified," offered without saying what was verified and against which specification, therefore carries little information. A proof that a system satisfies 20 stated properties is silent on the 21st that no one wrote down, and the distance between a marketed guarantee and a proven one is where losses tend to occur.
The pattern is visible in our own work. On a DeFi pool protocol we reviewed, the effort of writing down precisely what the system was supposed to do surfaced problems before any proof was attempted: a rounding error, and a configuration in which a particular execution order and set of inputs caused an over-protective reentrancy guard to lock a legitimate staking agent out of the pool. Neither issue came from the proof. Both came from specification engineering, which is where the difficulty and the value concentrate.
The same pattern appears in production cryptography. Cryspen, which maintains formally verified libraries used in work such as Signal's post-quantum transition, has documented that across years of use the bugs that surfaced sat either in the specifications being verified against or in unverified surrounding code, such as platform stubs and API wrappers, while the verified components stayed clean. The lesson is consistent: the guarantee covers exactly what was specified and verified, and the perimeter around it still requires ordinary review and testing.
The cost of being wrong is rising for a structural reason. As Ethereum moves toward rollup-centric scaling and a SNARK-verifiable execution model, more of what happens onchain is recorded as a succinct proof rather than as inspectable transaction data. Once a state-transition proof is accepted its correctness is presumed final, and any error that passes the verification layer becomes effectively irreversible short of social consensus. When the deployed artifact cannot be inspected or amended after the fact, errors have to be excluded before deployment rather than discovered after it. That shifts the economics toward stronger correctness guarantees and increases the value of methods that provide exhaustive assurance.
A flaw in a single application affects that application, whereas a flaw in a proving system, verifier, or virtual machine affects everything that inherits its trust assumptions. Verifiers are especially attractive targets for formal verification because they are comparatively small, public, and systemically important. A proof of verifier correctness therefore yields an unusual amount of assurance per unit of effort. Our formal verification of the honesty of ZKsync's onchain verifier was motivated by exactly that asymmetry.
The same reasoning applies to virtual machines. Our team completed the first known formal verification of the functional correctness of a RISC-V-based zero-knowledge virtual machine (zkVM), and our collaboration with Succinct on SP1 has worked through extracting circuit constraints, writing precise specifications, and proving properties of the arithmetic chips against a formal definition, with full RISC-V coverage as a long-term target rather than a completed claim. The same approach now extends to other zkVMs: we verified the RV32IM extension of OpenVM (Axiom) in Lean, and similar work on Brevis's Pico has been completed.
These are bounded problems with explicit boundaries, which is precisely where proof is most effective. A large application with many interacting components rarely offers a single component whose correctness determines the correctness of the whole, which has historically made full-system proof impractical there. The tractable target is narrower: the specific invariants and high-value components whose failure would be catastrophic. Proving those is moving from impractical toward worthwhile as specification tooling matures. Circuits and virtual machines remain the cleaner case: their boundaries are explicit, their specifications are comparatively stable, and the systems around them inherit their assumptions.
In a recent security update, Aave committed to letting formal verification shape the architecture for all major protocol development. Measured against the fact that most exploits originate offchain, that can look misdirected. The comparison becomes more interesting when viewed through the lens of infrastructure risk. If 15% to 20% of 2025's losses were code-level failures, against total losses of around $3.5 billion, then the software-correctness share alone falls somewhere near $500 million to $700 million in a single year. Amortized over time, that is a recurring cost to the ecosystem in the hundreds of millions annually. Total formal verification spend across Web3 almost certainly does not approach $100 million a year. On the direct dollar figure alone the comparison favors the work, and that is before accounting for trust.
Direct losses are only part of the calculation.
A correctness failure in core infrastructure is interpreted differently from an operational one: losses to social engineering register as human error, while a system that returns the wrong answer erodes confidence in the technology itself. That erosion is felt well beyond the protocol that failed, as slower institutional adoption, higher operational overhead, and a higher risk premium across the sector. Those effects resist precise measurement, and they push the economics further in the same direction.
The limits matter because the guarantee is precise rather than general. Specifications can be wrong, operational infrastructure can be compromised, governance can fail, and side channels can defeat an otherwise correct system. Most of the preconditions for a catastrophic loss sit outside any formal model.
The build and deployment pipeline is the clearest example of a layer that resists these methods. If continuous integration is compromised and code is altered after it is written, a proof about the source in the repository says nothing about the binary that shipped, which is a class of side-channel problem rather than a failure of the proof. Our practice is to bind a proof to a specific binary, so the artifact in use can be checked by hash against the artifact that was verified, which contains the problem without dissolving it. The underlying software stacks were designed decades ago, and some of those constraints are real.
Compliance shifts the calculation again. Institutions that want meaningful exposure to this infrastructure tend to require evidence that is exhaustive, reproducible, and replayable, and formal proofs supply exactly that: the proof of an invariant can be re-checked at any time against an explicit specification rather than resting on the judgment of the last reviewer. A regulator protecting citizens' funds can reasonably ask for the standard of assurance that other critical industries already meet. The harmonization work now underway, including emerging standards for verifying zkVM constraint systems and standardization efforts at bodies such as ISO TC 307, points in this direction.
None of this turns formal verification into a universal safeguard, and it should not be sold as one. Its clearest case today is a narrow band: the cryptographic primitives, ZK circuits, zkVMs, verifiers, and consensus components that everything else trusts by default. There, the problem is bounded, the boundaries are explicit, and the consequences of failure are severe enough that uncertainty is the more expensive option. That band is not the only place the logic holds. The same reasoning is beginning to reach the application layer: as the capital concentrated in individual smart contracts grows and the tools for specifying their critical invariants mature, proving those invariants moves from impractical toward worthwhile. Auditing and continuous testing remain the right baseline for most application code, with formal verification becoming a credible complement for the contracts where the cost of being wrong is highest. As more capital, more settlement, and more cryptographic machinery accumulate at that layer, and as the proof-centric model removes the ability to correct errors after deployment, the threshold at which proving correctness becomes the cheaper option keeps being crossed.
Teams weighing the engineering cost of formal verification for zkVMs or proving systems can start that conversation at nethermind.io/formal-verification.
The Leading Engineers of Blockchain Infrastructure
Nethermind © 2026
.svg)
.svg)
.svg)
.svg)
.svg)
.svg){kind=icon}
.svg)
.svg)
.svg)
.svg)
.svg)