Catching a DeFi Exploit with Quint: Modeling the Balancer Upscale Bug
In November 2025, Balancer V2’s ComposableStablePool was exploited across multiple chains, resulting in significant losses. The root cause has been described as a rounding bug in a token scaling function. That description is accurate, but it leaves out the most interesting parts: why the bug was invisible to standard invariants, how one specific rounding operation accidentally masked it in every standard code path except when tokens were routed through the vault’s internal balance mechanism, and how a simple pool-level consistency check catches it in under 50ms.
We modeled the protocol in Quint, a formal specification language with a randomized simulator, with a straightforward goal: given a faithful model of the pool with the bug present, do naturally-stated correctness invariants find it? This post is the account of that investigation.
Background: Key Concepts#
Four concepts are needed to understand the exploit: the vault, the pool, rate-bearing tokens, and GIVEN_OUT swaps.
The vault is Balancer’s central settlement layer, the actual custodian of all tokens. Every token that enters or leaves the protocol moves through the vault. Pools themselves hold no tokens. When a swap happens, the vault calls the pool to compute the required amounts, then moves the tokens. The vault also supports internal balances: rather than sending tokens to a user’s wallet after a swap, they can be credited to an internal account inside the vault for use in subsequent operations without touching the ERC-20 layer.
The pool (ComposableStablePool) is a StableSwap AMM that supports BPT as a first-class swap asset (BPT stands for Balance Pool Token and its the ownership share token of the pool). Users can swap directly between underlying tokens (such as WETH and wstETH) and BPT. The pool implements the stable math and exposes a swap interface for the vault to call.
Rate-bearing tokens. wstETH is a liquid staking token that accrues yield over time, so 1 wstETH is worth more than 1 WETH and that ratio grows. The pool tracks this through a rate provider that returns the current exchange rate (e.g., 1.15). Before the pool’s stable math can process wstETH amounts, it upscales them (multiplies by the rate) to bring everything into a common unit space.
GIVEN_OUT swaps. Balancer supports two swap kinds. In a GIVEN_OUT swap (the relevant one here) the user specifies the exact output amount they want, and the pool calculates the required input. For a BPT → wstETH swap (GIVEN_OUT), the user says “give me exactly X wei of wstETH” and the pool charges the corresponding amount of BPT.
The Bug: Upscale Rounding Direction#
The pool’s stable math operates on a uniform internal representation: all token amounts are scaled to 18 decimals and multiplied by the token’s current rate before any invariant calculation. This conversion is the job of _upscale. It is called at the entry point of every swap, join, and exit to translate the user-facing native amounts into the scaled amounts the math works with. Without it, the pool would compare wstETH and WETH amounts directly, ignoring that 1 wstETH is worth 1.15 WETH.
The function responsible is _upscale in Balancer’s ScalingHelpers.sol:
function _upscale(uint256 amount, uint256 scalingFactor) pure returns (uint256) {
return FixedPoint.mulDown(amount, scalingFactor);
}mulDown is fixed-point multiplication that rounds the result down: it returns ⌊amount × scalingFactor / 1e18⌋. For GIVEN_OUT swaps involving rate-bearing tokens (where the scaling factor is not 1), this is the wrong rounding direction. For tokens with rate 1 (like WETH), mulDown and mulUp produce the same result: the bug only bites when the scaled amount has a fractional part.
When a user requests a specific native output amount, the pool upscales it to compute the required input charge (the user always receives the exact native amount they asked for). If _upscale rounds down, the pool bases its charge on a slightly smaller scaled value than the output is actually worth, and undercharges the user. The correct choice for GIVEN_OUT is mulUp: round the scaled output up so the pool never charges less than the full value of what it gives away.
A concrete example. With wstETH rate 1.15 (= 23/20 in exact arithmetic), a user requests 12 wei of wstETH:
Buggy (mulDown): ⌊12 × 1.15e18 / 1e18⌋ = ⌊13.8⌋ = 13
Correct (mulUp): ⌈12 × 1.15e18 / 1e18⌉ = ⌈13.8⌉ = 14Effect on pool state. After each operation, the pool stores the StableSwap invariant D (a single scalar representing the pool’s total liquidity, computed from the current scaled balances). The pool uses this stored D as the reference for subsequent fee calculations and BPT pricing: given a desired output, it solves for the input that keeps D constant.
With the buggy mulDown, the pool records a scaled output of 13 and stores D accordingly (as if only 13 units of scaled value were removed). But the actual native balance decreased by 12 wstETH, which at rate 1.15 is 13.8 scaled units, and should be accounted for as 14 with correct rounding. Because only 13 (not 14) was subtracted from the scaled balance, the stored scaled balance is 1 unit higher than the actual, and the D computed from it is correspondingly higher. This is the root cause: the pool’s stored D no longer reflects its actual balances.
When it fires. The rounding discrepancy only occurs for rate-bearing tokens when the product amount × rate is not an integer. For wstETH with rate 23/20, this means any output amount not divisible by 20. For a token with rate 1 (like WETH), mulDown(amount, 1e18) = amount exactly (no gap ever occurs). The per-swap error is always exactly 0 or 1 scaled unit, regardless of swap size. The example above uses 12 wei for arithmetic clarity; in practice the attacker used amounts at the scale of the pool’s actual liquidity, carefully chosen so that amount × rate is not an integer at the token’s real rate (ensuring the rounding gap fires on every swap).
Each swap looks fair, but D drifts. The BPT charged per swap is always correct: as we will see, an accidental compensation in the charge computation cancels the rounding error, so each individual exit is priced fairly. BPT → WETH swaps are never affected because WETH’s rate is 1 and no rounding gap occurs. The bug's effect is subtler: each BPT → wstETH exit stores a D slightly higher than the pool's actual balances support, and this error accumulates with every swap. Note that D still falls in absolute terms as tokens are withdrawn (removing tokens always reduces D) but the stored value falls by slightly less than it should, opening a growing gap between stored D and true D. This relative inflation is the bug's fingerprint; as we will see, a separate mechanism drives D far lower still, and that is what actually enables the profit.
How the exploit was structured. The exploit runs in three phases. First, the attacker drains the pool's liquidity by repeatedly exiting BPT for tokens. Second, with near-zero liquidity remaining, the attacker pushes the pool into extreme one-sided imbalance through token-to-token swaps; at this point StableSwap's Newton-Raphson solver converges to a near-zero D. Third, the attacker deposits the accumulated tokens back for BPT (against that collapsed D, the pool over-issues BPT massively, returning far more BPT than was borrowed to start the attack). To execute all three phases atomically, the attacker used the vault's internal balance mechanism (toInternalBalance: true): tokens from Phase 1 are credited to an internal account inside the vault instead of being transferred out, so they are available immediately for Phases 2 and 3 within the same batch transaction.
Phase 2 is independent of the upscale bug: it is a consequence of StableSwap math breaking down at near-zero, highly imbalanced liquidity. Note that Phase 1 drains all underlying token balances toward zero; Phase 2 does not drain the pool further, but redistributes the tiny residual into extreme one-sided imbalance. StableSwap's D collapses under extreme imbalance, forcing the Newton-Raphson solver to converge to a near-zero D. The bug's role is to make Phase 1 possible at low cost; the profit is produced entirely by Phase 2's D collapse.
Why Standard Invariants Miss the Bug: the BPT Compensation#
Before arriving at an invariant that works, we tried three natural candidates. They fail to detect the bug, and understanding why is as instructive as the final result.
Tokens are conserved#
The simplest pool security property: the total tokens entering the pool equal the total tokens leaving. For a BPT → wstETH exit, the BPT burned and the wstETH released are both accounted for correctly at the token level. The bug is a self-inconsistency in the pool’s stored D (not a creation of tokens from nothing). This invariant describes a different class of bug and does not fire here.
BPT rate never decreases#
A natural LP protection: after each swap, the value per BPT (the pool’s total scaled value divided by the virtual BPT supply) should not fall. If the output released is worth more in scaled terms than the input collected, the pool’s total value shrinks relative to the outstanding BPT supply, and the BPT rate drops.
This invariant does not fire. To see why, trace what happens inside calcBptInGivenExactTokensOut (the function that computes how much BPT to charge) when it receives the buggy scaled output of 13 instead of the correct 14:
New balance: the function sets the new wstETH scaled balance to
bwstETH - 13instead ofbwstETH - 14. The pool’s wstETH balance appears 1 unit larger than it should be.New invariant: it recomputes D from these new balances. A 1-unit larger wstETH balance produces a slightly higher D (the pool looks like it retained slightly more value).
Invariant ratio:
divDown(newInvariant, currentInvariant)computes a slightly higher ratio, meaning the swap looks like it removed slightly less value.Complement:
1 - invariantRatiois slightly smaller, representing the fraction of pool value that was removed.BPT to charge:
mulUp(virtualSupply, complement)rounds up this product.
The result of steps 1–5 is that the BPT charged ends up identical whether scaledAmountOut is 13 or 14. The mulDown in _upscale and the mulUp in the BPT charge happen to cancel exactly (not by design, but coincidentally), at the pool sizes and balance ratios where the exploit operates. The pool is not losing BPT per swap, so the invariant holds.
We confirmed this in the Quint model with a concrete test:
run testBptChargeCompensation = {
init.then(
val scaledBalances = scaleBalancesByRate(pool.balances, pool.tokenRates)
val virtualSupply = getVirtualSupply(pool)
val bptBuggy = calcBptInGivenExactTokensOut(pool.amp, scaledBalances, wstETH, 13, virtualSupply, 0)
val bptCorrect = calcBptInGivenExactTokensOut(pool.amp, scaledBalances, wstETH, 14, virtualSupply, 0)
all {
assert(bptBuggy == bptCorrect), // compensation: same BPT charged either way
pool' = pool
}
)
}This test passes, the compensation is real and reproducible.
The invariant D should not decrease#
For token-to-token swaps, D stays constant — tokens are exchanged but total pool value is unchanged. For BPT → wstETH swaps (where the user gives BPT and receives underlying tokens, withdrawing liquidity from the pool), D legitimately decreases: value is leaving the pool, so a lower D is the expected and correct outcome. Trying to enforce D non-decreasing across these swaps fires every time (buggy or not) because D always drops when liquidity is removed. The invariant is not bug-specific and is simply the wrong property to check for this action.
The Natural Invariant: poolInvariantDSound#
After the three failures above, the pattern was clear: all three invariants checked outputs and flows (BPT charged, tokens in and out) and all three held. The bug left no trace there. The right question turned out to be different: not “what does the pool give away?” but “what does the pool store about what it gave away?” After a buggy swap, the pool’s stored D no longer matches the D its actual balances produce. That mismatch is the fingerprint.
With the buggy mulDown, the pool stores its invariant D based on a scaled amount that is 1 unit smaller than the actual scaled change in pool balances. Specifically:
Pool stores invariant D computed from balances where the wstETH balance is reduced by
scaledAmountOut =⌊nativeOut × rate⌋(buggy)The actual wstETH balance in the pool is
balance - nativeOut, which scaled is⌊(balance - nativeOut) × rate⌋
These are not the same. Integer division is not distributive over subtraction at rounding boundaries:
⌊balance × rate⌋ - ⌊nativeOut × rate⌋ ≠ ⌊(balance - nativeOut) × rate⌋The left side is what the pool stored (subtracting the floor-rounded amount). The right side is what the pool’s actual balance produces when scaled (floor of the new balance times rate). At rounding boundaries, the right side is 1 unit smaller than the left. The stored D is computed from a scaled balance that is 1 unit too high, so the stored D exceeds the D the pool’s actual balances support.
This gives us a purely pool-level invariant:
The pool’s stored invariant D must not exceed the D its actual balances support.
// poolInvariants.qnt
val poolInvariantDSound: bool = {
if (getVirtualSupply(pool) == 0) true
else pool.invariantD <= scaledInvariant(pool)
}where scaledInvariant(pool) recomputes D fresh from the pool’s current native balances scaled by their rates:
pure def scaledInvariant(state: PoolState): int = {
val scaledBalances = scaleBalancesByRate(state.balances, state.tokenRates)
calculateInvariant(state.amp, scaledBalances)
}Why it fires for the bug. After a wstETH exit with amount 12:
// balance = 10e18, rate = 1.15, nativeOut = 12
scaledAmountOut (buggy) = ⌊12 × 1.15⌋ = 13
pool.invariantD = D(wstETH: 11.5e18 - 13) ← stored using buggy floor
// scaledInvariant rescales the actual post-exit native balance from scratch:
scaledInvariant(pool) = D(wstETH: ⌊(10e18 - 12) × 1.15⌋)
= D(wstETH: ⌊9999999999999999988 × 1.15⌋)
= D(wstETH: ⌊11499999999999999986.2⌋)
= D(wstETH: 11.5e18 - 14) ← one less than stored
pool.invariantD > scaledInvariant(pool) → VIOLATIONWhy it holds for WETH exits. WETH has rate 1, so mulDown(amount, 1e18) = amount exactly, no rounding boundary exists. The stored D and the recomputed D are always equal.
Why it holds for the correct implementation. With mulUp, scaledAmountOut = ⌈12 × 1.15⌉ = 14. Then:
pool.invariantD = D(wstETH: scaled_balance - 14)
scaledInvariant(pool) = D(wstETH: ⌊(balance - 12) × 1.15⌋)
= D(wstETH: scaled_balance - 14)
pool.invariantD ≤ scaledInvariant(pool) → HOLDSRunning the Simulator#
With the invariant in place, running the Quint simulator requires no special setup:
quint run poolInvariants.qnt \
--invariant=poolInvariantDSound \
--max-steps=5 --max-samples=100 --backend=typescriptThe step action nondeterministically picks a user, a token, and an amount:
action step = {
nondet user = oneOf(USERS)
nondet tokenOut = oneOf(Set(WETH, wstETH))
nondet amount = oneOf(Set(12, 13, 34, 99, 111))
swapBptGivenOutToInternal(user, tokenOut, amount)
}The amounts are chosen to include non-multiples of 20 (where amount × 1.15 is not an integer and the rounding gap fires for wstETH). WETH exits are included so the simulator can find paths that should not violate the invariant, confirming it is bug-specific and not just “any exit fires it.”
Result:
[violation] Found an issue (41ms at 24 traces/second).
The counterexample has two steps: one WETH exit (no violation — rate 1, no rounding), then one wstETH exit with amount 99 (not divisible by 20 → rounding fires → stored D exceeds actual D).
Note that the model has no vault, no internal balances, and no toInternalBalance flag. The vault and its internal balance mechanism are what make the bug exploitable for profit in practice: they allow the gap between pool accounting and token credits to accumulate and be withdrawn. But the bug itself (a stored D that no longer reflects the pool’s actual balances) is a pool-level self-inconsistency that exists regardless of vault interaction. poolInvariantDSound catches it without any cross-component reasoning.
To confirm the invariant is bug-specific and not just “any exit violates it,” we run a WETH-only step:
quint run poolInvariants.qnt \
--invariant=poolInvariantDSound \
--step=stepWethOnly \
--max-steps=20 --max-samples=500 --backend=typescript
[ok] No violation found (26568ms at 19 traces/second).500 traces × 20 steps, all WETH exits, no violation. The invariant is precisely sensitive to the rate-rounding boundary.
Lessons Learned: Modeling DeFi Protocols in Quint#
1. The right invariant comes from what the code stores, not what it computes#
The breakthrough came from asking: after a buggy swap, what is in the pool’s state that should not be there? The answer was that pool.invariantD (a stored value) no longer reflected the pool’s actual balances. The invariant poolInvariantDSound follows directly from that observation: the stored D should be consistent with the actual D. It requires no knowledge of the attack, no ghost variables, and no comparison to vault state. The most useful invariants often come from storage consistency: the requirement that a cached or stored value remains faithful to what it represents.
2. Accidental compensation is a stronger signal than a found bug#
Discovering that _calcBptInGivenExactTokensOut accidentally cancels the _upscale rounding error is arguably more valuable than the invariant violation itself. It explains why the bug was not caught by standard pool-level testing, and it tells you where to look: any code path where the compensating mulUp is absent. In a live system, that path was toInternalBalance: true swaps, where the vault credits the user independently of the pool’s scaled accounting. Finding accidental compensation in a code review is a strong signal to enumerate the alternative paths.
3. Pool-level modeling is sufficient to detect the bug#
The full exploit required vault interaction: the attacker needed internal balances to accumulate the gap profitably. But the bug itself, the discrepancy between stored D and actual D, is observable purely at the pool level. This is practically useful: the smaller and more focused the model, the faster the simulator runs and the easier the invariant is to understand. Start with the smallest model that can express the property.
4. Model what the code does, not what it should do#
Our upscale function in the model is:
pure def upscale(nativeAmount: int, scalingFactor: int): int =
mulDown(nativeAmount, scalingFactor) // mirrors Solidity — bug includedA model that uses mulUp here (the “correct” behavior) would never find the bug. The model’s job is to faithfully represent what the code does, including its rounding choices and its mistakes. This is a different discipline from verification against a specification: you are not checking “does the code match a correct spec?” but “does what the code does satisfy the invariants?” To do that, the model must be the code.
5. Test that invariants are specific, not just that they fire#
The “D should not decrease” invariant also fires, but for any BPT → wstETH exit, not just buggy ones, because D legitimately drops whenever liquidity is removed. An invariant that fires for correct behavior is not useful for bug detection. After finding a violation, run the invariant against a “clean” variant of the step (in our case, WETH-only exits) to confirm it holds where it should. Specificity is as important as sensitivity.
Conclusions#
The Balancer V2 bug was not simply a case of using the wrong rounding function. It was a bug whose effect was silently cancelled by an unrelated mulUp in the BPT charge computation, making it invisible to pool-level accounting checks. The exploit required a specific code path (the vault’s internal balance mechanism) where that cancellation did not apply.
What makes the Quint model result surprising is that the bug is detectable without modeling the vault at all. The rounding error leaves a trace in the pool’s own state: the stored invariant D becomes inconsistent with the D the pool’s actual balances support. That inconsistency is exactly what poolInvariantDSound checks. It is a natural property (the pool’s cached value should not exceed what the pool actually has) and it fires immediately for the buggy code and holds for the correct implementation.
The broader point: formal models surface the structure of a vulnerability by making the model’s assumptions explicit. Here, the key assumption was that pool.invariantD faithfully reflects the pool’s scaled balances. The bug violates that assumption. Once you state it as an invariant, the simulator finds the violation in under 50ms. For any StableSwap pool with rate-bearing tokens, checking that the stored invariant D is consistent with the pool’s actual scaled balances is a natural property to add to a model and it requires no knowledge of any specific exploit to state.
The Quint model is available in our repository for anyone who wants to explore it, run the simulator, or adapt the patterns to their own protocol.