Skip to main content
[ DOCS · INVARIANTS ]

Invariants

Invariants are properties Riptide evaluates every tick. The init stub doesn't write any — pick the entries below for your protocol class, paste them into your adapter, and tune the bounds. The authoring guide at the end covers the patterns when none of the catalog entries fit.

Overview

An invariant is a machine-checkable property that should hold every tick of every run. When one fires, the engine records the firing tick, the run is marked failed, and the engine exits non-zero so CI can gate on it. Invariants live in the adapter — committed alongside the program, not reinvented per scenario.

For the schema (raw [[invariants]] vs semantic [[semantics.invariants]], supported ops, the severity field) see Invariants in the adapter spec. This page is the catalog (what the shipped fixture adapters declare per protocol class) and the authoring guide for writing your own.

Lending

The shipped lending adapter uses lending.v1 semantics. All three invariants are expression-based and reference derived values (debt_value, collateral_value, max_borrow_value) declared in [semantics.derived].

[[semantics.invariants]]
name = "bad_debt_bound"
expr = "debt_value <= collateral_value"
severity = "warn"
description = "Position debt must not exceed collateral value"

[[semantics.invariants]]
name = "ltv_below_max"
expr = "debt_value <= max_borrow_value"
severity = "warn"
description = "Position debt must not exceed max-borrow value"

[[semantics.invariants]]
name = "collection_worst_health_factor"
expr = "collection.worst_health_factor > 1.0"
severity = "warn"
description = "Worst observed reserve health factor should remain above 1.0"
  • bad_debt_bound — fires when any position's debt exceeds its collateral. The canonical "the protocol is now under-collateralized" signal; the lending case study is built on the first-firing tick of this invariant.
  • ltv_below_max — fires when a position's debt exceeds its max_borrow_value. Catches LTV-cap escapes before they cascade into bad debt.
  • collection_worst_health_factor — fires when the worst health factor across the entire population drops to or below 1.0. Collection-level invariants summarize across all agents — useful for population-pressure scenarios.

AMM / DEX

The shipped AMM adapter declares both amm.v1 semantic invariants and raw [[invariants]] blocks. The catalog below lists the raw CI-gate invariants: absolute integer caps that should never be crossed under any sane swap or liquidity event.

[[invariants]]
name = "fee_bps_bounded"
field = "pool.fee_bps"
op = "<="
value = 10000

[[invariants]]
name = "lp_shares_bounded"
field = "lp_position.lp_shares"
op = "<="
value = 100000000000000

[[invariants]]
name = "total_lp_supply_bounded"
field = "pool.total_lp_supply"
op = "<="
value = 100000000000000
  • fee_bps_bounded — fee bps must stay within 0-10000 (0-100%). Catches accidental fee writes that escape the basis-point range.
  • lp_shares_bounded — per-position LP share count must stay below 1e14. A sanity ceiling that catches integer-overflow-adjacent share-mint bugs.
  • total_lp_supply_bounded — pool-level total must stay below 1e14. The aggregate counterpart to lp_shares_bounded; catches cumulative drift even when individual positions stay in range.

Perpetuals

The shipped perpetuals adapter declares both perps-margin.v1 semantic invariants and raw [[invariants]] blocks scoped to the executable perps-lite surface.

[[invariants]]
name = "no_socialized_loss"
field = "market.cumulative_socialized_loss"
op = "=="
value = 0

[[invariants]]
name = "max_leverage_respected"
field = "position.leverage_bps"
op = "<="
value = 100000
  • no_socialized_loss — cumulative socialized loss must remain zero through the run. Fires the first tick the protocol distributes losses across surviving positions. Canonical insurance-fund-depleted signal.
  • max_leverage_respected — per-position leverage stays at or below 10x (100_000 bps). Catches leverage-cap escapes the program's pre-trade check should have rejected.

Liquid Staking

The shipped liquid-staking adapter declares both lst.v1 semantic invariants and raw [[invariants]] blocks tied to slash and exchange-rate observations.

[[invariants]]
name = "no_slash_during_healthy_run"
field = "pool.cumulative_slashed"
op = "=="
value = 0

