The ten invariants (I1–I10)

Every protocol invariant — precise statement, why it holds, where it is enforced, and how it is verified by Foundry fuzz — plus the senior-protection structural invariant that backs the junior-first-loss waterfall.

Inflexion’s safety is not a story about good intentions — it is ten machine-checked invariants, each one a precise predicate over the contract state, each one enforced in the contracts and exercised by Foundry fuzz over the whole price domain. The settle-path set I1–I9 is unchanged from before the v4.0 hybrid pivot; I10 is the price cap, added upstream of settle and orthogonal to the rest.

This page gives each invariant the full treatment: what it says, why it is true at the formula and code level, exactly where it is enforced, and the test that proves it. It closes with the senior-protection structural invariant — not numbered I1–I10, but central to the trust story for the tranches.

The one structural fact everything else hangs on: in FULL mode collateral is locked at MaxIL and coverage is min(realized_IL, MaxIL), so payout ≤ collateral by construction (I1/I2). That proof is oracle-independent — it holds under any price path. See the no-bad-debt math and MaxIL.

The ten at a glance

ID	Statement	Where enforced	Verified by
I1	No bad debt (FULL): $\text{payout} \le \text{collateral} = \text{MaxIL}$	InflexionCore cap; vaults re-check payout ≤ lockedAmount in ConvexityVault and UnderwriterVault	testFuzz_I1_I2_payoutCappedAtMaxIL (256 runs)
I2	Cap correctness: $\text{payout} = \min(\text{realized\_IL}, \text{MaxIL})$	InflexionCore settle	same fuzz as I1
I3	Non-negativity / no underflow (guarded subtraction)	ILMath	testFuzz_I3_ilNonNegative (256 runs)
I4	LP never profits from the swap: $V_{lp} \ge V_{hold} \Rightarrow \text{payout} = 0$	ILMath (the : 0 arm)	test_il_atEntryIsZero + I3 fuzz
I5	Vault solvency: $\text{locked} \le \text{deposited}$ per MM; $\text{totalLocked} \le \text{juniorAssets}$ for the pool	UnderwriterVault; ConvexityVault	invariant_I5_lockedLeDeposited (256 runs × 128k calls × 0 reverts)
I6	Liquidity immutability: settle uses L stored at creation	InflexionCore create and settle paths	testFuzz_I6_settleUsesStoredLiquidity + the F-2 e2e test
I7	Capacity authority: $\text{consumedNotional}[\text{quoteId}] \le \text{maxNotionalV0}$; a cancelled bit cannot fill	InflexionCore; router reads only	test_createSwap_consumedNotional_tracked + _rejectsUsedNonce
I8	Settlement liveness (Fork 1): settle() always succeeds within the window	OracleManager.getSettlementPrice backstop	5 fuzz tests, ~1,280 runs
I9	Band enforcement (Fork 2): createSwap reverts iff $\lvert\text{bps}(P_{live}, \text{quotePrice})\rvert > \text{priceBandBps}$ (Path B only)	InflexionCore band check	testFuzz_I9_priceBandViolationReverts + _withinBandAccepts (256 each)
I10	Price cap (launch): $\text{premium} \le \text{FairPremium}\cdot(1 + \text{maxLoadBps})$ on both paths, by construction	Path A clamp in CvammPricing; Path B require in InflexionCore	testFuzz_I10_clamp + invariant-suite assertion

LPs are always paid with no bad debt in FULL mode — qualified: capped payoff + solvent USDC + oracle/settlement liveness.

The no-bad-debt guarantee is exact only under the full clause:

• FULL collateralization — the underwriter has posted exactly MaxIL per swap, locked for the life of the position.
• Capped payoff — the payout is min(realized_IL, MaxIL). The cap is load-bearing: it is what makes payout ≤ collateral hold by construction.
• Solvent USDC — the collateral numeraire (dUSDC) holds its peg and remains redeemable.
• Oracle / settlement liveness — the price oracle stays live and settle() runs within the protocol’s settlement window.
• No rehypothecation breach — locked collateral stays instantly liquid; it is never routed to utilization-gated venues.

