Invariants the protocol enforces, attack vectors it defends against, and what's been verified vs what's deferred. Companion to MATH.md (the formulas) and spec.md §13 (the canonical list).

CI scope: GitHub Actions (.github/workflows/ci.yml) runs only forge fmt + forge build + forge test. It does not run cargo / cargo stylus, the Node benchmark scripts, or the Python suite — so all Stylus and quant validation is manual (local Nitro / WSL2). The Solidity FairValueOracle is exercised in CI (it is what forge test compiles), which is why it is retained as the revm-executable cross-check of the shipped Stylus oracle.

All ten invariants from spec §13 with their verification status. Test references point to files in packages/contracts/test/.

Sourced from spec §9 + the external audit findings memory (inflexion-audit-findings, 12 fixes applied → spec v3.3, 2 forks resolved). The audit work is summarised in PR #5 + Phase 14.11.

These are NOT bugs — they're behaviours of the current implementation that differ from the most ambitious reading of the spec and that we've chosen to surface in NatSpec rather than paper over. Tracked for spec review.

Spec wording (§13 I8): "settle() always succeeds within expiry + LIVENESS_WINDOW + MAX_STALENESS + GRACE_PERIOD."

Implementation reality: the staleness require in spec §6.1's literal code fires before the backstop can recover the round. The actual usable settlement window is:

[ expiry + LIVENESS_WINDOW,  expiry + MAX_STALENESS )
≈ 1 hour wide  (86,400s → 90,000s with current constants)

Past expiry + MAX_STALENESS the pinned round is "stale" per the spec-literal check; funds can still be settled via a newer Chainlink round (Arbitrum majors tick frequently), but not via the round-at-T. The 1h window is symmetric for both LP and MM (preserves fairness), just tighter than the I8 wording suggests.

Documented in: OracleManager.getSettlementPrice NatSpec + the boundary-pin test OracleManager.invariant.t.sol::test_I8_revertsPastStaleness_boundary.

Possible remediations (for spec review, not Phase 1):

• Bypass the staleness check when the backstop fires (one-line change, spec change required)
• Widen MAX_STALENESS to give the backstop more breathing room
• Accept the 1h window as the protocol guarantee and update spec wording

Spec §4.4 defines marketId = keccak(token0, token1, fee, durationSeconds) but doesn't specify how the contract resolves those four values from a marketId. We added an owner-managed MarketConfig registry; governance pre-registers each market with (token0, token1, fee, durationSeconds, oracleToken). createSwap cross-checks the position's actual (token0, token1, fee) against the registered tuple.

Documented in: InflexionCore NatSpec. Worth promoting into spec as a first-class concept.

Spec table:

±5%  range → MaxIL ≈ 0.3% of V0
±10% range → MaxIL ≈ 1.2% of V0
±20% range → MaxIL ≈ 4.8% of V0
±50% range → MaxIL ≈ 25%  of V0

Empirically measured (quant/notebooks/03_path_to_il.ipynb):

±5%  range → MaxIL ≈ 1.2% of V0
±10% range → MaxIL ≈ 2.4% of V0
±20% range → MaxIL ≈ 4.7% of V0
±50% range → MaxIL ≈ 13.8% of V0

Spec placeholders should be updated. Tracked in docs/MATH.md §3.

A review found that createSwap and settle accepted a caller-supplied sqrt price. settle computed the payout from the caller's sqrtP_T (the validated Chainlink price was only emitted), so any permissionless settler could set the payout anywhere in [0, MaxIL]; createSwap took the entry sqrtP0 bounded only to [Pa, Pb], letting an LP pick the entry that sets MaxIL / premium / V0. Both prices are now derived on-chain from Chainlink via _oracleSqrtPriceX96 (decimal- and orientation-aware; MarketConfig decimals are read on-chain at registerMarket, never trusted from calldata; the oracle orientation is immutable across re-registration). This restores invariants I2 / I4 and the Fork-1 oracle pinning, and aligns the code to spec §5.2/§5.4 (which already specified P0 = oracle.getPrice). Accepted residuals, by design:

