| Id | Invariant |
|---|
| C1 | For every series: quoteEscrow == N_c + prefundRemaining + claimableQuote + refundableQuote + accruedFees |
| C2 | For every series: stockEscrow == stockMatched + refundableStock + claimableStock |
| C3 | USDG.balanceOf(NoteCore) ≥ Σ quoteEscrow and Stock.balanceOf(NoteCore) ≥ Σ stockEscrow per token |
| C4 | NoteLegs.totalSupply(couponId) ≤ matchedNotional and totalSupply(shieldId) ≤ matchedNotional, equality once every depositor has settled and before any redemption |
| C5 | couponIndex is non-decreasing; Σ accrued(holder) ≤ couponPool |
| C6 | nextObs is non-decreasing and ≤ observations.length |
| C7 | Status transitions follow the state machine; terminal statuses never change |
| C8 | Total USDG ever paid out of a series ≤ total USDG ever deposited into it |
| C9 | Total stock ever paid out of a series ≤ total stock ever deposited into it |
| C10 | prefundRemaining ≥ (remaining coupon observations) × N × couponBps / 1e4 while Live |
C1 and C2 are the escrow invariant. C8 and C9 follow from C1 to C3 but are asserted independently as ghost-variable checks.
| Id | Invariant |
|---|
| O1 | An observed price always comes from the last round with updatedAt ≤ closeTs + closeGrace, which satisfies updatedAt ≥ closeTs − maxPreCloseLag; the selected round is independent of the call time |
| O2 | If two feeds are configured and both pass, they differ by ≤ maxDeviationBps |
| O3 | forceObserve can only execute ≥ forceDelay after its proposal and ≥ deferralWindow after closeTs |
| O4 | isOfficialClose(t) implies t is a weekday, not a holiday, and equals the regular or registered early close for its day |
| Id | Invariant |
|---|
| T1 | NOTE.totalSupply ≤ CAP and mintedInEpoch[e] ≤ mintCapPerEpoch for every epoch |
| T2 | Only whitelisted minters ever increase totalSupply |
| T3 | sNOTE share price (totalAssets+1)/(totalSupply+1e6) is non-decreasing |
| T4 | NOTE.balanceOf(sNOTE) ≥ totalAssets + unvestedRewards() |
| T5 | Treasury: redeemedInWindow ≤ reserveValueQuote × dailyRedemptionCapBps / 1e4 within any window |
| T6 | Treasury floor reserveValueQuote / circulatingSupply is non-decreasing across redemptions |
| T7 | RevenueRouter: every fill price ≥ floorPriceWad; every fill ≤ maxFillBps of the buyback reserve |
| T8 | RevenueRouter: USDG.balanceOf(router) ≥ buybackReserve |
| T9 | BondDepository: Σ payouts(market) ≤ capacity(initial); currentDebt ≤ maxDebt |
| T10 | Desk: deployedPerSeries ≤ perSeriesCap × totalAssets, likewise per underlying and total, at the time of each fill |
- One handler contract per module exposing every external mutating function with bounded random inputs and a rotating set of actors.
- A
TimeHandler that warps to the next official close and drives the oracle mocks with fuzzed prices, occasionally stale or negative answers, and occasional backup-feed disagreement.
- Ghost variables track cumulative deposits and withdrawals per series and per token.
fail_on_revert = false so that expected reverts (too early, caps) do not abort a run; unexpected reverts are asserted separately in unit tests.- Default 512 runs × 64 depth locally; 5,000 × 64 in CI.
status The handler suites are committed: test/invariant/core (CoreInvariantHandler, NoteCore.invariant.t.sol, reachability test), test/invariant/token (Desk, NOTE, RevenueRouter, Treasury, sNOTE) and test/invariant/governance (veNOTE, GaugeController, Gauge, Minter). The core handler includes a lazyCrank action so that the crank-in-exit path is exercised under the escrow invariant. Heavy runs (5,000 × 64) and their logs are recorded in the internal security review under audit/.