Stated without these qualifiers, the guarantee is not correct.

---

I1 — No bad debt (FULL): payout ≤ collateral == MaxIL

1. Statement

   In FULL mode the LP’s payout can never exceed the collateral the underwriter locked, because that collateral was set to MaxIL and the payout is capped at MaxIL:

   $\text{payout} \;\le\; \text{collateral} \;=\; \text{MaxIL}.$

2. Why it holds

   Two facts compose. Coverage is $\text{payout} = \min(\text{realized\_IL}, \text{MaxIL})$, so $\text{payout} \le \text{MaxIL}$ for any price path. And in FULL mode the locked collateral is MaxIL. Therefore $\text{payout} \le \text{MaxIL} = \text{collateral}$. This is structural, not heuristic — provable by fuzz over the whole price domain (in-range, below Pa, above Pb, and the no-IL region). Crucially it is oracle-independent: settle caps the payout at MaxIL == collateral regardless of any pricing oracle, so the FairValue and Vol oracles are not load-bearing for I1.

3. Where enforced

   The payout cap is the ternary in settle:

   uint128 payout = realisedIL > s.maxIL ? s.maxIL : uint128(realisedIL);
   

   Collateral was locked at MaxIL at creation on both Path A and Path B. Both vaults defensively re-check payout ≤ lockedAmount at release in ConvexityVault and UnderwriterVault, so the cap is enforced twice.

4. How verified

   testFuzz_I1_I2_payoutCappedAtMaxIL — 256 runs, asserting payout ≤ maxIL across the full price domain.

I1 is one of two never-merged claims. Claim A (LPs are always paid, FULL, code-enforced) is structural. Claim B (depositors/MMs can lose principal) is a separate fact — see the tranches and <ClaimB /> below.

---

I2 — Cap correctness: payout == min(realized_IL, MaxIL)

1. Statement

   $\text{payout} = \min(\text{realized\_IL}, \text{MaxIL}).$ The payout is exactly the cap applied to the recomputed IL — never more, never less, never caller-influenced.

2. Why it holds

   The same line that enforces I1 is the min. The decisive detail is the input: realized_IL is recomputed on-chain at settle from the Chainlink-pinned settlement price, never caller-supplied. The settlement sqrt price is derived on-chain via _oracleSqrtPriceX96 from the Chainlink round-at-T, not from calldata. This closes the hole where a permissionless settler could otherwise set the payout anywhere in [0, MaxIL]. See price pinning.

3. Where enforced

   computeIL over the oracle-pinned price in InflexionCore settle, then the cap ternary.

4. How verified

   The same fuzz as I1, testFuzz_I1_I2_payoutCappedAtMaxIL: it asserts the payout equals the capped IL, not merely that it is bounded.

---

I3 — Non-negativity / no underflow

1. Statement

   $\text{realized\_IL} = \begin{cases} V_{hold} - V_{lp} & V_{hold} > V_{lp} \\ 0 & \text{otherwise}\end{cases}$ — never an unchecked subtraction.

2. Why it holds

   The IL kernel uses a guarded ternary, so the subtraction is only ever evaluated when V_hold > V_lp. (Note: assert(payout >= 0) is vacuously true on uint256; the real content is that the subtraction is guarded, and the fuzzer drives V_lp > V_hold cases asserting no-revert and payout == 0.)

3. Where enforced

   return V_hold > V_lp ? V_hold - V_lp : 0; // I3: guarded subtraction
   
4. How verified

   testFuzz_I3_ilNonNegative — 256 runs, including price paths where the LP would have out-performed hold.

---

I4 — LP never profits from the swap

1. Statement

   $V_{lp} \ge V_{hold} \;\Rightarrow\; \text{realized\_IL} = 0 \;\Rightarrow\; \text{payout} = 0.$ The LP is made whole, never more — the swap is a hedge, not a lottery.

