The KelpDAO Exploit Was Not a Bug

Incident note. Theme: signatures are not semantics.

TL;DR

On April 18, 2026, at 17:35 UTC, a transaction routed through the LayerZero EndpointV2 contract on Ethereum released 116,500 rsETH from the Kelp bridge to an attacker-controlled address. The transaction was successful, emitted Transfer, OFTReceived, and PacketDelivered events, and carried a claimed source EID of 30320. Kelp later acknowledged “suspicious cross-chain activity,” said it had paused rsETH contracts across mainnet and several L2s, and Aave disclosed that its Guardian began freezing rsETH and wrsETH markets at 18:52 UTC. As of April 19, 2026, LayerZero said it was still investigating the root cause with Kelp and SEAL, and had not yet published a full joint post-mortem. That means some implementation details remain provisional, but the core exploit path is already publicly verifiable. (1) (2) (3) (4)

The technical thesis is simple and brutal: this was not fundamentally a “bridge hack” in the colloquial sense, and it was not merely “bad luck.” It was a specification failure. LayerZero’s own documentation makes clear that an application’s security stack is configurable: DVNs verify a message payload hash, and once the configured threshold is met, the message can be committed and executed on the destination chain. The question, then, is not whether a signature existed. The question is whether the executed destination transition was semantically justified by a real, unique, finalized source-chain debit event. In the Kelp path that failed, public on-chain analysis indicates the rsETH OFT adapter was effectively operating with a one-of-one DVN configuration, turning “a valid attestation exists” into “release funds.” That is a catastrophic mismatch between cryptographic verification and protocol correctness. (5) (6) (7)

A widely circulated investigator claim held that the Unichain-side rsETH float was only 49 tokens at the time, or at least in that neighborhood, which is why the incident has been summarized as “116,500 rsETH withdrawn against 49 on the source.” I have not seen an official post-mortem or immutable primary-source snapshot from KelpDAO or LayerZero that conclusively proves the exact pre-attack “49” figure. What is beyond dispute is the order-of-magnitude mismatch: a successful Ethereum-side release of 116,500 rsETH was executed and logged on-chain, and contemporary investigator posts framed the source-side inventory as trivial by comparison. For engineering purposes, the exact scalar is less important than the violated invariant: the destination transition consumed more economic entitlement than the source side could plausibly have produced. (1)

The blast radius was not created by the bridge alone. It was created by composability. The attacker turned the unbacked or provenance-corrupted rsETH into borrow power across lending venues, exploiting the fact that lending protocols reason primarily about collateral valuation, caps, and liquidation thresholds, not about whether a bridged token’s source-chain transition was semantically valid. Aave’s own documentation describes health-factor- and liquidation-threshold-based risk control; the Compound III documentation similarly describes collateral factors, borrow collateralization, and pause-guardian controls. Those are necessary controls, but they are not provenance proofs. When Kelp failed, those protocols inherited toxic state. (8) (9)

The conclusion of this article is deliberately adversarial: DeFi in 2026 is still too willing to confuse signatures with truth, audits with assurance, and emergency multisigs with engineering. A serious remediation strategy has to start from invariants, temporal semantics, and refinement proofs. It has to move cross-chain execution from “attested packet delivery” to “proof-carrying state transition.” It has to treat economic safety properties as first-class formal predicates, not as after-the-fact risk commentary. That is exactly the direction suggested by recent formal-methods work such as KindHML and the original proof-carrying code literature. (10) (11)

Key takeaways

• Destination execution must be gated by semantic entitlement (a unique, finalized source debit), not by “some attestation exists.”
• A 1-of-1 security stack turns protocol messaging into a single-point-of-failure oracle; it is a trust downgrade, not “decentralization.”
• Composability is an amplifier: once provenance-corrupted collateral is admissible, lending venues inherit toxic state regardless of their own local correctness.
• The remediation is invariant-driven design + proof-carrying transitions + operational circuit breakers; “add another signer” is not a spec.
• Treat every exploit as a counterexample trace; ship the fix as a smaller language of reachable bad states, enforced in CI.

Assumptions