[[invariants]]
name = "exchange_rate_bounded"
field = "pool.exchange_rate_bps"
op = "<="
value = 100000
  • no_slash_during_healthy_run — fires the first tick a slash event mutates the pool's cumulative slashed counter. Pair with the panic-exiter persona to observe queue pressure post-slash.
  • exchange_rate_bounded — exchange rate must stay at or below 10x par (100_000 bps). Catches runaway-mint or rebase-overflow paths that would inflate the LST share-to-stake ratio.

Stablecoin

The shipped stablecoin adapter declares both stablecoin.v1 semantic invariants and raw [[invariants]] blocks tied to backing health.

[[invariants]]
name = "no_hedge_loss_during_healthy_run"
field = "pool.cumulative_hedge_loss_bps"
op = "=="
value = 0

[[invariants]]
name = "collateral_ratio_bounded"
field = "pool.effective_collateral_ratio_bps"
op = "<="
value = 100000
  • no_hedge_loss_during_healthy_run — fires the first tick apply_hedge_loss shrinks delegated collateral. Triggers the panic-redeemer cohort on effective_collateral_ratio_bps < 10000 — the UXD-style cascade.
  • collateral_ratio_bounded — effective collateral ratio stays at or below 10x par. Catches mint-without-deposit paths that would inflate the ratio outside any sane range.

Writing Your Own Invariant

The shipped invariants are starting points. As you formalize what "broken" means for your protocol, add invariants that name those properties. Three patterns cover most of what's worth checking:

1. Cumulative-counter invariants

Pattern: op = "==", value = 0 against a counter that should never increment in a healthy run. Cheap, blunt, and effective. Whenever your program has a "this counter only moves when something bad happens" field — bad debt, slashed amount, socialized loss, hedge loss, liquidation count — add one.

[[invariants]]
name = "no_bad_debt"
field = "pool.bad_debt"
op = "=="
value = 0

Scenarios then declare a shock that should increment it. Passing means the shock didn't fire it; failing names the tick. The lending whale-shock case study is exactly this pattern.

2. Bound invariants

Pattern: op = "<=" or ">=" against a hard cap your program enforces in pre-trade checks. Catches monotonicity escapes — places where the cap was logically supposed to hold but didn't under stress.

[[invariants]]
name = "max_leverage_respected"
field = "position.leverage_bps"
op = "<="
value = 100000

Useful targets: fee bps, leverage caps, exchange-rate ceilings, share-supply caps, max position size, max LTV.

3. Semantic relational invariants

For adapters with a versioned [semantics] block, prefer [[semantics.invariants]] with expr when the property is economic rather than a raw counter or bound. The typed surface lets one invariant express a relation that would need three or four raw field comparisons. Shipped fixtures cover lending.v1, perps-margin.v1, amm.v1, lst.v1, and stablecoin.v1.

[[semantics.invariants]]
name = "bad_debt_bound"
expr = "debt_value <= collateral_value"
severity = "warn"
description = "Position debt must not exceed collateral value"

The expression is evaluated against the per-position derived values declared in [semantics.derived]. Use collection.<name> to summarize across the whole population (the engine ships collection.worst_health_factor, etc.).

Picking values that don't trigger spuriously

Two common mistakes when authoring bounds:

  • Floor too tight. If a healthy program briefly touches the bound under normal load (e.g. health factor at exactly 1.0 right after a price update), the invariant will fire on a clean run. Sweep the boundary first; pick a value below the lowest healthy observation.
  • Wrong scope. A position-level field (position.debt) and a pool-level field (pool.bad_debt) read different things. Cumulative-counter invariants almost always want pool-level; relational invariants almost always want position-level (or collection-level). Check what your [state_mapping] actually exposes.

Validate before running

riptide lint <program> flags invariant fields that don't exist as observations. For adapter-only programs, riptide adapt --adapter .riptide/adapters/<program>.toml smoke-tests the adapter end-to-end. For harnessed programs, use a one-seed riptide run --harness .riptide/harness smoke so the invariant is checked against real setup state before activating it in CI.

Invariants in the adapter spec Observations Architecture: invariant evaluation