2. Why it holds

   The same guarded clamp as I3: when the LP would have profited versus passively holding, IL is zero, so the payout is zero. Settlement uses the oracle-pinned $P_T$, so the outcome reflects the true price, not a settler-chosen one — which restores I4 alongside I2. This is about the payout only; the LP still earns Uniswap fees on the custodied position, so total P&L can be positive. That is correct, not a leak — Inflexion hedges gross in-range IL, not net P&L. See the IL formula.

3. Where enforced

   ILMath — the : 0 arm of the guarded ternary.

4. How verified

   test_il_atEntryIsZero plus the I3 fuzz; the invariant suite asserts if (vLp >= vHold) payout == 0.

---

I5 — Vault solvency: locked ≤ deposited per MM (and totalLocked ≤ junior per pool)

1. Statement

   For every underwriter the locked collateral never exceeds what was deposited: $\text{locked}[\text{mm}] \le \text{deposited}[\text{mm}] \quad\text{(Path B)},\qquad \text{totalLocked} \le \text{juniorAssets} \quad\text{(Path A pool)}.$

2. Why it holds (by construction)

   lockCollateral requires $\text{available}(\text{mm}) = \text{deposited} - \text{locked} \ge \text{amount}$, so post-lock $\text{locked}' \le \text{deposited}$. releaseAndDistribute requires $\text{payout} \le \text{lockedAmount} \le \text{locked}$, so $\text{deposited}' - \text{locked}' \ge 0$ in UnderwriterVault. For the pool, freeAssets() = totalAssets − totalLocked and lockCollateral requires free ≥ amount in ConvexityVault; the pool analogue $\text{totalLocked} \le \text{juniorAssets}$ is the senior-protection invariant below.

3. Where enforced

   Path B: UnderwriterVault.lockCollateral (the avail < amount revert) and releaseAndDistribute. Path A: ConvexityVault free-asset accounting and the lock check.

4. How verified

   invariant_I5_lockedLeDeposited — recorded at 256 runs × 128,000 fuzzed vault-op calls × 0 reverts — plus testFuzz_I5_lockedNeverExceedsDeposited.

---

I6 — Liquidity immutability: settle uses L stored at creation

1. Statement

   Settlement computes IL with the liquidity L snapshotted at creation; an external increaseLiquidity on the custodied NFT cannot inflate payout above MaxIL.

2. Why it matters (attack F-2)

   The position NFT is held in protocol custody during the swap, but increaseLiquidity on a Uniswap v3 NFT is not owner-gated — anyone can call it. If settle re-read positions(tokenId).liquidity, an attacker could blow up the computed IL after creation. Storing L once neutralizes this entirely; the extra liquidity is simply returned with the NFT at settle.

3. Where enforced

   L is read exactly once in _prepareSwap and stored at execution on both Path A and Path B. Settle passes the stored s.liquidity to computeIL, never a re-read.

4. How verified

   testFuzz_I6_recordsStoredLiquidity + testFuzz_I6_settleUsesStoredLiquidity, plus the end-to-end testFuzz_F2_externalIncreaseLiquidity_arbitraryAmount, which mutates the on-chain L between create and settle and asserts payout unchanged.

---

I7 — Capacity authority: consumedNotional[quoteId] ≤ maxNotionalV0; a cancelled bit cannot fill

1. Statement

   The on-chain ledger is authoritative over the off-chain engine. A signed quote can fill repeatedly only up to its capacity, never after its nonce bit is cancelled, and concurrent submissions cannot over-consume. Path B only — Path A has no signed quote.

2. Why it holds

   Check-and-increment is atomic in one transaction, in PHASE 3 effects, before any external call. The capacity check (consumedNotional[quoteId] + g.V0 > maxNotionalV0 ⇒ revert) runs in PHASE 2; the atomic consumedNotional[quote.quoteId] += g.V0 and _useNonce(...) run together in _executePathB. Capacity is denominated in V0 (position value), not collateral. Nonces are a Permit2-style bitmap (nonce = word<<8 | bit), so an MM cancels one quote by flipping one bit — never cancel-all.