• Some incident details remain provisional until Kelp/LayerZero publish a joint RCA; the analysis is constrained to publicly verifiable chain data + primary docs. (1) (5)
• The effective trust boundary is the destination adapter’s release guard; once it accepts a packet, the system treats the resulting state transition as truth.
• “DVN threshold satisfied” is modeled as a cryptographic predicate over a payload hash; it is not assumed to imply source-state membership.
• Downstream lending protocols are assumed to be locally correct with respect to their own specs (oracle valuation, health factor, liquidation rules) while being provenance-agnostic by design. (8) (9)

Non-goals

• This is not a final RCA, and it does not claim attribution for the root cause beyond the observable invariant breach.
• This does not attempt a loss allocation analysis across venues; that is governance + accounting, not protocol correctness.
• This is not an argument that LayerZero-style messaging is “inherently insecure”; it is an argument that semantic settlement cannot be reduced to packet attestation.

Security properties

P1 — Supply conservation (economic safety)

For each channel c and message identifier guid, the destination release must be bounded by the entitled amount induced by a unique, finalized source debit:

release_amount(c, guid) ≤ entitled_amount_from_source(c, guid).

P2 — Provenance (unique finalized debit)

Every destination release implies existence of exactly one corresponding source event in canonical finalized state:

release(guid, a, r) → ∃! burn_or_lock(guid, a, r) ∈ FinalizedSource.

P3 — Replay safety (single consumption)

Execution is idempotent and consumes guid exactly once:

execute(guid) → verified(guid) ∧ ¬consumed(guid) and execute(guid) → X(consumed(guid)).

P4 — Negotiation / config integrity (no silent trust downgrade)

Security-stack parameters (required/optional DVNs, thresholds, receive libraries) must be explicit, authenticated, versioned, and observable. “Equivalent” legacy spellings are downgrade gadgets. (5)

P5 — Blast-radius containment (compositional safety)

If provenance cannot be verified cheaply, the system must isolate risk domains (caps/silos/spokes) such that a provenance failure cannot drain shared liquidity.

Incident reconstruction

There are two constraints on honest analysis here. First, the exploit is recent and some public numbers are still moving. Second, neither KelpDAO nor LayerZero has published the full formal RCA yet. So the right posture is not false certainty. It is disciplined reconstruction from public chain data, official protocol statements, and primary documentation. The timeline below reflects that standard. (1) (2) (3)

The transaction itself is unusually revealing. On Etherscan, the exploit transaction shows a direct interaction with LayerZero EndpointV2, successful execution status, a timestamp of April 18, 2026 at 17:35:35 UTC, and a transfer of exactly 116,500 rsETH from the Kelp bridge contract to the attacker. The decoded log shows OFTReceived with srcEid = 30320, followed by PacketDelivered. That is not a vague “possible exploit.” It is a concrete destination-side state transition that the system admitted as valid. (1)

Public on-chain analysis published within hours of the incident described the active security stack as effectively one required DVN, zero optional DVNs, and no meaningful redundancy. LayerZero’s own documentation explains why that matters: DVNs independently verify the payload hash, and once the required DVNs and optional threshold are satisfied, an executor or other authorized caller can commit the nonce and drive execution on the destination endpoint. LayerZero also documents that the default security stacks for new channels are multi-DVN presets, not single-signer production assumptions for high-value pathways. If a nine-figure bridge path was running as one-of-one in practice, that was not the protocol “being decentralized.” It was a brittle trust downgrade. (5) (7)

The follow-up attempts matter almost as much as the initial drain. CredShields reconstructed a 46-minute interval from the first drain to Kelp’s pauseAll, and reported two later attempts at roughly 18:26 UTC and 18:28 UTC that did not succeed. That means the failure mode was not singular or self-limiting. It remained reachable until a human emergency control intervened. In other words, the system’s actual safety property was not “invalid releases are impossible.” It was “invalid releases remain possible until a multisig wakes up.” (2)

The architecture of the vulnerable path can be expressed plainly:

flowchart LR
    A[Unichain-side sender context] --> B[Packet claims source burn]
    B --> C[DVN attestation over payloadHash]
    C --> D[Receive library threshold satisfied]
    D --> E[LayerZero EndpointV2 lzReceive]
    E --> F[Kelp bridge adapter on Ethereum]
    F --> G[Escrow release of 116,500 rsETH]
    G --> H[Attacker]
    X[Missing control] -.-> F
    X["No proof of canonical source-state membership,
    no uniqueness proof, no semantic entitlement proof"]

The public timeline is equally stark. The following is an analytical reconstruction of blast-radius expansion from public timestamps and protocol responses. The y-axis is not “dollars lost.” It is the count of trust domains that had now become active incident participants: bridge, public detection, issuer controls, lending markets, and ecosystem governance. (2) (3)

xychart-beta
    title "Attack propagation versus time"
    x-axis ["17:35","17:52","18:21","18:26","18:52","20:10","Apr 19"]
    y-axis "Incident domains activated" 0 --> 6
    line [1,2,3,3,4,5,6]

And the time sequence itself, rendered as a directly reusable timeline:

timeline
    title KelpDAO exploit reconstruction
    17:35 UTC : Exploit transaction succeeds on Ethereum
              : 116,500 rsETH released
    ~17:52 UTC : Public on-chain alerting begins
    18:21 UTC : Kelp emergency pause executes
    18:26 UTC : Follow-up attempt observed
    18:28 UTC : Additional follow-up attempt observed
    18:52 UTC : Aave Guardian starts market freezes
    20:10 UTC : Kelp publicly confirms suspicious cross-chain activity
    Apr 19 : LayerZero says RCA still in progress
            : Aave says mainnet rsETH appears fully backed and exposure is capped

The invalid state was reachable

The right abstraction for this exploit is not a bug report. It is a counterexample trace in a state machine. That framing is standard in serious formal work on smart contracts and temporal properties: the system is a stateful transition system, and vulnerability means the existence of an execution trace reaching a forbidden state. KindHML explicitly models contracts as stateful systems and targets temporal properties that unfold across multiple transactions; SmartPulse makes the same point from an adjacent direction. (10) (12)

For this class of bridge, a minimum semantic model is:

State s =
  (escrow_eth,
   remote_supply[chain],
   executed_guids,
   finalized_roots[chain],
   bridge_config,
   risk_limits)

Input m =
  (src_chain, dst_chain, guid, amount, receiver,
   claimed_sender, claimed_root, proof_or_attestation)

The safety of the system is governed by a small set of invariants. If these had been specified, checked, and made gate conditions for execution, the exploit path would have been mechanically rejected.

In ASCII temporal notation, those properties look like this:

Conservation:
  release_amount(channel, guid) <= entitled_amount_from_source(channel, guid)

Provenance:
  release(guid, a, r) -> exists unique burn_or_lock(guid, a, r) in finalized source state

Atomicity:
  execute(guid) -> verified(guid) and not consumed(guid)
  execute(guid) implies next(consumed(guid) = true)

Temporal ordering:
  G( release(guid) -> P source_debit(guid) )

Economic admissibility:
  G( transition -> preserves_solvency and preserves_risk_limits )

The critical observation is that the exploit trace is easy to write down once the guards are written honestly.

s0:
  source-side rsETH float is tiny
  Ethereum escrow contains substantial rsETH
  bridge_config.requiredDVNCount = 1
  no source-state proof is required at release time

a1:
  attacker submits forged or otherwise invalid attested packet
  claiming srcEid = 30320, amount = 116,500, receiver = attacker

a2:
  verification threshold is considered satisfied

a3:
  EndpointV2 calls lzReceive on destination path

a4:
  Kelp bridge adapter releases 116,500 rsETH from escrow

s1:
  executed release exists without semantically sufficient source debit
  conservation fails
  provenance fails
  invalid state is reached

That is the exploit. Not “someone signed something bad.” The exploit is that the transition guard was too weak to preserve the intended invariant set.

The flawed guard can be summarized as follows:

flawed_release_guard(message):
    require attestation_threshold_satisfied(message.payloadHash)
    require not consumed(message.guid)
    release(message.amount, message.receiver)
    consumed(message.guid) = true

The fixed guard has to be materially stronger:

proof_carrying_release_guard(message, proof):
    require verify_attestation_threshold(message.payloadHash)
    require verify_source_state_root(message.src_chain, proof.root)
    require verify_inclusion_of_debit_event(
        proof.root,
        proof.guid,
        proof.amount,
        proof.receiver,
        proof.source_sender
    )
    require proof.amount == message.amount
    require not consumed(message.guid)
    require within_local_risk_limits(message.amount, message.src_chain)
    release(message.amount, message.receiver)
    consumed(message.guid) = true

This is where proof-carrying execution becomes the right mental model. The original proof-carrying code result made the principle explicit: do not trust the producer’s authority, require an efficiently checkable proof that the artifact satisfies the consumer’s safety policy. The same principle should govern cross-chain settlement. A signature over a payload hash is not enough when the safety policy is “this transfer corresponds to a real source-side debit in the formal bridge semantics.” The proof presented to the destination should carry that statement, not just a weaker cryptographic acknowledgment that some worker saw a packet. (11)

The desired destination path therefore looks like this:

flowchart LR
    A[Source chain burn or lock event] --> B[Finalized source state root]
    B --> C[Proof package]
    C --> D[Destination verifier]
    D --> E{Check all obligations}
    E -->|Valid| F[Release exactly entitled amount]
    E -->|Invalid| G[Reject]
    C -. includes .-> H[Event inclusion proof]
    C -. includes .-> I[Uniqueness and anti-replay proof]
    C -. includes .-> J[Economic admissibility proof]
    C -. includes .-> K[Threshold witness attestation]

Composability turned failure into bad debt

The attacker did not need to dump 116,500 rsETH directly into spot liquidity and eat the slippage. The more sophisticated route was to treat the stolen tranche as borrow power. Contemporary on-chain analyses put the Aave-specific borrow exposure at roughly 52,834 WETH on Ethereum and 29,782 WETH plus 821 wstETH on Arbitrum, with smaller positions also opened in Compound V3 and Euler before markets tightened and freezes propagated. Reporting across that first day placed total extracted borrow value across venues around the $236 million range, while estimates of Aave-specific bad debt ranged roughly from the high$100 millions into about $200 million depending on mark assumptions and unwind treatment. Those figures should still be treated as provisional because the joint RCA is not out yet, but the systemic point is already clear. (2)

Aave’s documented model is to let users borrow by posting collateral, with risk tracked through health factor, liquidation thresholds, and oracle-valued collateralization. Compound III documents the same basic structure in different language: collateral increases borrowing capacity through borrow collateral factors, and the system checks whether an account is borrow-collateralized. I am making an inference here, but it is a straightforward one from the docs: these engines are specified to reason about value and collateralization, not to prove source-chain provenance for every bridged collateral unit at borrow time. If an attacker can place a token into the eligible collateral state while the system still believes the token has acceptable value characteristics, shared liquidity is at risk. (8) (9)

That is why the phrase “mainnet rsETH appears fully backed,” which Aave later used in its public update, is not enough to dissolve the engineering problem. Even if the broader Ethereum mainnet rsETH supply remains asset-backed in aggregate, the specific tranche released by the exploit is still provenance-corrupted with respect to the source-to-destination bridge semantics. Lending markets do not survive by knowing that the category of asset is usually fine. They survive by knowing that the specific collateral units against a live debt position are actually realizable at liquidation time under the system’s settlement semantics. This is a subtle but decisive distinction, and it is exactly why composability failures are so vicious. (3)

The governance response was rational and still damning. Aave’s Guardian froze relevant rsETH and wrsETH markets starting at 18:52 UTC, later freezing WETH on several affected markets as a precaution. Compound III, by design, has a pause guardian with authority to halt supply, transfer, withdraw, absorb, and buy-collateral operations if an unforeseen vulnerability emerges. Those are necessary emergency tools. They are not substitutes for proof of correctness. They are social-consensus arrest powers. They exist because the underlying contracts are not fully self-defending against semantically invalid external state. (3) (9)

That is the architectural indictment. DeFi keeps advertising “code is law,” but under stress it reverts to social consensus at human speed. Humans freeze markets. Humans negotiate recovery. Humans decide who gets socialized losses. Humans interpret whether one wrapped asset should be made whole at the expense of another. None of that is illegitimate in a crisis. It is simply proof that the system failed to encode its own admissibility conditions up front.

The answer is not to abandon composability. It is to localize it. Shared-liquidity systems can be efficient, but efficiency without local semantic verification makes bad state mobile. The right direction is deterministic local verification: every collateral domain should be required to prove its own correctness locally before it is allowed to contaminate shared liquidity globally. Where that is too expensive, the system should fall back to local isolation: separate vaults, separate caps, or separate spoke risk buckets whose failure cannot drain shared liquidity. Energy should be spent minimizing blast radius, not defending the ideology of seamless composability at all costs.

What rigorous remediation looks like

The remediation program for a protocol like this cannot be “commission another audit and add another signer.” Audits are useful. They are not enough for cross-domain systems whose failure modes are semantic, temporal, and compositional. What is needed is a verification-aware architecture in which invariants are design inputs, not post-incident commentary.

The first design rule is invariant-driven architecture. That means every asset path should begin with a protocol-level invariant catalog: conservation, provenance, uniqueness, atomicity, ordering, bounded exposure, liquidity admissibility, and system-composition constraints. Every external call path and every privileged role must be mapped to the invariants it is allowed to affect. If a bridge path cannot state its invariants in unambiguous machine-checkable form, it is not mature enough to secure nine figures.

The second design rule is layered verification, because no single technique is enough. Model checking is excellent for state machines, temporal properties, and counterexample generation. SMT-based provers are excellent for transaction-level safety properties and bounded symbolic reasoning over code. Theorem provers are where refinement proofs and semantic equivalence arguments become trustworthy. Symbolic execution and invariant fuzzing remain indispensable because they generate adversarial witnesses and operationalize the threat model that the other layers specify. Recent smart-contract research and tooling reflect exactly this division of labor. KindHML targets temporal multi-transaction properties and leverages Kind2; SmartPulse targets temporal properties via instrumentation and checking; Solidity’s SMTChecker and commercial provers operate in the SMT-verification space; Foundry invariant testing and symbolic-execution tools provide aggressive counterexample search. (10) (12)

The third design rule is proof-carrying state transitions. A cross-chain release should be accompanied by a proof object carrying at least the following facts:

ProofCarryingRelease =
  {
    src_chain,
    dst_chain,
    guid,
    finalized_src_root,
    debit_event = (token, amount, sender, receiver, nonce),
    inclusion_proof,
    anti_replay_proof,
    threshold_witness_attestation,
    economic_admissibility_commitment
  }

The destination verifier should accept a release only if the proof establishes that the source-side debit event exists in canonical finalized state, maps uniquely to the claimed destination release, has not already been consumed, and does not violate local risk limits. This is not just “use more signatures.” It is change the admissibility predicate. Threshold witnesses still matter, but as attestations over finalized state and semantic facts, not as a replacement for those facts.

The fourth design rule is threshold witness governance. LayerZero’s documentation explicitly supports an X-of-Y-of-N model for DVNs and recognizes multiple implementation types, including multisignature, zero-knowledge proof, oracle, protocol-adapter, and light-client approaches. For a pathway securing nine-figure collateral, one-of-one is not a security budget; it is a confession. A sane minimum would require independent witness domains, explicit liveness and disagreement handling, and a hard separation between governance authority and execution authority. Governance can change parameters under delay. Governance must not be the thing that semantically certifies whether a release is real. (5)

The fifth design rule is deterministic local verification. If a bridge-delivered asset is admitted as lending collateral, then the lending venue should be able to verify, locally and deterministically, that the collateral unit belongs to a class of semantically valid claims. Where that is too expensive, the system should fall back to local isolation: separate vaults, separate caps, or separate spoke risk buckets whose failure cannot drain shared liquidity globally.

The sixth design rule is verification-aware CI. A serious CI/CD pipeline for a protocol exposed to this class of risk should include:

• invariant inventories as version-controlled artifacts;
• model checks on abstract bridge and settlement machines;
• SMT checks on release guards and role transitions;
• invariant suites over randomized transaction sequences;
• symbolic execution over attacker-controlled sequences;
• differential tests between abstract semantics and concrete implementations;
• regression suites for every discovered counterexample;
• policy checks preventing one-of-one security stacks or uncapped collateral onboarding in production.

This must become build hygiene, not a special engagement after a hack.

Finally, the offensive cost model changed. Anthropic’s own disclosures around Mythos Preview and Project Glasswing state that frontier models are being used to find vulnerabilities faster, and the 2025 “Prompt to Pwn” work showed LLM-based systems generating functional smart-contract proof-of-concept exploits with high success rates on benchmarked tasks. That does not mean models autonomously break every cross-contract economic system today. It does mean the cost of invariant hunting has collapsed, and protocol teams that still rely on “it passed audit” are now facing machine-scale adversarial search. Formal specifications are no longer academic overhead. They are increasingly the only way to keep the offense-defense economics from becoming absurdly one-sided. (13) (14) (15)

The mandate serious protocols should fund

If I were brought in to harden a protocol against the exact class of failure exposed here, I would not start with patching one adapter and declaring victory. I would start by forcing the protocol to state, in machine-checkable form, what transitions are actually allowed to move value. Then I would force the implementation, the proof layer, and the risk layer to refine that specification. The deliverables below are not theoretical. They are what a competent protocol should now consider table stakes.

The concrete work products I would want a protocol to walk away with are these:

First, an executable bridge specification that states, in one place, the semantics of debit, settlement, replay prevention, ordering, cancellation, timeout, and pause behavior.

Second, a proof obligation ledger mapping every security claim to one of three states: formally proven, empirically stress-tested, or assumed but not yet discharged. Most protocols would find that far too much of their current “security” lives in the third column.

Third, a proof-carrying transition format for every high-value cross-domain release path, so that the destination accepts a transition because it is semantically justified, not because some signer stack emitted an acceptable packet hash.

Fourth, local admissibility rules for collateral. If a token cannot prove provenance cheaply, it should not have access to shared liquidity in the same way as assets with fully verifiable provenance.

Fifth, a CI system that treats every discovered exploit trace as a first-class regression artifact. The objective is not merely to fix the specific bug. It is to make the counterexample language smaller with every release.

Sixth, governance boundaries that are explicit and formally bounded. Emergency roles should be able to stop the system, not silently redefine truth.

That is the practical roadmap. The deeper verdict is harsher.

The KelpDAO exploit should end a certain style of DeFi thinking. The style I mean is the one that says modularity absolves responsibility, that bridge security is a parameter, that signatures are “decentralization,” that audits stand in for semantics, and that it is acceptable to let downstream protocols discover your trust assumptions only after they have already accepted your asset as collateral.

It should also end the lazy way people talk about formal verification. Formal methods are not a luxury reserved for aerospace or consensus code. They are what you reach for when a wrong transition can destroy nine figures in under a second and then metastasize through shared liquidity before a human can finish reading the alert.

The KelpDAO incident is DeFi’s Chernobyl moment only if the industry learns the right lesson from it. The right lesson is not “bridges are risky.” Everyone already knew that. The right lesson is that DeFi still builds systems whose safety depends on unstated semantics, human interpretation, and emergency governance after the fact. That is not high-assurance infrastructure. That is leveraged ambiguity.

If a protocol wants to become serious infrastructure, it has to do three things. It has to define correctness mathematically. It has to force every high-value transition to carry evidence of that correctness. And it has to contain failure locally when correctness cannot be established cheaply enough.

Until then, DeFi is not replacing fragile finance. It is digitalizing fragility and calling it innovation.

Failure modes

• Attestation-as-truth: a destination release guard equates payload-hash attestation with semantic entitlement (no source-state membership proof).
• Configuration downgrade: security-stack defaults are bypassed (1-of-1 DVN; optional threshold set to 0; unpinned receive library), creating a single oracle.
• Replay / duplication: message identifiers are not consumed correctly, or the same semantic debit is claimable multiple times under different identifiers.
• Finality confusion: a non-finalized, reorgable, or non-canonical source event is treated as final, enabling reversible debits to back irreversible releases.
• Composability contagion: a provenance failure escapes into shared-liquidity venues where the admissibility predicate is valuation, not provenance.
• Human-speed safety: the true invariant is “invalid release remains possible until a multisig pauses,” which is not a safety property.

What to monitor

• Per-channel outflow invariants: released(dst) − debited(src) bounds, tracked per asset + channel with alerting on divergence growth.
• Security-stack drift: required/optional DVNs, thresholds, receive library identifiers, and any governance-controlled parameters (detect silent downgrades).
• First-flight anomalies: bursty lzReceive execution counts, unusual srcEid distributions, and repeated guid failures/successes.
• Collateral admission telemetry: bridged-asset collateralization share, borrow utilization, and liquidation pipeline health (especially during incident windows).
• Circuit-breaker activation time: minutes-to-pause is a KPI; target seconds, not “46 minutes to multisig.”

Rollback plan

For operators running high-value cross-domain settlement paths:

1. Fail-closed: pause releases on the destination adapter, freeze mint/redeem paths, and block unknown srcEid routes.
2. Quarantine collateral domains: isolate affected bridged assets in lending (caps to zero, freeze borrows, halt transfers if supported).
3. Invalidate and re-pin configs: redeploy or reconfigure to remove 1-of-1 stacks, pin receive libraries, and require explicit multi-witness thresholds.
4. Reconcile entitlement: compute a deterministic ledger of source debits vs destination releases; mark provenance-corrupted units for unwind or socialized resolution.
5. Ship a guard upgrade: require proof-carrying release objects (finalized root + inclusion + uniqueness + anti-replay) before unpausing.

Evidence

• Exploit transaction (lzReceive on LayerZero EndpointV2 releasing 116,500 rsETH): etherscan.io/tx/0x1ae232da.... (1)
• Aave Guardian freeze timeline (rsETH/wrsETH frozen starting 18:52 UTC): governance.aave.com/t/rseth-incident-2026-04-18. (3)
• Incident reconstruction and follow-up attempts (18:26 / 18:28): discover.credshields.com/incident-report-kelp-dao-rseth-bridge-exploit. (2)
• LayerZero security stack semantics (required DVNs, optional threshold, default configs): docs.layerzero.network/.../security-stack-dvns. (5)
• One-of-one DVN configuration details and addresses: defiprime.com/kelpdao-rseth-exploit. (7)

Checklist

• Treat “attestation verified” as necessary but not sufficient; the guard must bind to a unique, finalized source debit.
• Make supply conservation explicit and enforce it at the destination transition boundary.
• Require multi-witness verification by policy (no one-of-one stacks for high-value channels) and hash+pin configs on-chain.
• Add proof-carrying release objects (event inclusion + uniqueness + anti-replay + economic admissibility).
• Isolate bridged-collateral risk domains by default (caps, spoke vaults, or per-asset silos) when provenance cannot be verified cheaply.
• Add outflow circuit breakers (seconds, not “46 minutes to multisig”).
• Version and regression-test every incident counterexample trace in CI.

Further reading

• KindHML (temporal verification of smart contracts via Kind2): arxiv.org/abs/2604.14038. (10)
• SmartPulse (temporal checking of smart contracts): microsoft.com/.../SmartPulse-Oakland21-preprint.pdf. (12)
• Proof-Carrying Code (original principle): cs.cmu.edu/~necula/papers/pcc-pldi97.pdf. (11)
• Prompt-to-Pwn (LLM-driven exploit synthesis + validation): arxiv.org/abs/2508.01371. (15)
• Anthropic Project Glasswing: anthropic.com/glasswing. (13)
• Anthropic Mythos Preview (security implications): red.anthropic.com/2026/mythos-preview. (14)