March 13, 2023. Euler Finance gets drained of $197M in a single transaction. The root cause was one missing health check in one function.

That's it. Every other function that touched a user's position called checkLiquidity(). donateToReserves() didn't. Three audit firms missed it. The protocol had been live for over a year.

This post shows what the bug actually looked like and the exact invariant that closes the vulnerability class permanently — not just for Euler, but for any lending protocol with the same asymmetry.

The bug

donateToReserves() let users voluntarily contribute their eToken balance to the protocol reserve. Legitimate feature. The function decreased the user's balance and emitted an event.

What it didn't do was check whether the position was still solvent after the donation.

solidity

// Every borrow/repay/withdraw path called this.
// donateToReserves() did not.

function checkLiquidity(address account) internal view {
    uint collateralValue = getCollateralValue(account);
    uint liabilityValue  = getLiabilityValue(account);
    require(collateralValue >= liabilityValue, "under collateralized");
}

// The entire bug lives in this absence.
function donateToReserves(uint subAccountId, uint amount) external {
    address account = getSubAccount(msg.sender, subAccountId);
    decreaseBalance(account, amount);
    // ← no checkLiquidity()
    emit Donate(account, amount);
}

The attacker took a large leveraged position, donated the collateral away via donateToReserves(). Loan outstanding, collateral gone. Position underwater — but no health check fired so the protocol didn't know. That opened a liquidation opportunity. The liquidation math also had a miscalculation that let the attacker profit from their own liquidation, extracting more than they borrowed.

$197M. ~12 transactions. One missing function call.

Why audits didn't catch it

Three firms reviewed Euler. None flagged this. donateToReserves() looks fine in isolation — it does exactly what the name says. The missing health check only becomes obvious when you're specifically verifying that every position-modifying path calls it. That kind of cross-function coverage is hard to maintain manually as a protocol grows. Functions get added. The invariant stays documented. The enforcement doesn't follow it.

The invariant

The constraint is simple. Any active borrower's collateral value must be greater than or equal to their liability value. Always. Doesn't matter which function was called. State is state.

In ISL:

// euler-solvency.isl
@invariant per_account_solvency
@severity  Solvency
@protocol  euler_markets = env("EULER_MARKETS_MAINNET")

  @constraint no_unbacked_positions
    forall account in ACTIVE_BORROWERS:
      let collateral = field(euler_markets, collateral_value_slot(account))
      let liability  = field(euler_markets, liability_value_slot(account))
      implies(liability > 0, collateral >= liability)

  @constraint reserve_increase_not_from_collateral_loss
    let curr_reserve = field(euler_markets, total_reserve_slot())
    let prev_reserve = previously(field(euler_markets, total_reserve_slot()), 1)
    let curr_col     = field(euler_markets, total_collateral_slot())
    let prev_col     = previously(field(euler_markets, total_collateral_slot()), 1)
    implies(
      curr_reserve > prev_reserve,
      curr_col >= prev_col
    )

The first constraint catches any insolvent account directly. The second catches the pattern: reserve growing while total collateral shrinks. That's the exact signature of the donation exploit. Both fire.

What the epoch looks like

IVP provers commit a Merkle root of monitored state at epoch open, run the ZK circuit over the full window at close. The exploit executes inside epoch N. State violation persists — the attacker can't unwind it without returning the funds. Circuit sees it at reveal.

EPOCH N-1       → clean. all accounts solvent.
EPOCH N OPEN    → prover commits Merkle root of live state
BLOCK 16818056  → exploit executes. accounts insolvent. reserve/collateral mismatch.
EPOCH N CLOSE   → ZK circuit runs both constraints over full window
REVEAL          → violation_count = 2. proof on-chain.
+256 BLOCKS     → finality closes. claim filed. vault pays out automatically.

No committee. No governance vote. Proof is on-chain, payout executes. If Euler had registered this invariant and funded a coverage vault, users would have been compensated within ~300 blocks of the exploit.

The bug class

This is a general pattern: two functions that should behave identically, where one is missing a critical side effect. We keep finding it. The fix is always the same — add the missing call to the missing path. Five lines. But the window between deploy and fix is where the damage happens.

The ISL spec above is in the invariant library. Fork it for your lending protocol. The constraint is written once, enforced every epoch, forever.

IVP is runtime invariant enforcement for DeFi — protocols register ISL specs on-chain, a prover network verifies them every epoch, violations trigger automatic payout. No committees. Math closes it.

github.com/invariant-protocol · invariantprotocol.xyz