3. Router subtlety (also I7)

   In createSwapRouted, only the executed rail mutates nonce/capacity/lock. The router’s Path-B usability predicate _quoteUsableAndPremiumB is view: it reads isNonceUsed/consumedNotional but never calls _useNonce. A quote that loses the route consumes nothing.

4. Where enforced

   InflexionCore — the capacity mutation, the capacity check, and _useNonce.

5. How verified

   test_createSwap_consumedNotional_tracked + test_createSwap_rejectsUsedNonce.

Limit: full handler-driven stateful fuzz of the capacity ledger is deferred to post-mainnet. Why: stateful capacity fuzzing requires a dedicated quote-lifecycle handler that models concurrent fills and selective cancels — a larger harness than the current scope allowed. Mitigation: the atomic check-and-increment lives in a single transaction before any external call, so the race it would test for cannot occur within a transaction; the unit tests cover replay, used-nonce rejection, and capacity tracking directly. Stateful fuzz hardens confidence; it is not load-bearing for the property itself.

---

I8 — Settlement liveness (Fork 1): settle() always succeeds within the window

1. Statement

   For any swap, under any price path, settle() succeeds by $\text{expiry} + \text{LIVENESS\_WINDOW} + \text{MAX\_STALENESS} + \text{GRACE\_PERIOD}$ — the lone-spike check never permanently locks funds. This is the Fork 1 resolution.

2. Constants

   GRACE_PERIOD = 3600, LIVENESS_WINDOW = 86_400 (24h), LONE_SPIKE_BPS = 500 (5%) in OracleManager; MAX_STALENESS is per-token, Sepolia value 90,000s in the on-chain address registry.

3. Why it holds

   Settle pins the Chainlink round-at-T (unique, bracketed by updatedAt ≤ expiry). A glitched print — a “lone spike” differing from both neighbours by ≥ LONE_SPIKE_BPS — is deferred, but only until block.timestamp ≥ expiry + LIVENESS_WINDOW, after which the backstop accepts the round unconditionally. A missing neighbour round across a Chainlink phaseId boundary is read tolerantly via _tryRound (try/catch returning ok=false instead of reverting), so it degrades to the backstop rather than a permanent lock. A real fast move persists across rounds and passes the lone-spike check immediately.

4. Where enforced

   OracleManager.getSettlementPrice.

5. How verified

   The OracleManager invariant suite — 5 fuzz tests, ~1,280 runs: testFuzz_I8_settleSucceedsAnywhereInBackstopWindow, testFuzz_I8_sustainedMoveSettlesImmediately, testFuzz_I8_loneSpikeDefersBeforeBackstop, testFuzz_I8_sequencerRecoveryRespectsGrace, test_I8_revertsPastStaleness_boundary.

Limit / documented design observation (NOT a bug): the spec-literal staleness require fires before the backstop can recover the round, so the actual usable window is $[\text{expiry} + \text{LIVENESS\_WINDOW},\ \text{expiry} + \text{MAX\_STALENESS})$ ≈ 1 hour wide (90,000 − 86,400 = 3,600s), not the full additive sum the I8 wording suggests. Why: the staleness gate and the liveness backstop are two independent checks whose windows overlap by exactly one hour with the current constants. Mitigation: past expiry + MAX_STALENESS the round-at-T is stale, but funds can still settle via a newer Chainlink round (Arbitrum majors tick frequently), and the 1h window is symmetric for LP and MM, so fairness is preserved. Surfaced in OracleManager NatSpec and in a boundary test — not papered over.

---

I9 — Band enforcement (Fork 2): createSwap reverts iff drift exceeds the band

1. Statement

   A Path-B signed quote auto-voids on-chain, deterministically, iff the live oracle has drifted beyond the MM’s chosen band: $\text{createSwap reverts} \iff \lvert\text{bps}(P_{live}, \text{quotePrice})\rvert > \text{priceBandBps}.$ This is not last-look. Path A has no signed quote and thus no such vector — it prices off the live oracle directly. This is the Fork 2 resolution.

2. Bounds

   PRICE_BAND_MIN_BPS = 25 (0.25%), PRICE_BAND_MAX_BPS = 500 (5%), MM default 100 (1%) in InflexionCore.

