+ The Nexus Mutual liquidity pool never sells NXM below book value, + and never buys it back above book value. +
+{name}
+ {constraint}
+ + + {source} + +
+{children}
++ 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. +
+
+
+ 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.
+
+ The proof covers every code path through{' '}
+ calculateNxm:
+ both the BV branch (ratchet has converged, prices snap to book
+ value ±1%) and the ratchet branch (still converging, prices
+ move gradually). It holds for any value of the reserve and
+ timing inputs, which means any sequence of swaps, ETH
+ adjustments, or elapsed time is included.
+
+ The guarantee depends on{' '}
+ capital and{' '}
+ supply being
+ correct. These come from{' '}
+
+ pool.getPoolValueInEth()
+ {' '}
+ and{' '}
+
+ tokenController.totalSupply()
+
+ , which the proof takes as trusted inputs. If those values were
+ wrong (e.g. a Chainlink oracle returning a stale price), the
+ book value itself would be wrong, and the price band would
+ anchor to the wrong number. Oracle correctness is a separate
+ verification scope.
+
+ 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{' '}
+ 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. +
+
+ If the build succeeds, the proof is correct.{' '}
+
+ 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. +
+
+ 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: +
+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.
+
+ 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.
+
+ 1e18 × capital / supply
+
+ , and the convergence check in both branches compares against{' '}
+
+ eth × supply
+
+ . Always true after NXM's initial distribution.
+
+ 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.
+
+ eth=20, capital=13, supply=4
+
+ . These thresholds are the tightest bounds where the invariant
+ still holds: 100 wei is ~10−16 ETH. With real
+ values (capital ~200k ETH, supply ~7M NXM), these ratios are
+ on the order of 1018.
+
+ The theorem also requires{' '}
+ hNoOverflow{' '}
+ hypotheses (not listed individually). Solidity's{' '}
+ uint256 wraps
+ around at 2256. 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 2256. With Nexus Mutual's capital
+ pool at ~200k ETH (~288 wei), the largest products
+ reach ~2176, far below the limit.
+
+
+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +
+