Balancer ReClamm Swap Rounding Invariant

Balancer is an automated market maker protocol for programmable liquidity pools. ReClamm is one of its Balancer v3 two-token pool designs: it combines real balances with virtual balances so liquidity can be concentrated and readjusted over time. The swap quote is computed by onSwap, which calls into ReClammMath for exact-in and exact-out swaps.

Why this matters

ReClamm prices swaps using the product (balanceA + virtualBalanceA) * (balanceB + virtualBalanceB). Exact-in swaps must round output down. Exact-out swaps must round input up. If either direction rounded in the trader's favor, repeated swaps could extract value from the pool.

How this was modeled and proven

We modeled the ReClamm swap quote in Verity, LFG Labs' language for writing executable smart-contract models and proving properties about them in Lean 4. The model keeps the swap branch structure close to the Solidity source. The exact-in branch follows computeOutGivenIn and its Solidity division, which rounds the output down. The exact-out branch follows computeInGivenOut and calls the modeled mulDivUp helper, matching Balancer's ceiling-rounded input calculation.

The source model is in Contract.lean. The invariant is stated in Specs.lean using the same helpers shown above: L_before and L_after.

The proof first extracts the returned quote from the executable hRun. It then proves the floor inequality for exact-in swaps and the ceiling inequality for exact-out swaps. The last step is arithmetic over natural numbers: applying the real balance deltas cannot reduce the product.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.Balancer.ReClammSwapRounding.Compile

Proof status

Proven. The ReClamm case has one theorem and one spec. The reference proof compiles with no sorry, no admit, and no axiom.

Assumptions

The theorem uses these hypotheses. They are explicit proof boundaries, not axioms.

• hTokenPair(indexIn, indexOut) is either (0, 1) or (1, 0)

  ReClamm two-token pool design

  This is the valid route condition for a ReClamm two-token pool: token A to token B, or token B to token A. A production swap entering this pool is already in one of these two cases; the scalar Verity model keeps it explicit because token indexes are raw inputs.

• hNoOverflowthe successful Solidity arithmetic path does not overflow

  Solidity 0.8 checked arithmetic

  This bundles the five concrete overflow checks used by the proof: the token-A total, token-B total, exact-in denominator, exact-in numerator, and exact-out numerator. If any of these operations overflowed in Solidity, the swap quote would revert instead of returning a successful amount. The proof uses this bundle to compare Verity's executable Uint256 execution with ordinary natural-number arithmetic.

• hRunonSwap returns success amountCalculatedScaled18

  Executable Verity model

  The theorem is about successful quotes. If a require fails, the swap reverts and there is no returned amount to apply.

View specs in LeanView proofs in Lean

Learn more

Upstream Solidity source: ReClammPool.sol and ReClammMath.sol.

Certora report: April 15, 2025 ReClamm formal verification report.

Full case directory in the Verity benchmark repository.

What is a formal proof? A short explanation for non-specialists.