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 It 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 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

Hypotheses

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

• swap goes token A to B or token B to A

  ReClamm two-token pool design

  The swap indexes (indexIn, indexOut) are either (0, 1) or (1, 0): 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.

• the successful swap math does not overflow

  Solidity 0.8 checked arithmetic

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

• the swap quote succeeds

  Executable Verity model

  onSwap returns success with amountCalculatedScaled18. 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.