Nexus Mutual Book Value Invariant

Nexus Mutual is a decentralized insurance protocol. Members pool ETH into a shared capital pool, and that pool pays out claims when covered smart contracts are exploited. The NXM token represents membership and a share of the pool's value.

The RAMM (Risk-Adjusted Market Maker) is a separate on-chain pool that handles NXM trading. It holds its own ETH reserve (target: 5,000 ETH), distinct from the capital pool, and prices trades against book value: the capital pool's total capital divided by NXM supply. Buy and sell prices are derived from virtual reserves that converge toward book value ±1% via a time-based ratchet. During convergence the spread can be wider than 1%, but the invariant always holds: sell price never exceeds book value, and buy price never drops below it.

View source contract

Why this matters

If the sell price exceeded book value, anyone could buy NXM cheap and sell it back at a profit, draining the RAMM's own ETH reserve (the trading pool).

The damage wouldn't stop at the trading pool. When the RAMM's reserve drops below its 5,000 ETH target, adjustEth automatically refills it from the capital pool (the insurance pool) at up to 100 ETH per day. A sustained arbitrage would therefore drain not just the RAMM, but the capital pool that pays out members' insurance claims.

How this was proven

The calculateNxm function uses branching logic with non-linear uint256 arithmetic: scaling reserves, computing ratchet convergence terms, and comparing products to decide between book-value pricing and ratchet pricing. Standard testing cannot cover all input combinations.

The contract logic was modeled in Verity. The model captures both branches of calculateNxm for buy and sell sides, matching the Solidity's division ordering exactly. The theorem was given to AI agents as a benchmark task and solved.

The proof is checked by Lean 4's kernel, a small program that accepts or rejects proofs deterministically. If the proof were wrong, it would not compile.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.NexusMutual.RammPriceBand

Note: the proof required discovering a tight threshold for the sell-side invariant. Integer division truncation means the property only holds when eth × supply / capital ≥ 99. Below that (at 98), a machine-checked counterexample exists.

Hypotheses

Trust assumption: capital and supply are correct. These come from onchain oracles and token accounting. The proof takes them as given inputs and does not verify oracle correctness.

Given that, the theorem requires these hypotheses:

• hEtheth ≠ 0

  RAMM design invariant

  The current ETH reserve passed to calculateNxm is positive. Both buy and sell spot prices are computed as 1e18 × eth / nxmReserve, so a zero ETH reserve would make pricing undefined. The RAMM targets ~5,000 ETH via adjustEth.

• hOldEtholdEth ≠ 0

  RAMM design invariant

  The previous ETH reserve was positive. Both calculateBuyReserve and calculateSellReserve begin by scaling the old NXM reserve to the current ETH level: scaledReserve = oldNxm × eth / oldEth. Division by zero here would make the scaled reserve undefined.

• hSupplysupply ≠ 0

  NXM base assumption

  NXM total supply is positive. Book value is 1e18 × capital / supply, and the convergence check in both branches compares against eth × supply. Always true after NXM's initial distribution.

• hCapitalcapital ≠ 0

  Pool base assumption

  The protocol's capital pool has value. Used to compute the buffered capital targets: capital × 10100 / 10000 for buy (BV + 1%) and capital × 9900 / 10000 for sell (BV − 1%). A zero capital would collapse both price targets to zero.

• hRealisticScalecapital ≥ 100 ∧ eth × supply / capital ≥ 99

  Realistic operating range

  Only needed for the sell side. At very small values (wei scale), integer division loses enough precision that the sell price can exceed book value, for example with eth=20, capital=13, supply=4. These thresholds are the tightest bounds where the invariant still holds: 100 wei is ~10⁻¹⁶ ETH. With real values (capital ~200k ETH, supply ~7M NXM), these ratios are on the order of 10¹⁸.

The theorem also requires hNoOverflow hypotheses (not listed individually). Solidity's uint256 wraps around at 2²⁵⁶. If an intermediate multiplication overflowed, the wrapped result would be meaningless and the invariant could break. These hypotheses assert that every intermediate product in calculateNxm stays below 2²⁵⁶. With Nexus Mutual's capital pool at ~200k ETH (~2⁸⁸ wei), the largest products reach ~2¹⁷⁶, far below the limit.

View in LeanNexus Mutual contracts

Learn more

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