From 0acd8fc1b89fe773125a150ed388db8d71bccc2a Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 10 Apr 2026 11:38:30 +0100 Subject: [PATCH 1/3] Add Nexus Mutual book value invariant article Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/NexusMutualGuarantee.jsx | 137 +++++++ data/research.js | 9 + pages/research/nexus-mutual-book-value.jsx | 369 +++++++++++++++++++ 3 files changed, 515 insertions(+) create mode 100644 components/research/NexusMutualGuarantee.jsx create mode 100644 pages/research/nexus-mutual-book-value.jsx diff --git a/components/research/NexusMutualGuarantee.jsx b/components/research/NexusMutualGuarantee.jsx new file mode 100644 index 0000000..27f6962 --- /dev/null +++ b/components/research/NexusMutualGuarantee.jsx @@ -0,0 +1,137 @@ +import { useState, useEffect, useRef } from 'react' +import katex from 'katex' +import { ExternalLinkIcon } from './ExternalLink' + +function K({ tex }) { + const html = katex.renderToString(tex, { throwOnError: false }) + return +} + +function Term({ tex, label, detail, align = 'center' }) { + const posClass = + align === 'left' + ? 'left-0' + : align === 'right' + ? 'right-0' + : 'left-1/2 -translate-x-1/2' + + return ( + + + + + + + {label} +
+ {detail} + + + + ) +} + +export default function NexusMutualGuarantee() { + const [showEnglish, setShowEnglish] = useState(true) + const timerRef = useRef(null) + + useEffect(() => { + timerRef.current = setTimeout(() => setShowEnglish(false), 5000) + return () => clearTimeout(timerRef.current) + }, []) + + const handleToggle = () => { + if (timerRef.current) { + clearTimeout(timerRef.current) + timerRef.current = null + } + setShowEnglish((prev) => !prev) + } + + return ( +
+ + +
+
+ + + + + + + +
+
+

+ The RAMM never sells NXM below book value, and never buys it back + above book value. +

+
+
+ +
+ + View Lean + + +
+
+ ) +} diff --git a/data/research.js b/data/research.js index e793009..35d936f 100644 --- a/data/research.js +++ b/data/research.js @@ -1,4 +1,13 @@ export const research = [ + { + slug: 'nexus-mutual-book-value', + title: 'Nexus Mutual Book Value Invariant', + subtitle: 'A formally verified price band property of the RAMM.', + description: + 'How we proved the book value invariant of Nexus Mutual\'s RAMM pricing mechanism using Verity and Lean 4.', + date: '2026-04-09', + tag: 'Case study' + }, { slug: 'formalizing-transaction-interpretation', title: 'Formalizing Transaction Interpretation', diff --git a/pages/research/nexus-mutual-book-value.jsx b/pages/research/nexus-mutual-book-value.jsx new file mode 100644 index 0000000..31a4a0a --- /dev/null +++ b/pages/research/nexus-mutual-book-value.jsx @@ -0,0 +1,369 @@ +import Head from 'next/head' +import Link from 'next/link' +import PageLayout from '../../components/PageLayout' +import ResearchCard from '../../components/ResearchCard' +import NexusMutualGuarantee from '../../components/research/NexusMutualGuarantee' +import Disclosure from '../../components/research/Disclosure' +import CodeBlock from '../../components/research/CodeBlock' +import ExternalLink from '../../components/research/ExternalLink' +import { research } from '../../data/research' + +function Hypothesis({ name, constraint, source, children, border = true }) { + return ( +
  • +
    + + + + + {name} + {constraint} + +
    +

    + + {source} + +

    +

    {children}

    +
    +
    +
    • + ) +} + +const VERIFY_COMMAND = `git clone https://github.com/lfglabs-dev/verity-benchmark +cd verity-benchmark +lake build Benchmark.Cases.NexusMutual.RammPriceBand` + +export default function NexusMutualBookValuePage() { + const otherResearch = research.filter( + (r) => r.slug !== 'nexus-mutual-book-value' + ) + + return ( + <> + + + Nexus Mutual Book Value Invariant | Research | LFG Labs + + + + + +
    + + +
    +

    + Nexus Mutual Book Value Invariant +

    +
    + + {/* The Guarantee */} +
    + +

    + Nexus Mutual's RAMM (Risk-Adjusted Market Maker) prices NXM + token trades against a book value anchor: the protocol'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 */} +
    +

    + Why this matters +

    +

    + If the sell price exceeded book value, anyone could buy NXM + cheap and sell it back to the RAMM at a profit, draining the + RAMM's ETH reserve. +

    +

    + The damage wouldn't stop there. When the RAMM's + reserve drops below its 5,000 ETH target,{' '} + adjustEth{' '} + automatically refills it from the capital pool at up to 100 ETH + per day. A sustained arbitrage would therefore drain not just the + RAMM, but the capital pool that backs every insurance claim on + the protocol. +

    + +

    + This proof covers the price band arithmetic in both branches of{' '} + calculateNxm: + when the ratchet has converged (BV branch) and when it's + still converging (ratchet branch). +

    +

    + Several parts of the RAMM are not modeled because they + don't affect price computation.{' '} + TWAP oracle observes prices but never feeds + back into{' '} + calculateNxm.{' '} + Circuit breakers limit trade volume per period + but don't change how prices are calculated.{' '} + Access control ( + whenNotPaused,{' '} + nonReentrant) + are on/off guards on a permissionless function, not price + logic. +

    +

    + + adjustEth + {' '} + and swap execution are already covered: the + proof takes{' '} + eth,{' '} + oldEth, and old + NXM reserves as free parameters, so any post-swap or + post-adjustment state is included. +

    +

    + Oracle correctness, whether{' '} + + pool.getPoolValueInEth() + {' '} + returns the true pool value, is the main thing not covered. It + requires modeling{' '} + Pool.sol, + Chainlink feeds, and multi-asset conversion: a different proof + scope entirely. +

    +     +
    + + {/* How this was proven */} +
    +

    + 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. +

    + + {VERIFY_COMMAND} +

    + If the build succeeds, the proof is correct.{' '} + + Source repository + +

    +     +

    + 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 */} +
    +

    + Hypotheses +

    +

    + The proof uses zero axioms. The theorem requires these + hypotheses, which encode assumptions about valid protocol states: +

    +
      + + 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. + + + 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. + + + 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. + + + 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. + + + 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−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. +

    +

    + + View in Lean + + + Nexus Mutual contracts + +

    +
    + + {/* Learn more */} +
    +

    + Learn more +

    +

    + + What is a formal proof? + {' '} + A short explanation for non-specialists. +

    +
    + + {otherResearch.length > 0 && ( +
    +

    + More research +

    +
    + {otherResearch.map((r) => ( + + ))} +
    +
    + )} +
    +     + + ) +} From 6a95a22ccde84c36f940e318976e8825783e2cc7 Mon Sep 17 00:00:00 2001 From: Fricoben Date: Fri, 10 Apr 2026 14:08:48 +0100 Subject: [PATCH 2/3] Refine article disclosure, hypotheses, and copy Co-Authored-By: Claude Opus 4.6 (1M context) --- pages/research/nexus-mutual-book-value.jsx | 64 ++++++++++------------ 1 file changed, 28 insertions(+), 36 deletions(-) diff --git a/pages/research/nexus-mutual-book-value.jsx b/pages/research/nexus-mutual-book-value.jsx index 31a4a0a..087e27d 100644 --- a/pages/research/nexus-mutual-book-value.jsx +++ b/pages/research/nexus-mutual-book-value.jsx @@ -123,46 +123,31 @@ export default function NexusMutualBookValuePage() {

    - This proof covers the price band arithmetic in both branches of{' '} + The proof covers every code path through{' '} calculateNxm: - when the ratchet has converged (BV branch) and when it's - still converging (ratchet branch). -

    -

    - Several parts of the RAMM are not modeled because they - don't affect price computation.{' '} - TWAP oracle observes prices but never feeds - back into{' '} - calculateNxm.{' '} - Circuit breakers limit trade volume per period - but don't change how prices are calculated.{' '} - Access control ( - whenNotPaused,{' '} - nonReentrant) - are on/off guards on a permissionless function, not price - logic. -

    -

    - - adjustEth - {' '} - and swap execution are already covered: the - proof takes{' '} - eth,{' '} - oldEth, and old - NXM reserves as free parameters, so any post-swap or - post-adjustment state is included. + 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.

    - Oracle correctness, whether{' '} + The guarantee depends on{' '} + capital and{' '} + supply being + correct. These come from{' '} pool.getPoolValueInEth() {' '} - returns the true pool value, is the main thing not covered. It - requires modeling{' '} - Pool.sol, - Chainlink feeds, and multi-asset conversion: a different proof - scope entirely. + 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.

    @@ -221,8 +206,15 @@ export default function NexusMutualBookValuePage() { Hypotheses

    - The proof uses zero axioms. The theorem requires these - hypotheses, which encode assumptions about valid protocol states: + 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:

      Date: Fri, 10 Apr 2026 15:44:19 +0100 Subject: [PATCH 3/3] Clarify RAMM vs capital pool distinction and guarantee wording Co-Authored-By: Claude Opus 4.6 (1M context) --- components/research/NexusMutualGuarantee.jsx | 4 +-- pages/research/nexus-mutual-book-value.jsx | 38 ++++++++++++-------- 2 files changed, 25 insertions(+), 17 deletions(-) diff --git a/components/research/NexusMutualGuarantee.jsx b/components/research/NexusMutualGuarantee.jsx index 27f6962..ab50091 100644 --- a/components/research/NexusMutualGuarantee.jsx +++ b/components/research/NexusMutualGuarantee.jsx @@ -115,8 +115,8 @@ export default function NexusMutualGuarantee() { aria-hidden={!showEnglish} >

      - The RAMM never sells NXM below book value, and never buys it back - above book value. + The Nexus Mutual liquidity pool never sells NXM below book value, + and never buys it back above book value.

      diff --git a/pages/research/nexus-mutual-book-value.jsx b/pages/research/nexus-mutual-book-value.jsx index 087e27d..8297a48 100644 --- a/pages/research/nexus-mutual-book-value.jsx +++ b/pages/research/nexus-mutual-book-value.jsx @@ -87,13 +87,21 @@ export default function NexusMutualBookValuePage() {

      - Nexus Mutual's RAMM (Risk-Adjusted Market Maker) prices NXM - token trades against a book value anchor: the protocol'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. + 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.

      @@ -109,17 +117,17 @@ export default function NexusMutualBookValuePage() {

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

      - The damage wouldn't stop there. When the RAMM's - reserve drops below its 5,000 ETH target,{' '} + 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 at up to 100 ETH - per day. A sustained arbitrage would therefore drain not just the - RAMM, but the capital pool that backs every insurance claim on - the protocol. + 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.