3. Why it holds

   At createSwap the contract reads the live oracle price once — the same read that pins P0, so zero extra oracle cost, carried as g.livePrice — and checks $\lvert\text{bps}(P_{live}, \text{quote.quotePrice})\rvert \le \text{quote.priceBandBps}$. Beyond the band ⇒ revert. Because the check is deterministic with no MM discretion at fill, it is not last-look: the MM is exposed only to drifts within the band it chose (it priced for them), never to gaps that blow through it. Signed quotes are bearer instruments that survive past an off-chain cancel, so an on-chain band is the only sound defense. See no last-look.

4. Where enforced

   InflexionCore PHASE 2 band check: bandDevBps = oracle.absBps(g.livePrice, quote.quotePrice), then revert PriceOutOfBand. absBps is the pure helper in OracleManager. The single live read is in _prepareSwap. The router mirrors this as a non-reverting boolean.

5. How verified

   testFuzz_I9_priceBandViolationReverts + testFuzz_I9_priceBandWithinBandAccepts — 256 runs each, both directions.

---

I10 — Price cap (launch; by construction; upstream of settle)

1. Statement

   On both paths the charged premium can never exceed the fair value plus the maximum load: $\text{premium} \;\le\; \text{FairPremium}\cdot(1 + \text{maxLoadBps}).$ Overcharge is impossible by code, not by trust.

2. Why it holds (Path A)

   The load sum is a mechanical, deterministic clamp: $\text{total} = \min(\text{baseLoad} + \text{util\_skew} + \text{dispersion\_skew},\ \text{maxLoad}),$ so the premium ceiling holds for all sequences of states and all price paths (FULL and PARTIAL both), with no MM discretion and no graceful-degradation path. CvammPricing.totalLoadWad and loadComponents both apply the total > maxLoad ? maxLoad : total clamp; premiumFromLoad then computes $\lceil \text{FairPremium}\cdot(1+\text{total}) \rceil$. Wired in _pricePathAFromFair. See the load stack.

3. Why it holds (Path B)

   The premium is derived from the on-chain FairPremium, not streamed raw: $\text{premium} = \lceil \text{FairPremium}\cdot(1 + \text{loadBps}/10^4) \rceil$ with a hard require(loadBps ≤ maxLoadBps). The quote can only set a load over the published fair value, never the premium itself — the LoadExceedsMax revert and _pricePathB in InflexionCore.

4. Both paths also cap premium at MaxIL

   Neither path ever charges more than the max possible payout, on both Path A and Path B in InflexionCore.

5. How verified

   testFuzz_I10_clamp plus an invariant-suite assertion that charged ≤ fairPremium·(1e4 + maxLoadBps)/1e4.

Orthogonality: I10 lives in PHASE 1 (pricing, READ), strictly upstream of settle. It does not touch settle, the MaxIL formula, or I1–I9. The no-bad-debt proof (I1) is structural ($\text{collateral} = \text{MaxIL} \ge \text{payout}$) and always true by code, while I1 additionally depends on oracle/settlement liveness; I10 is always true by code with no liveness dependency. Neither the senior/junior premium split nor the totalLocked ≤ juniorAssets constraint affects I10 or settle semantics.

---

The senior-protection structural invariant (distinct from I5)

Not numbered I1–I10, but central to the trust story for the tranches and enforced in ConvexityVault:

$\text{totalLocked} \;\le\; \text{juniorAssets} \quad\text{at every } \texttt{lockCollateral}.$

1. Why it protects senior

   Since every payout $\le$ its MaxIL $=$ its locked amount, total payouts $\le \text{totalLocked} \le \text{juniorAssets}$. So the junior-first-loss waterfall absorbs all underwriting loss before senior is ever touched. The waterfall in releaseAndDistribute takes $\text{juniorLoss} = \min(\text{payout}, \text{juniorAssets})$ first and $\text{seniorLoss} = \text{payout} - \text{juniorLoss}$ only after; by the invariant the min is defense-in-depth — senior is never reached.

