The phrase "the contracts were audited" used to be the end of a security conversation. In modern DeFi it is the start of one. Many of the highest-profile DeFi failures of the last three years occurred in protocols that had already been audited — often by more than one firm, sometimes by the closest thing the industry has to brand reassurance. The audits were not lazy. The auditors were not careless. The exploited paths were rarely textbook reentrancy or arithmetic mistakes that competent reviewers find in the first day. The exploits lived elsewhere: between contracts and oracles, between governance proposals and execution, between the smart account and the approval prompt, between version N and version N+1, and between blockchains that were never designed to share a trust assumption.
The dominant failures in DeFi are no longer local code defects. They are boundary failures. And boundary failures do not respect the unit of review that a smart contract audit naturally produces.
Core claim
- Smart contract audits are necessary, but bounded — they review artifacts under stated scope, not the system that surrounds those artifacts.
- The dominant DeFi failures of recent years live at boundaries: integration assumptions, upgrades, governance actions, off-chain dependencies, cross-chain messaging, and multi-transaction logic.
- These boundaries are exactly where local audit logic stops being sufficient.
- Formal verification matters because it forces these system-level invariants to be written down explicitly and machine-checked.
- Formal verification does not prove the real world safe; it proves an implementation conforms to a specified model under stated assumptions.
- The shift is from security as a pre-launch event to security as a continuous system-boundary discipline.
Audits Remain Necessary, but Become Insufficient at the System Boundary
Smart contract audits remain necessary. They reduce local implementation risk, catch the bug classes a competent reviewer is trained to find, and produce an artifact a protocol team can defend in front of users and integrators. None of that is in dispute. The argument of this piece is narrower and sharper: audits become insufficient the moment protocol safety depends on interactions across contracts, across upgrades, across governance actions, across off-chain systems, across cross-chain systems, or across transaction sequences. At that point the assurance question is no longer "is this contract correct in isolation?" It is "does the system continue to satisfy its invariants as it composes, evolves, and is operated over time?" That is a different property. It needs a different discipline.
What This Article Means by "Boundary Failure"
A boundary failure is a security failure that arises not inside a single contract but at the seam between artifacts the protocol depends on. Six categories are load-bearing for the rest of this article:
- Integration boundary — failures at the interface between two contracts that each assume something about the other (oracle adapters, token wrappers, liquidation routers, external-protocol integrations). Driven by unstated integration assumptions.
- Upgrade boundary — failures introduced when a new version of the protocol breaks an invariant the old version preserved, including patches that fix one issue while opening another. The core concern of upgrade safety.
- Governance boundary — failures whose execution depends on a governance proposal, its parameters, its execution window, and the behavior of the upgrade executor.
- Off-chain boundary — failures that occur in frontends, RPC layers, signing pipelines, or operator infrastructure while the on-chain contracts remain technically correct. The space of off-chain dependencies.
- Cross-chain boundary — failures in bridges, message authentication, finality assumptions, and relayer trust that propagate across chains regardless of the local correctness of either side.
- Temporal / multi-transaction boundary — failures that emerge only across a sequence of transactions whose individual steps look legitimate. The domain of multi-transaction logic and reachable-history reasoning.
These are not exhaustive, but they cover the failure modes that show up repeatedly in postmortems and that audit-only assurance is structurally bad at defending.
Smart Contract Audits Are Snapshots — DeFi Protocols Are Pipelines
A smart contract audit is, by construction, a snapshot. A team of reviewers takes a commit hash, reads it under time and scope constraints, asks questions, files findings, and writes a report. The report describes what the auditors found within their model of the system, under their threat assumptions, against the property set they considered in scope. This is irreplaceable risk reduction when done well, and theater when done poorly. Either way, it is a snapshot of an artifact.
Modern DeFi is not an artifact. It is a delivery pipeline. The contracts are the deployed surface, but they are surrounded by — and entangled with — a governance process, an upgrade executor, a set of off-chain price feeds, token assumptions the protocol cannot enforce, liquidation logic that depends on bots and infrastructure outside the codebase, cross-chain messaging contracts that someone else maintains, frontends and RPC endpoints that the user actually interacts with, and a steady drumbeat of governance proposals that change parameters, deploy patches, and migrate state. The moment value moves through several of these at once, DeFi security stops being a property of one artifact and becomes a property of how those artifacts compose, evolve, and trust each other over time.
Aave's governance proposal for continuous formal verification states this out loud. In a complex system of smart contracts, the team writes, it is hard to ensure that changes introduced via governance are safe and do not break protocol behavior, and manual audits are difficult to apply in ongoing, time-controlled governance settings. That is a protocol-level admission, not a research claim. The delivery model has outrun the assumptions of periodic review.
Three Boundary Classes Where Smart Contract Audits Stop Being Enough
The integration boundary: oracle and interface assumptions
In late 2022, Compound froze its cETH market after a governance-approved price feed upgrade went live. The new oracle had been discussed publicly, audited three times, and ratified through governance. It still bricked the market on day one because the upgrade assumed the cETH token implemented an underlying() method, and cETH does not. The contract did not blow up. Nothing was stolen at that moment. But the price feed returned wrong values, lending and borrowing in cETH had to be paused, and recovery required another governance proposal under a multi-day execution window. Downstream protocols that had built on Compound's cETH market — including structured-product issuers — had to manage the spillover.
The structural failure is straightforward. The bug was not in any single contract. It was at the seam between two contracts that had each been reviewed in isolation. The oracle's specification assumed a behavior of cETH; cETH never agreed to that contract. No audit of the oracle alone could see the missing method on the other side of the integration. No audit of cETH alone would have flagged a future oracle that had not yet been written.
This is the integration boundary. It is the place where two pieces of code communicate through an interface that exists only in the assumptions of the authors. The Compound incident is the canonical example, but the pattern is universal: every oracle adapter, token wrapper, bridging contract, liquidation router, and external-protocol integration is an instance of unstated integration assumptions. A smart contract audit that looks at the code on one side of the boundary, in scope, will produce a clean report while leaving the interface assumption undefended.
The upgrade boundary: regressions, patches, and upgrade safety
In March 2023, Euler lost roughly two hundred million dollars to an attacker who used a function called donateToReserves to push his own account into an unhealthy state, then self-liquidated under conditions that returned a profit. The function had been introduced in a previous patch — a fix for a separate first-depositor issue that prior audits had missed. That patch had itself been audited. The new code did not contain a glaring bug. It contained a missing check: the donation path did not verify the donor's account health, which made it possible to engineer a configuration in which liquidation was profitable for the same actor. The invariant that "no actor can manipulate their own account into a state where they can liquidate themselves for profit" is not the kind of property that lives in a single function. It is a property of the relationship between several functions across reserves, account health, and the liquidation engine.
The Euler exploit is best read not as a bug but as a regression. The security posture of the protocol changed when the protocol changed, and the audit of the change was scoped to the change, not to the invariant the change affected. Patches are the most common source of this regression because patches narrow attention. The reviewer asks "does the new function do what it claims to do?" and rarely "what global property of the protocol is now responsible for ensuring this new path does not interact pathologically with everything else?"
This is the upgrade boundary, and it is structurally identical to the integration boundary except that the other side of the integration is a future version of the same protocol. Aave has moved publicly toward equivalence checking for upgrades — a formal statement that, except for a precisely declared delta, the new version preserves the observable behavior of the old one. Upgrade safety, treated as its own verification problem, is the only way to keep a governed protocol's security posture stable across a long sequence of changes that each, considered alone, looks reasonable.
The off-chain and cross-chain boundary: frontends, bridges, and message authentication
Two failures clarify how far the system extends past the bytecode. The first is KyberSwap's 2022 frontend exploit. The contracts were not touched. The attacker compromised the project's Cloudflare configuration, injected malicious code into the user interface, and persuaded users to approve a hostile address. The smart contracts were exactly as safe as they had been the day before. Users were not. From the system's perspective — and the user's — that distinction was meaningless. Off-chain dependencies are part of the security model whether the assurance documents say so or not.
The second is Nomad's bridge failure in mid-2022. The exploit did not come from any contract behaving incorrectly in isolation. Nomad's own root-cause analysis identifies the cause as a flaw in how the Replica contract authenticated cross-chain messages: the validation logic allowed a forged message to pass through to the BridgeRouter. Once the system-level message authentication property failed, every contract downstream of it inherited the failure. The bridge was not a bag of contracts. It was a message-validation system spanning roots, attestations, timers, and remote execution assumptions. A clean audit of any single component could be entirely accurate and still tell you nothing about whether the property "only authenticated messages execute" actually held end to end.
Frontends are off-chain. Cross-chain messaging is partially off-chain in the sense that it depends on relayers, observers, finality assumptions, and bridge designs that no single audit can fully model. Both failures are reminders that DeFi users do not consume one contract. They consume a pipeline. And the pipeline has surface area that the contract-centered assurance model does not address.
Multi-Transaction Logic and Reachable Histories in DeFi
The pattern beneath these cases is older than DeFi but newer than most security tooling. The serious failures are not single-call vulnerabilities. They are sequences. The attacker enters with capital, often borrowed; stages the protocol's state through a series of transactions, each of which appears legitimate on its own; manipulates a boundary condition — an oracle update, a tick state, a health calculation; triggers the exploit at the exact moment the staged state intersects with the invariant the protocol failed to defend; extracts value; returns the borrowed capital; and exits. The losses are visible in seconds. The setup is not.
KyberSwap Elastic's 2023 exploit is the cleanest illustration. The vulnerability was not a misnamed variable. Kyber's own analysis describes a discrepancy between cross-tick estimation and final price calculation, made worse by rounding, that produced a mismatch between the tick state and the liquidity state along certain swap paths. The exploit was a swap. The dangerous swap was only dangerous because preceding swaps had positioned the pool into the specific configuration that allowed it. Read in isolation, none of the transactions were obviously malicious. Read together, they were the entire attack. Prior smart contract audits had reviewed the code; they had not reviewed the choreography.
This is what makes audit logic insufficient for a growing share of real exploits. The unit of review for a smart contract audit is the function, the contract, occasionally the workflow. The unit of attack is the trace — a sequence of state transitions across the global blockchain state, the protocol's storage, and the protocol's external dependencies. The mismatch is not a tooling gap that better dashboards will close. It is a different kind of property. Recent verification research has begun to name multi-transaction logic directly: tools that center their reasoning on generating transaction sequences which demonstrate flaws, and verification frameworks that explicitly target temporal properties — sequenced behaviors — over expressive subsets of Solidity. The center of gravity for meaningful smart-contract analysis is shifting from proving individual functions to proving reachable histories.
"Reachable histories" is the right primitive for DeFi security. The question is not "can this function be misused in isolation?" but "across all sequences of operations the system actually permits, does the property I claim to defend remain true?" That is also, almost word for word, what formal verification is built for.
Why Formal Verification Is Returning to DeFi Security Now
Formal verification is back in serious conversation not because the field has been rediscovered but because the operational gap has grown large enough that protocols with real money have started funding the work, and the gap is widening fast enough that ad hoc review cannot keep up.
Vitalik Buterin's May 2026 essay pushing formal verification back into the center of protocol discussion is a contextual signal that the topic is overdue, not the argument itself.
Three things changed at once. The first is governance cadence. Mature DeFi protocols are governed; they ship parameter updates, oracle changes, integration upgrades, and risk module rotations on a continuous schedule. Each change is small. The aggregate is a stream. Auditing every change in the depth required to defend system-wide invariants is not feasible in calendar time, and it is not feasible in budget. Aave's response is a continuous formal verification program funded at roughly $1.7 million across six months — not as a pre-launch event but as a permanent function inside the protocol's security posture. That is not a marketing number. It is the price a serious protocol attached to refusing the periodic-audit model. How AI is starting to compress the labor curve behind that cost — and which failure modes AI-assisted verification introduces — is the subject of the third piece in this series.
The second change is that the dominant exploit class is no longer a class a smart contract audit naturally finds. Recent Solidity verification research is direct about this: the majority of real-world losses today stem from business-logic errors rather than common bug patterns. Reentrancy is a solved problem in the sense that competent reviewers and standard tooling catch it; integer arithmetic is mostly solved by the language. The losses come from properties that have to be stated specifically for each protocol — invariants about accounting, about reserve solvency, about parameter constraints, about the interaction between liquidation logic and oracle freshness, about what is preserved across an upgrade. These are the properties formal verification is for. They are also the properties that audits cannot fully address without writing the same specification in a less rigorous medium.
The third change is the maturation of the toolchain and the literature around its limits. Specification languages and verification engines for Solidity are not where their authors want them to be, but they are usable in production for invariant-heavy modules. Compound has separated formal verification from simulation-based economic security in its own documentation — a clarifying move, because not every meaningful property is deductive in the same way. Composable DeFi verification has emerged as its own research line, with explicit modeling of interacting protocols rather than isolated contracts. Temporal verification work is advancing toward the multi-transaction frontier that contemporary exploits actually inhabit.
It is worth being precise about where each piece of this story sits. Smart contract audits and local invariant review are established practice. Continuous formal verification, equivalence checking on upgrades, and protocol-level invariant programs are emerging practice — used in production by a small number of mature protocols, increasingly funded as a permanent line item. Temporal verification, multi-transaction reasoning, and full system-level composition verification remain a research frontier — directionally important, partially usable today, but not yet a turnkey workflow for most teams. Conflating these layers is how the conversation gets sloppy.
What Formal Verification Adds to DeFi Security
The most accurate way to describe formal verification to a protocol team is that it forces explicit invariants. It demands the property be written down in a language a machine can check, and that the proof — or the counterexample — be produced against the model the team has agreed represents the system. The discipline is the value before the tool is.
The most uncomfortable lesson from recent audit-of-audits research is that the natural-language claim a team thought they were verifying often did not match the property the prover actually checked. Analysis of real audit reports has surfaced cases where the public property description and the formal specification diverged in ways that mattered — and where load-bearing assumptions used by the prover never made it into the report at all. That is a specification failure, and specification failures are exactly the failures that audit-centric workflows are structurally bad at catching, because the specification lives mostly in the auditor's head and the protocol team's marketing.
When formal verification is done well, the artifact is not the proof. It is the specification. The specification is a contract between the protocol team and the future: this is what we promise will remain true, here are the assumptions under which the promise holds, here is the model in which it is checked. The proof is the receipt that says the implementation matches. The receipt is valuable. The contract is more valuable.
Formal verification scales, when it scales, by selecting the right targets. The highest-value modules are usually the ones that move value: accounting, solvency, parameter bounds, liquidation logic, upgrade equivalence, interface invariants for tokens and oracles. Trying to verify everything is a doomed project. Verifying the modules where the blast radius is largest, with invariants that hold across upgrades and across compositions, is the operational shape that has actually emerged from production protocols willing to make the investment.
What Formal Verification Does Not Add
A proof is a proof of the modeled system against the stated specification under the assumed environment. It is not a guarantee about the real world. Formal verification did not save KyberSwap's users from a Cloudflare compromise. It could not, on its own, have saved Compound from a governance change that shipped with a wrong interface assumption — the assumption itself would have to be specified, the integration would have to be modeled, and the change would have to be checked against the model before it executed. Even where verification can address a property, the property has to be stated correctly; the environment has to be modeled adequately; the language semantics have to be approximated soundly; and the operator has to understand what kind of witness the tool is actually producing.
Formal verification matters because it narrows specific attack surfaces, makes hidden assumptions explicit, and forces upgrade equivalence into the development process. It does not produce safety. It produces a sharper, more defensible model of what the team has committed to keeping true. That model has to be maintained, extended to new boundaries as the protocol composes outward, and stress-tested against the failure modes it does not yet cover. It is a permanent function, not a deliverable.
I unpack what "verified" actually means — the four-place relation between implementation, specification, environment model, and verifier semantics, and where each of those can quietly break — in the follow-up piece on the proof boundary.
DeFi Security as a System-Boundary Discipline
The shift this article describes is small in words and large in operating consequence. It is the shift from treating DeFi security as something that happens at a moment — the pre-launch audit window, the post-incident response — to treating it as a continuous discipline of stating, proving, and defending invariants across the boundaries the protocol actually depends on. The boundaries are not new. Contracts have always integrated with tokens and oracles and bridges and frontends. The governance process has always been part of the trust assumption. The upgrade path has always been part of the security posture. What changed is that the volume, value, and composition of these interactions have grown to the point that the assurance model can no longer pretend the boundaries are out of scope.
Formal verification is not the only response to this shift. It is the response that takes specification seriously. Other parts of the response — continuous monitoring, simulation-based economic security work, adversarial bot testing, post-execution incident playbooks, governance veto windows, equivalence checks for upgrades — are equally necessary, and the protocols that do them well are the ones whose specifications are clean enough for those tools to do their jobs.
The honest framing for a protocol team in 2026 is this. A smart contract audit is a necessary investment in local correctness, and it will catch the kind of mistakes any production codebase can produce. It will not, by itself, defend the integration boundary, the upgrade boundary, the governance boundary, the off-chain boundary, the cross-chain boundary, or the transaction-sequence boundary. Those are different properties, and they have to be written down before they can be defended. The protocols that have learned this are funding continuous formal verification, equivalence checking on upgrades, and explicit invariant work on the modules that move value. The protocols that have not learned it yet are the ones whose next incident will read like the last one.
Key takeaway
- Smart contract audits review artifacts; modern DeFi fails across boundaries and across transaction histories.
- The expensive failures of the last three years lived at integration, upgrade, governance, off-chain, cross-chain, and multi-transaction boundaries — not inside isolated contracts.
- Formal verification matters because it makes system-level invariants explicit and machine-checkable, not because it proves the real world safe.
- The future of DeFi security is not replacing audits, but extending assurance beyond the contract boundary into upgrade safety, integration assumptions, off-chain dependencies, and reachable-history reasoning.