• In-range is now defined at the ORACLE price, not the pool's slot0. The Pa ≤ P0 ≤ Pb gate compares the Chainlink-derived P0. When oracle and pool spot diverge (normal basis, thin pool, transient dislocation), a position that is in-range by pool-truth but out-of-range by the oracle is rejected (and vice versa). Intentional and consistent with settlement (also oracle-pinned); not a fund-loss vector.
• Bounded entry-timing freedom. P0 is the latest Chainlink round at the LP's chosen block, clamped to within priceBandBps of the MM-signed quotePrice over a 5–15 s validity window, so an LP can prefer a marginally favourable round — bounded by the MM's chosen band, blunted by premium scaling with MaxIL. This is the intended firm-quote + oracle-band design (I9), not a drain.
• Phase-boundary liveness. getSettlementPrice reads neighbour rounds tolerantly (_tryRound): across a Chainlink phaseId boundary (where roundId ± 1 is not the real neighbour) a missing next round degrades to the liveness backstop (accept the pinned round past LIVENESS_WINDOW) rather than a permanent fund-lock (invariant I8). It never lets a settler choose the price — the round-at-T is uniquely bracketed below by updatedAt ≤ expiry.

Roadmap hardening (not blocking): decimals are validated on-chain today; for any future non-USD-quoted pair the USD-stable = $1 numéraire assumption (spec §19) must be revisited before listing.

fairRate = E_Q[min(IL, MaxIL)] / MaxIL is priced under risk-neutral GBM with the forward pinned at F = P0 (martingale, r = 0, q = 0). A nonzero financing rate r or ETH staking yield q tilts the true risk-neutral forward to F = P0·exp((r − q)·T), and the v3 IL payoff is asymmetric about P0, so the tilt is not strictly price-neutral. Sized and found economically negligible at launch scope (re-pricing il.py under a forward-tilted terminal across widths ±5–50% and 7/30/90-day durations, σ = 0.6):

• Worst absolute move: +0.32 pts of MaxIL (±20%, 90d, aggressive θ = r − q = −0.08); worst relative move: +0.7%.
• Worked $50k / ±10% / 30d position (MaxIL $1,280): premium moves ≤ $1.30 even at θ = −0.08; ≤ $2.50 at 90d — at/below the $1 dust-floor resolution for typical carry (|θ| ≤ 0.04) and well inside the load.

Conclusion: r = 0 is acceptable for the buildathon; revisit only for long-dated (≥ 90d) or high-carry pairs. (Original red-team sizing; the scratch script that produced these figures has been removed — this paragraph is the retained record.)

Multi-LLM external audit (Claude Opus 4.7, GPT, Gemini) of the protocol design. Result: 12 fixes applied → spec v3.3 + 2 architectural forks resolved:

• Fork 1 (Option B) — oracle settlement deadlock: round-at-T pinning
  • lone-spike sanity + liveness backstop. Implemented in OracleManager (Phase 3).
• Fork 2 (Option B) — firm-quote pickoff: oracle-anchored price band. Implemented as the absBps(P_live, quotePrice) ≤ priceBandBps check in InflexionCore.createSwap (Phase 5). Invariant I9.

Audit details live in project memory (inflexion-audit-findings); the original audit files were cleared after integration into spec v3.3 per project policy.

Independent adversarial audit of the Monte Carlo solvency model (GPT-5 + Code Interpreter, Gemini 2.5 Pro). 6 HIGH-severity findings; 9 fixed in-band, 6 deferred as mainnet-TODOs with named owners.