2. Where enforced

   ConvexityVault — the SeniorProtectionBreached revert in lockCollateral and the junior-first waterfall in releaseAndDistribute.

3. The adaptive-vs-fixed distinction

   This is the adaptive code form of the $u \le 1 - sf$ rule, keyed to the actual junior buffer (safer than a fixed ratio). The target tranche ratio $sf = 0.60$ is for UX/incentives, not the hard cap. With $sf = 0.60$, junior $= 1 - sf = 0.40$, so the invariant is exactly $u \le 0.40 = 1 - sf$.

4. Run defense

   Withdrawals are cooldown-gated (requestWithdrawal → withdraw after withdrawalCooldown) and junior cannot be withdrawn below totalLocked (the JuniorBelowLocked revert). The same locked/free accounting that prevents a run also drives util_skew up before the pool over-commits.

Limit: senior $P(\text{loss}) = 0$ is a calibration result, not a structural guarantee. Why: it holds only while $u \le 1 - sf$; the structural invariant $\text{totalLocked} \le \text{juniorAssets}$ guarantees senior is shielded from underwriting loss specifically, but never from the systemic tail (USDC depeg, oracle failure, contract bug). Mitigation: the invariant is enforced on every lock, the run defense keeps junior $\ge$ totalLocked, and the disclosure below is mandatory on every depositor surface. Capital-not-guaranteed is the umbrella for both tranches.

Depositor capital is NOT guaranteed: the junior tranche is first-loss; the senior tranche is structurally protected from underwriting loss only, not systemic tail.

Underwriting capital — whether supplied to the pooled cvAMM vault (Path A) or posted directly by a market maker (Path B) — is at risk:

• Junior tranche — first-loss. Junior depositors absorb underwriting losses first and buffer the senior tranche.
• Senior tranche — protected from underwriting loss, exposed to the systemic tail. The senior tranche is structurally shielded from ordinary underwriting loss while junior capital buffers, but it still takes the systemic tail once the junior buffer is exhausted.

No-bad-debt is a guarantee to the LP being paid (see the FULL-mode payout clause), not a guarantee that depositor or MM capital is preserved.

---

How these are checked, in one place

Foundry invariant fuzz — the headline number

The aggregate vault-solvency run is recorded at 256 runs × 128,000 fuzzed vault-op calls × 0 reverts for I5. I1/I2, I3, I6, I9, and I10 each run 256-run targeted fuzz; I8 runs 5 tests at ~1,280 runs total. The settle-path invariants are exercised over the whole price domain — in-range, below Pa, above Pb, and the no-IL region — not just the happy path.

Static analysis (Slither 0.11.5)

Two passes. The core pass produced 27 findings → 1 fixed (reentrancy-no-eth in settle, resolved by hoisting status = SETTLED before any external call) + 26 accepted false-positives. The cvAMM pass produced 74 results → 0 high, 0 confirmed vulnerabilities, 1 cleanup, with manual confirmation of the junior-first-loss waterfall, the run defense, and the lockedAfter ≤ juniorAssets senior-protection check. See audits and CEI / reentrancy.

Where the invariants are oracle-independent vs oracle-dependent

I1–I7 and the senior-protection invariant are structural — they hold by construction regardless of any pricing oracle. I8 depends on Chainlink/sequencer liveness (that is exactly the property it bounds). I9 depends on the live oracle read at create. I10 is a deterministic clamp with no liveness dependency. The FairValue and Vol oracles are load-bearing for I10 and depositor solvency, not for I1’s no-bad-debt guarantee.

Related reading

The no-bad-debt math

The formula-level proof behind I1/I2 — why payout ≤ collateral holds on every arm of the payoff.

The two architectural forks

The full Fork 1 (I8) and Fork 2 (I9) story: the deadlock and pickoff classes, and the chosen resolutions.

Price pinning

How on-chain Chainlink derivation of P0 and P_T closes the settler-chosen-price hole (restoring I2/I4).

Attack vectors

The attack ↔ mitigation ↔ invariant table mapping each audited vector to its enforcing invariant.