The economy when agents read, buy and act
$578M in 19 days. Zero code bugs.
The case for multi-protocol formal verification
Source Adapted from $578M in 19 days. Zero code bugs., Paragraph (the Building in Public series), first published ; adapted .
I. The 19-day window
On 1 April 2026, the Drift admin team noticed anomalous activity and queued a privileged-role revocation. The transaction landed. By the time the dust settled, twelve minutes later, ~$285M USDC had been drained from the vault across 31 transactions.
On 18 April, seventeen days later, the KelpDAO restaking adapter on Ethereum minted 116,500 rsETH to a wallet that had locked precisely zero ETH on Unichain. The mint cleared block 24,908,285. By the time the freeze hit, ~$293M had been extracted into Aave and onward.
$578M in 19 days. Two protocols. Two chains. Two completely different failure modes — at least, that's how the public discussions framed it.
I think the public discussions had it exactly backwards. Both incidents had the same root cause. Both contracts had been audited. Both audits were correct. The contracts behaved exactly as their specifications required. What broke wasn't any single contract — what broke was the assumption each contract made about the others around it. And single-contract auditing, however thorough, cannot detect that class of failure by definition.
This essay walks through both incidents, shows the cross-protocol formal verification we used to reproduce them as model-checker counterexamples, and explains why this verification class catches what audits miss.
II. Two incidents, two protocols, one pattern
Kelp, 18 April
KelpDAO is a liquid restaking protocol. The contract at the centre of the incident, KelpAdapter, lives on Ethereum. Its job: when a user locks ETH on Unichain, mint a corresponding amount of rsETH on Ethereum.
To know whether a Unichain lock has occurred, the adapter relies on two upstream signals. A LayerZero DVN — a configured set of signers — attests that the lock event is real. An RPC node operator confirms that the underlying chain state matches. Both are single points of trust. Neither is enforced by the adapter contract; the adapter only checks that the message was signed by the configured DVN and that the configured RPC returned a positive observation.
On April 18, an adversary compromised both. A signed LayerZero message claimed a Unichain lock had occurred. The compromised RPC corroborated. The adapter, finding both signatures valid against its locally-configured trust roots, minted 116,500 rsETH to the attacker on Ethereum. Zero ETH had actually been locked on Unichain.
The KelpAdapter behaved exactly as its specification required. The DVN behaved exactly as its specification required. The RPCNode behaved exactly as its specification required. What broke was a property that lives across three protocols simultaneously: destination-chain supply must equal source-chain locks. No single contract enforces this, and a single-contract audit cannot express it.
Drift, 1 April
Drift is a Solana-native perpetuals DEX. The vault holds collateral for open positions; the market gates which collateral types can back which positions; the admin role can update the whitelist of collateral tokens.
On April 1, the Drift admin team queued a routine admin revocation. The 2-of-5 multisig collected approvals. The timelock enqueued. The revocation landed at slot S. By any single-contract reasoning, post-revocation the admin role had no privileged powers.
The attacker had spent the prior days preparing a transaction signed against a Solana durable nonce account. Solana's durable-nonce semantics are precise: a transaction signed against a Nonce account at slot S0 remains valid until the nonce is consumed, regardless of any state change between S0 and consumption. The attacker's pre-signed transaction added a fake CVT (collateral value token) to Drift's market whitelist.
Within the four-slot window after the revocation transaction landed, downstream consumers had not yet observed admin_active=FALSE. The market gating logic checked admin status against a stale view, found it satisfied, and admitted the add_cvt operation. The fake CVT was now whitelisted. A subsequent redeem transaction drained the vault: ~$285M USDC over 31 transactions in 12 minutes. Liquidations cascaded into Raydium pools.
The bug class: revocation of a privileged role mutually excludes future privileged actions. A single-protocol invariant that single-contract audits verify trivially. Under Solana's durable-nonce semantics, the assumption breaks.
The pattern
Same failure class, two different surfaces. In Kelp, the failure lives across three protocols (the adapter, the messaging layer, the RPC layer) and one chain (the bridge between Unichain locks and Ethereum supply). In Drift, the failure lives across two protocols (the admin/multisig stack and the market/vault stack) and the platform-level semantics of Solana's durable nonce.
Both failures have the same shape: a property that holds for any single component in isolation, and breaks when those components interact.
III. The audit, as practised
Before the two incidents, it is worth being exact about what a smart-contract audit is, because the argument that follows depends on it. I first wrote this teardown at the end of 2025; the shape of the process has not changed.
- You pay somewhere between $50,000 and $500,000.
- Expert humans read your code for two to six weeks.
- They write a report listing what they found.
- You fix those issues.
- You deploy with a badge saying you were audited.
Human auditors are brilliant, and they catch real bugs. They are also bounded in ways no amount of brilliance removes.
Time: they have days or weeks. Attackers have forever.
Scope: they check what they think to check. Attackers check everything.
Consistency: different auditors, different findings.
Subjectivity: "we found no critical issues" and "there are no critical issues" are different sentences.
When an auditor says "we reviewed your code and found no vulnerabilities", the honest reading is: in the time we had, checking the things we thought to check, we found nothing obvious. That is an opinion, and a valuable one. It is still an opinion.
The two April incidents push the argument one step further, and the step is the interesting part. Both audits were good. Even a perfect opinion about one contract says nothing about the system that contract lives in.
IV. Why the audits were correct
Six contracts were at the centre of these two incidents. All six had been audited. None of the audits found defects.
The audits were correct, and nobody was negligent.
A single-contract audit verifies that a contract behaves correctly under its declared assumptions about its environment. The KelpAdapter audit verified that, given a valid DVN message and a valid RPC observation, the mint produces the right rsETH amount. It did. The DriftMarket audit verified that, given an active admin and a satisfied timelock, add_cvt updates the whitelist correctly. It did.
What audits do not — and cannot — verify is whether those declared assumptions hold under adversarial composition with the actual contracts the system depends on. The audit doesn't see the DVN's signer set, the RPC's integrity, the durable-nonce semantics, the timing-window between revocation landing and downstream observation. The class of property the audit verifies is structurally weaker than the class of property the actual failure violates.
Here's the visual:
┌── SINGLE-CONTRACT AUDIT ─────────────────────────────┐
│ │
│ ┌───────────────┐ │
│ │ KelpAdapter │ Question: does this contract │
│ └───────────────┘ behave correctly under its │
│ declared environment │
│ Verdict: ✓ correct assumptions? │
│ │
│ (the audit was right — the contract IS correct) │
└──────────────────────────────────────────────────────┘
┌── CROSS-PROTOCOL FORMAL VERIFICATION ────────────────┐
│ │
│ ┌─────────┐ ┌─────┐ ┌──────┐ ┌─────────────┐ │
│ │ Adapter │◄──│ DVN │◄──│ RPC │ │UnichainSrc │ │
│ └─────────┘ └─────┘ └──────┘ └─────────────┘ │
│ │ ▲ │
│ └──────────────────────────────────┘ │
│ │
│ Question: does the JOINT system ever enter a │
│ forbidden state, across all reachable executions? │
│ │
│ Verdict: ✗ VIOLATED — here is the trace: │
│ [5-step counterexample, isomorphic to Apr 18] │
└──────────────────────────────────────────────────────┘The first verification class subsumes the second only when the composition is trivial. For any non-trivial multi-protocol system, it doesn't.
This is the thesis of this essay. The detection of failures like Kelp and Drift requires expressing the composition explicitly, the joint state space exhaustively, and the safety claims temporally — a class of verification that existing audit practice does not include.
V. How model checking works
The verification class I'm describing has a name: model checking. It's a textbook technique from formal methods, developed in the 1980s and applied at scale to hardware verification (Intel, ARM, Boeing avionics) for two decades before reaching the smart-contract space.
The idea is simple. You build a mathematical model of the system: a set of state variables, an initial condition, and a transition relation describing how the state evolves. You write a property the system must satisfy as a temporal-logic formula. You hand both to a tool — a model checker — that explores the entire reachable state space and either proves the property holds in every reachable state or returns a counterexample: a concrete trajectory through the state space that exhibits a state the property forbids.
┌─────────────────────┐ ┌─────────────────────────┐
│ System model │ │ Property formula │
│ (state vars, │ │ (CTL or LTL — what │
│ init, transitions)│ │ "must always hold") │
└──────────┬──────────┘ └────────────┬────────────┘
│ │
▼ │
┌─────────────────────┐ │
│ State-space │ ◄────────────────────┘
│ exploration │ check property over
│ (symbolic search) │ every reachable state
└──────────┬──────────┘
│
▼
┌──────────────────────────────────────────────────┐
│ Verdict │
│ ✓ PROVEN — holds in every reachable state │
│ ✗ VIOLATED — counterexample trace produced │
└──────────────────────────────────────────────────┘Two property logics matter for what follows.
CTL — Computation Tree Logic. Reasons over the branching tree of possible executions. The operator AG reads "Always Globally" — in every reachable state of the system, the inside formula holds. Other operators include EF ("Exists a Future where") and AF ("on All paths, eventually"). Here's a Kelp invariant decoded:
AG ( kelp.rseth_supply ≤ unichain.real_lock_count )
│ │ │
│ │ └─ source-chain locks
│ │ on Unichain
│ └─ destination-chain rsETH
│ supply on Ethereum
│
└─ "Always Globally" — in every reachable state
of the joint system, the inside must hold
In English: "destination supply must never exceed
source locks, in any reachable state."LTL — Linear Temporal Logic. Reasons over individual infinite executions. The operator G reads "Globally" — on every infinite execution, the inside holds at every step. F reads "Finally" — at some future point on the execution. Here's the Kelp signer-rotation property decoded:
G ( ¬dvn.signer_integrity_0 → F ¬dvn.message_signed )
│ │ │ │
│ │ │ └─ DVN no longer
│ │ │ signing
│ │ └─ "Finally" — at some
│ │ future point on the
│ │ execution
│ │
│ └─ DVN signer compromised
│
└─ "Globally" — on every infinite execution
In English: "if a DVN signer is ever compromised,
eventually the DVN must stop signing."CTL is checked exhaustively under symbolic representations called binary decision diagrams (BDD) — the exploration covers every reachable state of the system, no matter how many. LTL is typically checked under bounded model checking (BMC) — the exploration covers every execution up to a fixed depth k, beyond which there are no guarantees.
The trade-off: CTL/BDD gives you a definitive verdict (PROVEN means it really is proven over the entire reachable state space) but can struggle on very large systems. LTL/BMC always terminates within the bound but only proves "no counterexample exists within depth k" — for safety properties, this is usually enough.
For Kelp and Drift, we used both. Safety invariants got CTL/BDD treatment. Liveness-flavoured properties got LTL/BMC at depth 10.
VI. The Kelp counterexample
Kelp is modelled as five components. Each is a small state machine.
┌─── KelpAdapter ──────┐ ┌─── LayerZeroDVN ─────┐
│ idle ──► queued │ │ honest ──► signed │
│ │ │ │ │ │ │ │
│ │ ▼ │ │ │ ▼ │
│ └────► minted │ │ └────► broadcast │
└──────────────────────┘ └──────────────────────┘
┌─── RPCNode ──────────┐ ┌─── UnichainSource ───┐
│ honest ──► staged │ │ no_lock ──► locked │
│ │ │ │ │ (real_lock_count │
│ │ ▼ │ │ stays 0 in the │
│ └────► compromised │ │ counterexample) │
└──────────────────────┘ └──────────────────────┘
┌─── AaveCollateral ───┐
│ available ──► used │
│ (post-mint sink for │
│ the unbacked rsETH)│
└──────────────────────┘These five state machines compose synchronously. Each protocol declares which of its outputs are observable to which other protocols, and the joint state space is the product of all the local state spaces.
┌────────────────┐
│ UnichainSource │ real_lock_count
└───────┬────────┘
│ (observed by adapter — not
│ wired in violating trace)
▼
┌────────────┐ attestation_verified ┌──────────────┐
│LayerZeroDVN├───────────────────────►│ KelpAdapter │
└────────────┘ │ │
│ │
┌────────────┐ rpc_integrity │ │
│ RPCNode ├───────────────────────►│ │
└────────────┘ └──────┬───────┘
│ rseth_supply
▼
┌──────────────┐
│AaveCollateral│
└──────────────┘
Joint state space = every reachable combination of
(adapter, dvn, rpc, source, collateral) variables.
The model checker explores ALL of them.Five properties were checked against this composition.
| Property | Verdict | Notes |
|---|---|---|
| Bridge authenticity | VIOLATED | 4-step counterexample. DVN buffer cycles before the adapter records the claim. |
| Cross-chain supply invariant | VIOLATED | 5-step counterexample — Apr 18 isomorphism. |
| Oracle-source legitimacy | VIOLATED | 5-step counterexample. RPC integrity flips at the same step the adapter consumes the oracle. |
| Access control (control property) | PROVEN | Discriminating-power witness — see below. |
| Admin revocation window | VIOLATED | Bounded counterexample within depth 10. |
The cross-chain supply counterexample is the headline. Five steps:
Step 1.1 ─ Initial steady state
adapter: idle dvn: honest
rpc: honest unichain: real_lock_count = 0
rseth_supply: 0 rpc_integrity: TRUE
Step 1.2 ─ Adversary stages forgeries
adapter: idle dvn: signed (forged)
rpc: staged (forged) unichain: real_lock_count = 0
rseth_supply: 0 rpc_integrity: TRUE
(signers still appear honest from joint observer)
Step 1.3 ─ DVN broadcasts
adapter: idle dvn: broadcast
rpc: staged (forged) unichain: real_lock_count = 0
rseth_supply: 0 rpc_integrity: TRUE
Step 1.4 ─ Adapter receives, queues mint
adapter: queued dvn: buffer_cycled
rpc: staged (forged) unichain: real_lock_count = 0
rseth_supply: 0 rpc_integrity: TRUE
┌─ Step 1.5 ─ ⚠ VIOLATING STATE ─────────────────────┐
│ adapter: minted dvn: idle │
│ rpc: compromised unichain: real_lock=0│
│ rseth_supply: 1 rpc_integrity: FALSE │
│ │
│ Property AG(rseth_supply ≤ real_lock_count) │
│ evaluates: 1 ≤ 0 → FALSE → VIOLATED │
│ │
│ Real-world: 116,500 rsETH minted on Ethereum │
│ block 24,908,285 against 0 ETH locked on Unichain│
└────────────────────────────────────────────────────┘In the model: 1 rsETH minted against 0 locks. In the real world: 116,500 rsETH minted against 0 locks. The numbers differ because the model uses bounded integers 0..10 for tractability — but the violating trajectory is identical. Destination supply minted against zero source backing while RPC integrity is compromised at the moment of mint.
The model checker found this in 22 milliseconds with no human guidance. Only the cross-protocol composition and the property statement.
An audit of KelpAdapter in isolation would never surface this trace, because the violation requires the joint state of Adapter + DVN + RPC + UnichainSource at the same reachable instant.
Why the control property's verdict matters
A skeptic should ask the obvious question. If you build a sufficiently permissive model, won't every property fail? The answer is yes — and this is why the control property exists.
The fifth property in the table — every consumed oracle was preceded by a recorded claim — is engineered to hold in every reachable state. It's a structural truism of the model: the transition that consumes the oracle is gated on the prior recording of a claim. The model checker confirms this exhaustively, with no counterexample.
Five properties checked against the Kelp composition:
Property Verdict
────────────────────────────────────────────
Bridge authenticity ✗ VIOLATED
Cross-chain supply ✗ VIOLATED ◄── Apr 18 isomorphism
Oracle legitimacy ✗ VIOLATED
Access control (control) ✓ PROVEN ◄── discriminating power
Admin revocation window ✗ VIOLATED
────────────────────────────────────────────
The control property's PROVEN verdict is the
discriminating-power witness. The model has the
power to PROVE invariants that hold; it does not
blanket-violate every property. The four violations
are real bugs in the composition, not artefacts
of a permissive abstraction.Combined wall-clock for all five: ~120 milliseconds.
VII. The Drift counterexample
Drift's composition is denser. Eight modules, with the bug path running through six of them.
Bug path (thick arrows)
┌───────────┐ ┌──────────────┐ ┌───────────┐
│ Multisig ├────►│ DriftAdmin │ ◄───┤ Timelock │
│ (2-of-5) │ │ admin_active │ │ │
└───────────┘ └──────┬───────┘ └───────────┘
│ (revocation
│ flips FALSE)
▼
┌───────────────────┐ observed by ┌─────────────┐
│SolanaDurableNonce ├──────────────►│ DriftMarket │
│ (process-typed — │ replay_in_ │ add_cvt_* │
│ 4-slot replay │ window │ cvt_whitelist│
│ window) │ └──────┬──────┘
└───────────────────┘ │
│ (whitelisted
│ fake CVT
│ redeemed)
▼
┌─────────────┐
│ DriftVault │
│ collateral │
└─────────────┘
Peripheral (not on bug path)
┌─────────────────┐ ┌─────────────────┐
│OracleAggregator │ │ RaydiumPool │
│ (NOT on the │ │ (cascade target │
│ trust path — │ │ post-drain; │
│ see §VII caveat)│ │ not the cause) │
└─────────────────┘ └─────────────────┘The same five-property structure was applied.
| Property | Verdict | Notes |
|---|---|---|
| Admin revocation window | VIOLATED | 5-state lasso, loop at state 1.4 — Apr 1 isomorphism. |
| Solvency invariant | VIOLATED | 3-state reachability witness ending in vault.drained=TRUE. |
| Oracle-source legitimacy | VIOLATED | Reachability witness — see caveat below. |
| Access control (control property) | PROVEN | Discriminating-power witness. |
| Governance timelock | VIOLATED | Bounded counterexample — add_cvt_signal=TRUE while timelock unsatisfied. |
The admin revocation counterexample is the headline. It runs as a five-state lasso, with the loop-back at state 1.4. The four conjuncts of the violated formula — revocation executed, replay window open, whitelist add signal active, all simultaneously — converge on state 1.4, a state the property forbids.
Step 1.1 Step 1.2 Step 1.3
┌──────────┐ ┌────────────┐ ┌──────────────┐
│ Initial │ ────────►│ Queue │ ────────►│ Multisig 2/5 │
│ admin=ON │ │ revoke + │ │ threshold; │
│ vault=285│ │ attacker │ │ timelock │
└──────────┘ │ pre-signed │ │ enqueued │
└────────────┘ └──────┬───────┘
│
▼
┌─ Step 1.4 ── ⚠ THE INCIDENT ───────┐
│ admin_active = FALSE │
│ replay_in_window = TRUE │
│ add_cvt_signal = TRUE │
│ timelock_satisfied = FALSE │
│ │
│ All 4 conjuncts hold in the │
┌──────────►│ SAME reachable state — a state │
│ │ the property forbids. │
│ │ │
│ │ cvt_whitelist: 1 → 2 │
│ loop │ (fake CVT now resident) │
│ on 1.4 └────────────────────────────┬───────┘
└────────────────────────────────────────┘
│
▼
┌──────────────────┐
│ Step 1.5+ │
│ vault.drained=T │
│ collateral=0 │
│ cascade → Raydium│
└──────────────────┘
Property G ¬(admin.revocation_executed
∧ nonce.replay_in_window
∧ market.add_cvt_signal)
evaluates at state 1.4: ¬(T ∧ T ∧ T) = ¬T = FALSE
→ VIOLATEDIn real-world terms: 31 transactions over 12 minutes, ~$285M USDC. In the model: one add_cvt plus one redeem, sufficient to expose the bug class. The 4-slot durable-nonce gap between revocation landing and downstream consumers seeing admin_active=FALSE is the exploitation window — encoded as replay_in_window = nonce_signed_pre_revoke ∧ ¬nonce_consumed ∧ replay_slot < 4.
A note on the oracle-legitimacy verdict, because it's important to read it correctly. The model also flags a separate oracle-source check; this is the same composition gap viewed from a different invariant — it is not a claim that Drift's price feed was compromised on April 1. Drift's oracle behaved correctly throughout the incident.
The verdict is technically right under the property's binding (vault.drained implies oracle.confidence_ok ∧ oracle.liquidity_ok): the model permits a state where the vault drains while oracle health is degraded, because the drain transition does not gate on oracle health. The correct lesson is that a defense-in-depth oracle gate cannot prevent this class of failure — the trust path that drained the vault was admin → whitelist → CVT.redeem, and the oracle was never on that path.
The control property — every privileged action was authorized at the action's slot — is proven exhaustively. Combined wall-clock for all five Drift properties: ~5 seconds.
VIII. The audit-gap thesis, restated
Six contracts. All audited. None of the audits surfaced any of the counterexamples above.
The audits were correct under their scope, and nobody was negligent. The class of property an audit verifies, each contract behaves correctly under its declared environment assumptions, is structurally weaker than the class the model checker verified, the composition behaves correctly across all reachable joint states. The first subsumes the second only when the composition is trivial, and for multi-protocol systems it rarely is.
This is a property of the verification class itself, and says nothing against audit firms or audit quality. Single-contract auditing answers the question "does this contract do what its specification says?" Cross-protocol formal verification answers "does the composition of these contracts ever enter a state the joint specification forbids?" Both questions are valid, and they are different questions. Asking only the first one is what the industry has been doing.
IX. Why proof is not yet everywhere
If proof is this strong, why is it not standard? I gave three reasons in 2025, and they still hold.
Expertise is scarce. Writing a formal specification means understanding the code and the mathematics at once. Most smart-contract developers know Solidity; few know temporal logic, and the people who know both are a few hundred, expensive, and not multiplying.
It costs time and money. A formal-verification engagement has typically run to months and six figures. For a team shipping fast, that has meant no engagement at all.
The specification is the hard part. To prove code correct you need a formal statement of what correct means, and a wrong specification yields a proof of the wrong thing. Garbage specification in, garbage proof out.
All three are the kind of bottleneck AI changes. A model can draft the specification from the code and its documentation, a human expert reviews it instead of writing it, and the checker gives the verdict in seconds instead of weeks. The case study above took no human guidance beyond the model and the property: 13 modules across the two systems, 10 properties, under five seconds of wall-clock for both, with verdicts isomorphic to the published chronologies of the incidents.
That work belongs to Kerubim, the venture of the Fucina Nexus Program whose function is AI-powered code writing and formal verification, with mathematical proof. It is in production, with a limited subset of what it will do. The stack described here composes per-protocol state-transition models into a synchronous product, states the joint properties in CTL or LTL, and runs them through a symbolic model checker. The output is either an exhaustive proof or a counterexample trace.
X. What comes next
Web3 needs verification that follows the trust path, and the trust path ignores contract boundaries.
The trust path that drained Drift on 1 April ran from a Solana durable nonce, through a market gating function, into a vault that did not gate on oracle health. The trust path that minted unbacked rsETH on 18 April ran from a compromised LayerZero DVN, through a compromised RPC, into an adapter that did not gate on source-chain reality. None of these paths fits inside a single contract. All of them are expressible, and decidable, under cross-protocol formal verification.
Nothing here is hypothetical. The two largest DeFi incidents of April 2026 are the case study. Both contracts had been audited. Both audits were correct. And cross-protocol model checking finds the violation in milliseconds, with the counterexample isomorphic to the published chronology.
The audits did exactly what they were asked to do. The question now is whether the industry is willing to ask the next question.