Invariants

These are the properties the code must satisfy for every sequence of calls, from any address, in any market state. They are implemented as Foundry invariant_* tests with bounded handlers, run at a minimum of 1 000 runs by 100 000 calls in a nightly job, and they are handed to auditors alongside the specification and the fuzz reports (Rule R-16.3).

Where a tolerance of n wei appears, n is the number of accruals that occurred in the sequence: interest is minted at accrual and rounding accumulates by at most one wei per accrual.

Supply and accounting

1. Global supply identity. Every fyUSD in existence is backed by a recorded debt, a recorded bad debt, or a PSM mint. There is no other source of supply.

fyUSD.totalSupply() == Σ_branches getEntireDebt() + Σ_branches badDebt + FYUSD.minted[PSM]   (± n wei)

2. Collateral accounting. Per-position collateral sums to the branch total, and the branch never owes more tokens than it holds.

Σ_u coll[u] == totalColl
totalColl + Σ_u collSurplus[u] <= token.balanceOf(branch)

3. Minimum debt. A position is either closed, at or above the minimum, or explicitly marked as reduced by a redemption.

debt(u) == 0  ∨  debt(u) >= minDebt  ∨  reduced[u]

14. Per-minter accounting. Each minter's recorded issuance matches what it owes, and the PSM's reserve matches its issuance exactly.

FYUSD.minted[branch] == branch.getEntireDebt() + branch.badDebt
PSM.reserve()        == FYUSD.minted[PSM]                            (± rounding)

Position safety

4. No self-inflicted undercollateralisation. No voluntary operation by a position's owner can leave it below the minting ratio of the state it executed in.

after any owner-initiated op:  ICR(u) >= CR_mint / (1 − haircut(confidence))

5. Solvency under a moving price. As long as the price does not fall by more than the margin the liquidation threshold provides between two accepted oracle readings, collateral covers debt net of bad debt. Tested with a slow-moving oracle mock, then with gaps.

Σ coll × price >= Σ debt − badDebt
  while Δprice between two accepted readings <= 1 − (1 + bonus + slippage)/MCR

8. Liquidation and redemption improve the position. A partial liquidation never leaves a position in worse shape than it found it, and the same holds for a partial redemption.

after partial liquidation:  ICR_post >= ICR_pre  ∧  debt_post >= minDebt
after partial redemption:   ICR_post >= ICR_pre

9. Collateral cannot leave without a valid cause. Traced with ghost variables across the whole sequence.

coll[u] decreases  ⇒  cause ∈ { withdraw by u, close by u, liquidation, redemption, post-shutdown settlement }

Interest

10. Interest is monotone and bounded, and the clock respects its stops.

interest index monotone non-decreasing
debt(u) <= recordedDebt[u] × (1 + rateMax × dt)
interestClock <= now − DEPLOY_TS
interestClock does not advance while (degradedSince != 0 ∧ now − degradedSince > 24 h)
interestClock does not advance after shutdownAt

Stability Pool and wrapper

6. The pool is solvent in both assets.

SP.totalDeposits <= fyUSD.balanceOf(SP)
Σ unclaimed collateral gains <= token.balanceOf(SP)

23. The wrapper never overstates its assets. The valuation of inventory being sold uses the lower of the two prices, so it can only understate. An in-kind redemption is exact.

sfyUSD.totalAssets() <= SP.getDeposit(wrapper) + pendingYield
                        + inventory × min(pRef, pLiq)
redeemInKind(shares) delivers exactly shares / totalSupply of each asset

Ordering and routing

7. The sorted list is sorted.

SortedTroves is ordered by ascending annualRate
length(SortedTroves) == count of positions where !reduced

Liquidation discipline

13. Nothing is liquidated when liquidation is forbidden.

no liquidation while regime == FROZEN
no liquidate during a quiet edge, a Closer liquidation freeze,
   or the first 24 hours of a token upgrade freeze
no liquidation at a pLiq above the one the same caller could observe 30 min earlier
no liquidate within SESSION_EDGE_S of a composite following a long silence,
   nor of any exit from FROZEN

30. A DEGRADED liquidation runs only under its own full set of conditions.

regime == DEGRADED
∧ flaggedAt ∈ [now − 6 h, now − CONFIRM_DRIFT]
∧ ICR(pLiq) < MCR   ∧   ICR(pLiq) >= 1 + B_MIN
∧ (dropConfirmed ∨ pLiq == pComposite)
∧ bucket not empty

34. A liquidation never creates bad debt and never worsens a position. The check is on the whole position, before execution, whatever maxDebtToRepay the caller passes.

∀ executed liquidations:
  coll × pLiq >= debt × (1 + B_MIN)   before execution
  ICR_post >= ICR_pre

15. Throughput buckets are respected. Every liquidation bucket is counted in debt burned, the same unit as invariant 31, so the two can never disagree about how much has been taken.

Σ debt burned over any 60-minute window <= bucket capacity (per branch, and globally)
Σ CollateralSale.buy over any 60-minute window <= its own bucket capacity

31 (I-8). The per-episode ceiling holds, in debt.

Σ debt burned in DEGRADED over one degraded episode
  <= min(1.0 × d2_eff, 15% × branch debt at the start of the episode)
each such liquidation burns <= 0.10 × d2_eff

Oracle

26 (I-2). The three prices keep their order, and the band is never written.

pComposite × (1 − BAND_BASE) <= pRef <= pComposite <= pRedeem
                                            <= pComposite × (1 + BAND_BASE)
pLiq ∈ { pRef, pComposite }   ∧   pLiq == pRef  ⇔  dropConfirmed
bandBps == BAND_BASE