Key fixes (per PR #5):

• n_runs 1,000 → 50,000 (1k was statistically meaningless for a 0.1%-tail estimate)
• VaR → CVaR for fund_target (coherent, tail-aware)
• Mean-pnl criterion for fee curve (not median)
• Fixed-point bisection for c_min ↔ fund_target (replaces hand-picked bootstrap)
• Severe stress params re-anchored to historical episodes (Terra, FTX, March 2020, May 2021)
• parameter_provenance per field (calibrated / heuristic / deferred)
• Annualised ruin budget surfaced (0.1%/30d ≈ 1.21%/year)
• 8 hand-calculated il.py fixtures from Uniswap §6.30 (audit C1)

Deferred to mainnet (documented in quant/params.json.notes):

• Portfolio-level multi-market calibration
• Empirical position mix from Uniswap subgraph
• Joint c_min × fee_curve optimisation
• Multi-period fund evolution
• MM / LP behavioural models
• Multi-σ floor curve
• Depeg / oracle-failure / liquidation cascade mechanisms

Ran Slither 0.11.5 against packages/contracts, filtered to src/ (test/, script/, lib/ excluded). Total: 27 findings → 1 fixed, 26 accepted false-positives. Reproduce:

slither packages/contracts --filter-paths "test|script|lib"

1 medium fixed — reentrancy-no-eth in InflexionCore.settle:

Before the fix, s.status = SETTLED was written after oracle.getSettlementPrice and ilMath.computeIL. A malicious oracle or IL-math implementation could re-enter settle on the same swapId while it was still ACTIVE. Both are owner-deployed trusted contracts in practice, but the hardening is essentially free.

Fix: hoisted s.status = Status.SETTLED to immediately after the validity checks, before any external call. Strict CEI. Re-entry now hits the Status.ACTIVE precondition and reverts. PR/commit: 5.13.

Accepted findings (26) — disposition:

Manual review pass: verified all I1–I9 invariants are enforced by the code paths the tests cover (see §1). No additional findings beyond the documented Fork-1 design observation (§3.1).

Re-ran Slither 0.11.5 on the cvAMM additions (ConvexityVault, FairValueOracle, VolOracle) + the modified InflexionCore (createSwap / createSwapPathA / createSwapRouted + the settle dispatch). 74 results → 0 high, 0 confirmed vulnerabilities; 1 cleanup applied (the stray foundry-template Counter.sol / Counter.t.sol / Counter.s.sol deleted — they were the only ^0.8.13 usage). Reproduce: slither packages/contracts --filter-paths "test|script|lib".

Manual review. ConvexityVault: the junior-first-loss waterfall (releaseAndDistribute caps payout at juniorAssets), the withdrawal cooldown + locked/free accounting (the pool cannot be run), and lockCollateral's lockedAfter ≤ juniorAssets check (the u ≤ 1−sf senior-protection condition); share math handles zero supply/assets. FairValueOracle / VolOracle: pure/view math

• a single permissionless poke; no fund custody, no reentrant surface. The FULL no-bad-debt guarantee (I1) is structural and independent of these oracles — settle caps payout at MaxIL == collateral. No findings beyond the documented design observations (§3.1). The Stylus FairValueOracle is upstream of settle and is a pure pricer; its accuracy/gas record is in docs/STYLUS_FAIRVALUE_BENCHMARK.md.

Settlement is non-custodial and on-chain. The off-chain matching engine's power is strictly bounded:

Mitigations against the powers it has (F-#13, spec §4.5):

1. Direct-to-contract fallback. Any LP holding a valid signed quote can call createSwap directly, bypassing the engine. The SDK exposes this path — a censoring operator simply loses the user.
2. Append-only quote log. Engine publishes its full quote stream and match decisions to a rotating log (Phase 6.7).
3. Deterministic price-time / FIFO matching rules.

The decentralisation roadmap is an Arbitrum Orbit chain hosting the quote book fully on-chain (Hyperliquid pattern) — out of hackathon scope but the clean answer to "isn't the matcher centralised?".

• PARTIAL mode + Insurance Fund security — Phase 15 (stretch). Quant track has produced params.json v2.0.0 with the parameters Phase 15 will deploy with, but the on-chain InsuranceVault contracts don't exist yet.
• Smart-contract upgradability — there is none. All deployed contracts are immutable; the setCore + freezeCore pattern lets us one-shot wire vaults to InflexionCore and then permanently lock the wiring.
• Front-end / engine security — out of scope of this doc; covered in docs/SECURITY.md of apps/web and packages/engine (Phase 10 / Phase 6).