The earlier form asserted pLiq <= pRef, and it failed the first time a fall was visible on-chain without being confirmed: valuation recognises such a fall and liquidation does not.

27 (I-4). LIVE24 means one price, with no exception.

regime == LIVE24  ⇒  pLiq == pRef == pRedeem == pComposite    (quiet edge included)
regime == LIVE24  ⇒  conf == 1 ∧ CR_mint_eff == CR_mint

37 (I-15). With no uptime feed there is no sequencer cause, ever.

sequencerFeed == 0  ⇒  cause != SEQ_DOWN
  ∀ sequences, including 72 hours with no ETH/USD round

40 (I-18). The basket moves confidence and nothing else.

changing pDex on any basket branch leaves pRef, pLiq, pRedeem
  and dropConfirmed unchanged; it moves only dispBps, and only downward
  in confidence

12. The price is independent of caller state. After any sequence of deposits, borrows, liquidations, token donations, swaps and pokes, the adapter returns the same price it would have returned without them.

invariant_priceIndependentOfCallerState:
  quote().price is a function only of (source data, adapter snapshots)

Liveness

11. Risk reduction always works. Every one of these succeeds in any oracle state and under any Closer freeze.

repay, addCollateral, close, claimSurplus,
SP.withdraw, SP.claimCollateral,
PSM.swapOut, sfyUSD.redeem, Router.withdrawToUSDG
  all succeed  ∀ oracleState  ∀ closerFreeze

Immutability

17. No constant ever changes. The hash of the full set of immutables and tier tables read at the start of a fuzz run equals the hash read at the end, for every call sequence — including sequences executed from the Closer's own address.

keccak(all immutables ‖ all tier tables)_before == keccak(...)_after   ∀ sequences

18. No residual role. For every contract, a write function called from a random address either succeeds or reverts with one of exactly six whitelisted authorisation errors. No other authorisation error exists anywhere.

∀ contract, ∀ writeFn, ∀ randomCaller:
  success  ∨  revert ∈ { NotBranch, NotLiquidationEngine, NotInterestRouter,
                         NotWrapper, NotCloser, NotSafe }

39 (I-17). The haircut never enters a branch-level condition.

TCR(pRef) >= CCR  ∧  badDebt == 0  ∧  now >= upgradeFreezeUntil
  ⇒  !mintFreeze,  whatever the haircut h

19. The Closer stops existing. After warping past the expiry, every Closer function reverts and no onlyCloser function anywhere in the system is reachable.

warp(EXPIRES_AT):
  ∀ fn ∈ Closer: revert CloserExpired
  ∀ fn marked onlyCloser in any module: unreachable

16. Every freeze expires on its own.

any Closer freeze lapses within 72 h with no action    (liquidation freeze: 24 h)
freezeCumul[branch] <= 30 days
liqFreezeCount[branch] <= 3

38 (I-16). A liquidation freeze is spaced, and it never traps anyone in.

two successful freezeLiquidation on one branch are >= 7 days apart
during a liquidation freeze:  SP.provide reverts, sfyUSD.deposit reverts,
                              SP.withdraw succeeds

Caps

20. The depth ratchet only ever tightens quickly.

d2_eff may fall immediately and by any amount
d2_eff may rise by at most 20% per 24-hour period,
  and never within 24 hours of the first observed rise in P25

21. Bad debt locks capacity permanently. For every subsequent sequence — full repayment, backstop coverage, redistribution — the branch never reaches a higher tier than the one in force when the first entry was recorded.

badDebtCumul > 0  ⇒  cAbs() <= cAbs_at_first_badDebt_entry   ∀ later sequences

22. One-way state transitions.

activatedAt: 0 → t, never back
shutdownAt:  0 → t, never back
sunsetAt:    0 → t, never back
activatedAt == 0  ⇒  debtCeiling() == 0

Value routing

24. The split is always a complete split.

at every route():  sp + backstop + treasury + pil == 1e18
treasury <= 20%
backstop > 0  ⇔  Backstop.balance < 2% × D_total

Module-level invariants

Beyond the fuzzed set, each module carries properties asserted in its own unit tests:

• FYUSD. No transfer or burn without a standard allowance. The minter set equals exactly the deployed bytecode's set — twenty branches and the PSM (Rule R-2.1.3).
• OracleAdapter. The price ordering of invariant 26 in every regime; bandBps always equal to BAND_BASE; LIVE24 implies all three prices equal to the composite and confidence 1; confidence is monotone when a source disappears; degradedSince is non-zero exactly when the regime is FROZEN; no adapter function writes a constant (Rule R-3.2.11).
• Branch. cAbs() is non-decreasing while badDebtCumul is zero and frozen afterwards; badDebtCumul is monotone (Rule R-3.3.2).
• StabilityPool. An offset reduces branch debt and branch collateral by exactly the amounts burned and transferred (Rule R-9.2.6). provide reverts under a Closer liquidation freeze; withdraw reverts under nothing but a same-block offset.
• RedemptionRouter. For burned fyUSD burned, total debt falls by exactly burned; no position below the liquidation threshold is touched; unconsumed fyUSD is returned rather than burned (Rule R-7.7.1).
• BranchRegistry. No two branches share a token; a branch is never removed, because the function does not exist.
• PSM. reserve == minted[PSM] in every mode, including during Sunset.

Running them yourself

The invariant suite ships in the repository and can be run against a local deployment or a fork. Auditors receive it together with the frozen specification, the fuzz reports and the zero-setter deployment report (Rule R-16.6).

If you find a sequence that breaks one of these, that is a finding regardless of whether it produces a loss. An invariant that can be violated is either a bug or a specification error, and both matter equally in a system that cannot be patched.

Last reviewed: 2026-09-07 · Spec v0.4