Protocol Invariants#

Formal invariants that must hold at all times in the Seesaw protocol.

Overview#

Invariants are properties that must remain true across all state transitions. Violating any invariant indicates a bug or attack. The catalog below is the authoritative list of guarantees the protocol upholds; integrators can rely on each one holding for any market they interact with.

Execution-Path Integrity#

These invariants govern how the order-placement, matching, and settlement paths behave under all inputs. They are the highest-risk guarantees for trading correctness and are described first because integrators depend on them holding for every fill.

INV-X1: Bounded Order-Placement Account Surface#

Placing an order never requires the accounts of arbitrary counterparties. Any value owed to a maker whose resting order is filled is deferred into market-owned claim state, which the maker (or anyone settling at market end) collects later. This keeps PlaceOrder against a fixed, bounded account surface and means a taker can always match against resting liquidity regardless of which makers placed it.

INV-X2: No Crossed or Unsorted Book on Commit#

Before any order is allowed to rest, the matching path performs a runtime no-cross and sortedness recheck against the committed orderbook state. An order that would cross the book or violate price ordering cannot be written. This is a stronger guarantee than INV-O1/INV-O5 alone: it holds on the production mutation path, not only in analysis helpers.

INV-X3: Single Canonical Fill-Accounting Transition#

Redeem, force-close, and deferred maker settlement all delegate to one shared fill-accounting transition. Because there is exactly one code path that credits fills and unlocks collateral, no settlement route can double-credit, miss an unlock, or drift from another route.

INV-X4: Emergency Status Fails Closed#

A market's emergency_status byte that is not a recognized value is rejected rather than silently treated as "no emergency". Corrupted or forward-incompatible state can never disable the protocol's emergency posture (pause / post-only); when in doubt the safer, more restrictive interpretation applies.

Note on retired limits. Earlier protocol versions exposed max_orders_per_user and max_position_size config fields. Neither was ever enforced on-chain, so both were retired to reserved layout slots; the account byte layout is unchanged. The protocol does not impose a per-user open-order or position-size cap (see Known Limitations in the threat model). Do not rely on either limit existing.

Global Invariants#

INV-G1: Account Ownership#

All protocol accounts must be owned by the program.

forall account A managed by protocol:

A.owner == PROGRAM_ID

INV-G2: PDA Authenticity#

All PDAs must derive correctly from their seeds.

forall PDA P with seeds S and bump B:

P == create_program_address(S ++ [B], PROGRAM_ID)

INV-G3: Discriminator Integrity#

All accounts must have correct discriminators.

forall account A of type T:

A.data[0..8] == T::DISCRIMINATOR

Market Invariants#

INV-M1: Epoch Alignment#

Market timing must align to the configured duration epochs.

code

forall market M:
    M.t_start == M.market_id * M.duration_seconds
    M.t_end == M.t_start + M.duration_seconds
    M.t_start % M.duration_seconds == 0

INV-M2: Snapshot Immutability#

Once captured, snapshots never change.

code

forall market M:
    once(M.start_price != 0) -> always(M.start_price unchanged)
    once(M.end_price != 0) -> always(M.end_price unchanged)

INV-M3: Resolution Determinism#

Same snapshots produce same outcome.

code

forall markets M1, M2:
    (M1.start_price == M2.start_price AND M1.end_price == M2.end_price)
    -> M1.outcome == M2.outcome

INV-M4: State Monotonicity#

States only transition forward.

forall market M:

state(M) transitions only:

PENDING -> CREATED -> TRADING -> SETTLING -> RESOLVED -> CLOSED

INV-M5: Resolution Rule#

Outcome determined by price comparison.

forall resolved market M:

M.outcome == (M.end_price >= M.start_price ? UP : DOWN)

INV-M6: Oracle Feed-Identity Pinning#

All three oracle entry points (start snapshot, end snapshot, expiry late capture) validate the supplied Pyth price account against the market's creation-bound feed address AND feed_id before reading any price. A substitute account — even one carrying the same feed_id — is rejected. The start path is the binding event: it reads the feed_id from the validated Pyth account and pins it into the market PDA seed (["seesaw","market", pyth_feed_id, ...]) and the stored market.pyth_feed address; the end and expiry paths then re-pin both the account address and the feed_id against that bound value.

code

forall market M, oracle entry point E in {start, end, expiry_late_capture}:
    let (addr_E, id_E) = the Pyth account address + feed_id supplied to E
    E proceeds to read a price
        -> addr_E == M.pyth_feed (creation-bound account address)
       AND id_E  == M.pyth_feed_id (creation-bound feed identifier)
    addr_E != M.pyth_feed     -> Err(OracleMismatch)   // substitute account rejected
    id_E   != M.pyth_feed_id  -> Err(FeedIdMismatch)    // wrong feed rejected

Production sites:

Start (binding event): src/processor/create_market.rs — validate_pyth_feed (L603), read_pyth_feed_id (L606), feed_id bound into the market PDA seed and stored via validate_create_market_pdas (L626-L641).
End snapshot: src/processor/snapshot.rs:218 validate_pyth_feed_address(accts.pyth_feed, &market_pyth_feed_addr) and src/processor/snapshot.rs:220 validate_pyth_feed_id(accts.pyth_feed, &ctx.pyth_feed_id).
Expiry late capture: src/processor/expire_market.rs:556 validate_pyth_feed_address(...); src/processor/expire_market.rs:716 validate_pyth_feed_address(...) and src/processor/expire_market.rs:722 validate_pyth_feed_id(...) inside try_late_price_capture.

Helpers: src/oracle/pyth.rs::validate_pyth_feed_address (L521-L532) and src/oracle/pyth.rs::validate_pyth_feed_id (L487-L501).

Production-bound evidence (instruction-level, real accounts — not a re-implemented twin): validate_pyth_feed_address/validate_pyth_feed_id are trivial [u8;32] equality checks, so the security-relevant assurance is that every call site passes the creation-bound expected value. That is verified at each path against the real production functions:

END snapshot: tests/security_wrong_feed_id.rs::test_attack_snapshot_end_wrong_feed_address_same_feed_id_rejected_by_oracle_mismatch drives the real SnapshotEnd instruction with a substitute account carrying the SAME feed_id but a different address, and asserts rejection with OracleMismatch at validate_pyth_feed_address — before validate_pyth_feed_id even runs.
EXPIRE late capture: src/processor/expire_market.rs::tests::expire_late_capture_rejects_substitute_feed_address supplies a Pyth account whose address differs from the market's bound pyth_feed and asserts determine_expire_market_resolution rejects with OracleMismatch at validate_pyth_feed_address (expire_market.rs:556).
START binding: at create-market the feed_id is read from the validated Pyth account and bound into the market PDA seed + stored market.pyth_feed; thereafter the END/EXPIRE paths re-pin against that bound value.

(A Kani harness over these helpers would only re-prove a one-line byte comparison against a copy of itself — semantically vacuous w.r.t. production per the H-01 finding — so the property is intentionally backed by the instruction-level tests above rather than a unit proof.)

Order Book Invariants#

INV-O1: No Crossed Book#

Best bid must be less than best ask.

code

forall orderbook O with non-empty bids and asks:
    O.best_bid < O.best_ask

INV-O2: Price Bounds#

All prices within valid range.

forall order ord in orderbook:

0 < ord.price_bps < 10_000

INV-O3: Quantity Positive#

All orders have positive quantity.

forall order ord in orderbook:

ord.quantity > 0

INV-O4: Order Ownership#

All orders have valid owner positions.

forall order ord:

exists position P: P.owner == ord.owner

INV-O5: Sorted Orders#

Bids sorted descending, asks sorted ascending.

code

forall orderbook O:
    O.bids is sorted descending by price
    O.asks is sorted ascending by price

Position Invariants#

INV-P1: Non-Negative Shares#

No negative share balances.

code

forall position P:
    P.yes_shares >= 0
    P.no_shares >= 0

INV-P2: Locked Less Than Total#

Locked shares cannot exceed total.

code

forall position P:
    P.locked_yes_shares <= P.yes_shares
    P.locked_no_shares <= P.no_shares

INV-P3: Single Settlement#

Positions settle at most once.

code

forall position P:
    once(P.settled) -> always(P.settled)
    P.settled -> P.payout is final

INV-P4: Collateral Coverage#

Locked collateral covers buy orders.

forall position P:

P.collateral_locked == sum(buy_order.value for buy_order in P.orders)

Vault Invariants#

INV-V1: Solvency#

Vault covers worst-case payouts.

forall market M with vault V:

V.amount >= max(M.total_yes_shares, M.total_no_shares) + M.accumulated_creator_fees

INV-V2: Conservation#

Trading preserves total value.

forall trade T:

collateral_in == collateral_out + fees

INV-V3: Empty at Close#

Vault empty when market closes.

forall market M transitioning to CLOSED:

M.vault.amount == 0

Total shares match sum of positions.

code

forall market M:
    M.total_yes_shares == sum(P.yes_shares + P.locked_yes_shares for P in positions)
    M.total_no_shares == sum(P.no_shares + P.locked_no_shares for P in positions)

Timing Invariants#

INV-T1: Snapshot Timing#

Snapshots captured after boundaries.

code

forall market M:
    M.start_price_timestamp >= M.t_start
    M.end_price_timestamp >= M.t_end

INV-T2: Trading Window#

Trading only during trading period.

code

forall order placed at time t in market M:
    M.t_start <= t < M.t_end

INV-T3: Settlement After Resolution#

Settlement only after outcome determined.

forall settlement S in market M:

M.outcome != None

Fee Invariants#

INV-F1: Capped-Linear-Decay Curve#

Taker fees follow the capped-linear-decay curve, with the cap enforced at the curve ceiling.

code

forall trade T at fill price p:
    raw_bps(p) = decay_rate_bps * (10_000 - p) / 10_000
    fee_bps(p) = min(fee_cap_bps, raw_bps(p))
    T.taker_fee == T.value * fee_bps(p) / 10_000 (ceiling)

INV-F2: Three-Way Fee Split#

Every taker fee splits cleanly among protocol, creator, and referral. The three shares are bps of the fee and MUST sum to exactly 10_000.

code

forall config:
    config.protocol_fee_bps
        + config.default_creator_fee_bps
        + config.referral_share_bps_of_fee
        == 10_000

INV-F3: Referral Attribution Lifetime#

Referral attribution is first-touch and immutable for the configured lifetime.

forall referral_account R:

R.referrer is unchanged for (R.attributed_at, R.attributed_at + 365*86_400]

INV-F4: Referrer Earnings Solvency#

The referrer treasury always holds at least the sum of all per-referrer accumulated earnings. Referrer earnings are sharded across 8 program-derived treasury accounts; this invariant is the system-wide form, restated per-shard as INV-REFERRAL-T2 and INV-REFERRAL-T3 below.

code

Σ_k referrer_treasury_k.balance >= Σ_referrer ReferrerEarningsAccount[r].accumulated   ; k ∈ [0, 8)

Multi-Fee-Recipients Invariants#

Protocol fees and referrer earnings are each distributed across 8 parallel destinations rather than a single account. Protocol fees route to one of 8 admin-configured SPL token accounts (config.treasury_recipients[8]), and referrer earnings route to one of 8 program-derived treasury shards. These invariants add no new on-chain runtime checks beyond the per-instruction validators listed below; the system-wide per-shard solvency totals (T3) are reconciled off-chain by the indexer.

INV-FEE-T1: Config holds exactly 8 treasury recipients#

code

config.treasury_recipients.len() == MAX_TREASURY_RECIPIENTS == 8

The treasury recipient list is a fixed-size array of 8, enforced at compile time by the type system. There are always exactly 8 protocol-fee destination slots.

INV-FEE-T2: Every fee-paying instruction binds the recipient to the configured set#

For every fee-paying instruction (PlaceOrder), the supplied treasury_token_account MUST equal config.treasury_recipients[protocol_treasury_index] for the protocol_treasury_index ∈ [0, 8) chosen in the instruction args, AND that token account MUST be a valid SPL Token v1 account whose mint equals the configured settlement mint.

code

∀ fee-paying ix:
  treasury_token_account.address() == config.treasury_recipients[protocol_treasury_index]
  AND treasury_token_account.mint == config.default_settlement_mint
  AND protocol_treasury_index < 8

An out-of-range index returns TreasuryIndexOutOfRange (0x8009); a mismatched address returns TreasuryRecipientMismatch (0x800A). Both are checked before any fee is moved.

INV-FEE-T3: System-wide solvency reconciliation across all shards#

code

Σ_{i=0..8} balance(config.treasury_recipients[i]) == Σ protocol_fees_collected (lifetime)

This is a cross-account total that cannot be checked inside a single instruction. It is a system-level invariant verified off-chain by the indexer's hourly treasury reconciliation job, which alerts on any drift.

INV-FEE-T4: `UpdateTreasuryRecipients` rejects zero pubkeys#

code

update_treasury_recipients(new_recipients):
  ∀ i ∈ [0, 8):
    new_recipients[i] != [0u8; 32]     →   else InvalidTreasuryRecipient (0x800B)

A treasury rotation cannot install a zero (all-zero) address in any slot. Each new recipient must also be owned by the SPL Token program.

INV-FEE-T5: `UpdateTreasuryRecipients` rejects pairwise duplicates#

code

update_treasury_recipients(new_recipients):
  ∀ i, j ∈ [0, 8), i < j:
    new_recipients[i] != new_recipients[j]    →   else DuplicateTreasuryRecipient (0x800C)

No two slots may hold the same address. The same distinctness check runs at config initialization.

INV-REFERRAL-T1: Every `ReferrerEarningsAccount` has a valid bound shard#

∀ ReferrerEarningsAccount r:

r.treasury_index < MAX_TREASURY_RECIPIENTS == 8

Each referrer-earnings account is permanently bound at creation to one of the 8 treasury shards. The shard index is bounds-checked at creation (returning TreasuryIndexOutOfRange for an out-of-range value), defensively re-checked on every accrual and claim, and immutable afterward.

INV-REFERRAL-T2: Per-shard credit/transfer pairing at PlaceOrder time#

Every credit to a referrer's accumulated earnings (with treasury_index = k) is paired with an equal-amount transfer into referrer treasury shard k. The supplied shard account must be the program-derived address for that index, validated before any state mutation.

code

∀ PlaceOrder credit Δ:
  ReferrerEarningsAccount[r].accumulated += Δ
  ⟺  TransferChecked(taker → referrer_treasury_<r.treasury_index>, Δ) succeeds
  AND referrer_treasury_<k> in the triple == derive_referrer_treasury_pda(k)

If the supplied treasury account is not the shard PDA derived from treasury_index, the instruction returns ReferrerTreasuryMismatch (0x8006) at both the PlaceOrder referral boundary and the ClaimReferrerEarnings boundary. The shard index is bounds-checked before any claim is paid.

INV-REFERRAL-T3: System-wide per-shard solvency reconciliation#

code

Σ_{k=0..8} balance(referrer_treasury_k) == Σ_referrer ReferrerEarningsAccount[r].accumulated

Implied by the per-credit pairing of INV-REFERRAL-T2 across all 8 shards. As with INV-FEE-T3, this cross-account total is verified off-chain by the indexer's hourly reconciliation job, which alerts on drift.

Verification#

Runtime Checks#

Each invariant has corresponding runtime assertions in the on-chain program. INV-V1 (solvency) and INV-O1 (no crossed book) are checked on every fill; INV-V2 (conservation) is checked on every trade. See src/logic/ for the assertion helpers.

Property Tests#

Invariants are verified under randomized inputs by the property test suite. See tests/property_tests.rs for the full set of property tests covering solvency, conservation, tick rounding, and deterministic resolution.

Formal Verification Targets#

Property	Method	Status
Solvency	K Framework	Target
Conservation	Certora	Target
No reentrancy	Static analysis	Done
Overflow safety	Clippy + MIRI	Done

Invariant Violations#

Detection#

Invariant violations manifest as:

Transaction failures with specific errors
Inconsistent state (detectable via indexer)
Unexpected account balances

Response#

The protocol's runtime invariant checks reject any transaction that would violate a core invariant — such transactions fail rather than committing inconsistent state. Where a protocol-wide issue is detected, the protocol can be paused (globally via Pause, or per market via SetMarketEmergencyStatus) to halt new trading while a fix is prepared.

Operational Notes#

A few behaviors are intentional and worth calling out for integrators so they are not mistaken for bugs:

Treasury recipients are admin-managed SPL token accounts, not PDAs. Protocol fees are sent to one of 8 configured SPL token accounts. Rebalancing funds between those 8 accounts is done by the admin off-chain; the protocol does not move balances between recipient slots automatically. The referrer treasury shards, by contrast, are program-derived and can only be debited by a referrer-signed ClaimReferrerEarnings.
A frozen treasury recipient degrades only its own shard. If a stablecoin issuer freezes one of the 8 protocol-fee token accounts, only orders that select that shard index fail; orders selecting any of the other 7 shards are unaffected. The admin can rotate the affected slot via UpdateTreasuryRecipients (subject to a one-hour rate limit).
Fee-config changes apply to live order flow, not retroactively to a resting order's terms. UpdateFeeConfig does not rewrite the fee owed on already-resting orders. Fees are always charged to the taker at the live curve at fill time, so a maker is never charged a fee for a change made after they posted. This matches the behavior of other on-chain order books and does not violate any invariant.

Price-Band Invariants#

These invariants are specific to the maker price-band gate (check_maker_band / compute_band in src/processor/place_order.rs). They govern the [lo, hi] window that Limit and PostOnly orders must fall within at placement time. Kani proofs live in src/verification/price_band.rs.

INV-BAND-1: No-panic on any `u16` input#

compute_band never panics for any combination of u16 inputs. All arithmetic is saturating; no branch can produce an unhandled overflow or array out-of-bounds.

forall bid, bid_count, ask, ask_count : u16:

compute_band(bid, bid_count, ask, ask_count) terminates without panic

Verified by Kani proof proof_compute_band_no_panic (src/verification/price_band.rs).

INV-BAND-2: `lo ≤ hi` always#

The returned band is never inverted.

code

forall bid, bid_count, ask, ask_count : u16:
    let (lo, hi) = compute_band(bid, bid_count, ask, ask_count)
    lo <= hi

Verified by Kani proof proof_compute_band_bounds_invariant (src/verification/price_band.rs).

INV-BAND-3: Band width bounded by `2 × MAKER_BAND_BPS` when dynamic#

When the book is two-sided and non-sentinel, the dynamic band is at most 2 × MAKER_BAND_BPS (currently 2 × 1000 = 2000 bps) wide.

code

when bid_count > 0 AND ask_count > 0 AND best_bid > 0 AND best_ask < P_MAX:
    let (lo, hi) = compute_band(best_bid, bid_count, best_ask, ask_count)
    hi - lo <= 2 * MAKER_BAND_BPS

Verified by Kani proof proof_band_width_bounded_by_2x_band_bps (src/verification/price_band.rs).

INV-BAND-4: Midpoint lies within `[lo, hi]` when band is dynamic and unclipped#

When the book is two-sided and the midpoint is far enough from both static clamps that neither endpoint is clipped, the midpoint is contained in the band.

code

when bid_count > 0 AND ask_count > 0 AND best_bid > 0 AND best_ask < P_MAX
    AND mid >= STATIC_MIN_BPS_FOR_BAND + MAKER_BAND_BPS
    AND mid + MAKER_BAND_BPS <= STATIC_MAX_BPS_FOR_BAND:
    let (lo, hi) = compute_band(best_bid, bid_count, best_ask, ask_count)
    lo <= mid <= hi

Verified by Kani proof proof_band_contains_mid_when_not_clamped (src/verification/price_band.rs).

INV-BAND-5: IOC orders bypass the gate unconditionally#

ImmediateOrCancel orders never rest on the book and are therefore exempt from the price-band gate. check_maker_band returns Ok(()) immediately for IOC order types without computing any band.

forall canonical_price_bps : u16, orderbook : OrderbookAccount:

check_maker_band(canonical_price_bps, ImmediateOrCancel, orderbook) == Ok(())

Source: src/processor/place_order.rs::check_maker_band — early return on OrderType::ImmediateOrCancel.

INV-BAND-6: Gate executes after canonical conversion + tick alignment, before matching#

The band gate fires at a fixed point in the place_order flow:

After convert_to_canonical (NO-side prices flipped to YES-book coordinates).
After tick alignment (price rounded to the configured tick size).
Before the match step (rejected orders never touch matching state).

Source: src/processor/place_order.rs — check_maker_band called at line ~1414, after canonical conversion and tick alignment but before route_to_slot / matching. Verified by step-ordering checks in tests/concurrency_price_band.rs and tests/determinism_price_band.rs.

Next Steps#

See Threat Model for attack analysis
Review Architecture Security for implementation

Protocol Invariants#

Formal invariants that must hold at all times in the Seesaw protocol.

Overview#

Execution-Path Integrity#

INV-X1: Bounded Order-Placement Account Surface#

INV-X2: No Crossed or Unsorted Book on Commit#

INV-X3: Single Canonical Fill-Accounting Transition#

INV-X4: Emergency Status Fails Closed#

Note on retired limits. Earlier protocol versions exposed max_orders_per_user and max_position_size config fields. Neither was ever enforced on-chain, so both were retired to reserved layout slots; the account byte layout is unchanged. The protocol does not impose a per-user open-order or position-size cap (see Known Limitations in the threat model). Do not rely on either limit existing.

Global Invariants#

INV-G1: Account Ownership#

All protocol accounts must be owned by the program.

forall account A managed by protocol:

A.owner == PROGRAM_ID

INV-G2: PDA Authenticity#

All PDAs must derive correctly from their seeds.

forall PDA P with seeds S and bump B:

P == create_program_address(S ++ [B], PROGRAM_ID)

INV-G3: Discriminator Integrity#

All accounts must have correct discriminators.

forall account A of type T:

A.data[0..8] == T::DISCRIMINATOR

Market Invariants#

INV-M1: Epoch Alignment#

Market timing must align to the configured duration epochs.

code

forall market M:
    M.t_start == M.market_id * M.duration_seconds
    M.t_end == M.t_start + M.duration_seconds
    M.t_start % M.duration_seconds == 0

INV-M2: Snapshot Immutability#

Once captured, snapshots never change.

code

forall market M:
    once(M.start_price != 0) -> always(M.start_price unchanged)
    once(M.end_price != 0) -> always(M.end_price unchanged)

INV-M3: Resolution Determinism#

Same snapshots produce same outcome.

code

forall markets M1, M2:
    (M1.start_price == M2.start_price AND M1.end_price == M2.end_price)
    -> M1.outcome == M2.outcome

INV-M4: State Monotonicity#

States only transition forward.

forall market M:

state(M) transitions only:

PENDING -> CREATED -> TRADING -> SETTLING -> RESOLVED -> CLOSED

INV-M5: Resolution Rule#

Outcome determined by price comparison.

forall resolved market M:

M.outcome == (M.end_price >= M.start_price ? UP : DOWN)

INV-M6: Oracle Feed-Identity Pinning#

code

forall market M, oracle entry point E in {start, end, expiry_late_capture}:
    let (addr_E, id_E) = the Pyth account address + feed_id supplied to E
    E proceeds to read a price
        -> addr_E == M.pyth_feed (creation-bound account address)
       AND id_E  == M.pyth_feed_id (creation-bound feed identifier)
    addr_E != M.pyth_feed     -> Err(OracleMismatch)   // substitute account rejected
    id_E   != M.pyth_feed_id  -> Err(FeedIdMismatch)    // wrong feed rejected

Production sites:

Start (binding event): src/processor/create_market.rs — validate_pyth_feed (L603), read_pyth_feed_id (L606), feed_id bound into the market PDA seed and stored via validate_create_market_pdas (L626-L641).
End snapshot: src/processor/snapshot.rs:218 validate_pyth_feed_address(accts.pyth_feed, &market_pyth_feed_addr) and src/processor/snapshot.rs:220 validate_pyth_feed_id(accts.pyth_feed, &ctx.pyth_feed_id).
Expiry late capture: src/processor/expire_market.rs:556 validate_pyth_feed_address(...); src/processor/expire_market.rs:716 validate_pyth_feed_address(...) and src/processor/expire_market.rs:722 validate_pyth_feed_id(...) inside try_late_price_capture.

Helpers: src/oracle/pyth.rs::validate_pyth_feed_address (L521-L532) and src/oracle/pyth.rs::validate_pyth_feed_id (L487-L501).

END snapshot: tests/security_wrong_feed_id.rs::test_attack_snapshot_end_wrong_feed_address_same_feed_id_rejected_by_oracle_mismatch drives the real SnapshotEnd instruction with a substitute account carrying the SAME feed_id but a different address, and asserts rejection with OracleMismatch at validate_pyth_feed_address — before validate_pyth_feed_id even runs.
EXPIRE late capture: src/processor/expire_market.rs::tests::expire_late_capture_rejects_substitute_feed_address supplies a Pyth account whose address differs from the market's bound pyth_feed and asserts determine_expire_market_resolution rejects with OracleMismatch at validate_pyth_feed_address (expire_market.rs:556).
START binding: at create-market the feed_id is read from the validated Pyth account and bound into the market PDA seed + stored market.pyth_feed; thereafter the END/EXPIRE paths re-pin against that bound value.

Order Book Invariants#

INV-O1: No Crossed Book#

Best bid must be less than best ask.

code

forall orderbook O with non-empty bids and asks:
    O.best_bid < O.best_ask

INV-O2: Price Bounds#

All prices within valid range.

forall order ord in orderbook:

0 < ord.price_bps < 10_000

INV-O3: Quantity Positive#

All orders have positive quantity.

forall order ord in orderbook:

ord.quantity > 0

INV-O4: Order Ownership#

All orders have valid owner positions.

forall order ord:

exists position P: P.owner == ord.owner

INV-O5: Sorted Orders#

Bids sorted descending, asks sorted ascending.

code

forall orderbook O:
    O.bids is sorted descending by price
    O.asks is sorted ascending by price

Position Invariants#

INV-P1: Non-Negative Shares#

No negative share balances.

code

forall position P:
    P.yes_shares >= 0
    P.no_shares >= 0

INV-P2: Locked Less Than Total#

Locked shares cannot exceed total.

code

forall position P:
    P.locked_yes_shares <= P.yes_shares
    P.locked_no_shares <= P.no_shares

INV-P3: Single Settlement#

Positions settle at most once.

code

forall position P:
    once(P.settled) -> always(P.settled)
    P.settled -> P.payout is final

INV-P4: Collateral Coverage#

Locked collateral covers buy orders.

forall position P:

P.collateral_locked == sum(buy_order.value for buy_order in P.orders)

Vault Invariants#

INV-V1: Solvency#

Vault covers worst-case payouts.

forall market M with vault V:

V.amount >= max(M.total_yes_shares, M.total_no_shares) + M.accumulated_creator_fees

INV-V2: Conservation#

Trading preserves total value.

forall trade T:

collateral_in == collateral_out + fees

INV-V3: Empty at Close#

Vault empty when market closes.

forall market M transitioning to CLOSED:

M.vault.amount == 0

Total shares match sum of positions.

code

forall market M:
    M.total_yes_shares == sum(P.yes_shares + P.locked_yes_shares for P in positions)
    M.total_no_shares == sum(P.no_shares + P.locked_no_shares for P in positions)

Timing Invariants#

INV-T1: Snapshot Timing#

Snapshots captured after boundaries.

code

forall market M:
    M.start_price_timestamp >= M.t_start
    M.end_price_timestamp >= M.t_end

INV-T2: Trading Window#

Trading only during trading period.

code

forall order placed at time t in market M:
    M.t_start <= t < M.t_end

INV-T3: Settlement After Resolution#

Settlement only after outcome determined.

forall settlement S in market M:

M.outcome != None

Fee Invariants#

INV-F1: Capped-Linear-Decay Curve#

Taker fees follow the capped-linear-decay curve, with the cap enforced at the curve ceiling.

code

forall trade T at fill price p:
    raw_bps(p) = decay_rate_bps * (10_000 - p) / 10_000
    fee_bps(p) = min(fee_cap_bps, raw_bps(p))
    T.taker_fee == T.value * fee_bps(p) / 10_000 (ceiling)

INV-F2: Three-Way Fee Split#

Every taker fee splits cleanly among protocol, creator, and referral. The three shares are bps of the fee and MUST sum to exactly 10_000.

code

forall config:
    config.protocol_fee_bps
        + config.default_creator_fee_bps
        + config.referral_share_bps_of_fee
        == 10_000

INV-F3: Referral Attribution Lifetime#

Referral attribution is first-touch and immutable for the configured lifetime.

forall referral_account R:

R.referrer is unchanged for (R.attributed_at, R.attributed_at + 365*86_400]

INV-F4: Referrer Earnings Solvency#

code

Σ_k referrer_treasury_k.balance >= Σ_referrer ReferrerEarningsAccount[r].accumulated   ; k ∈ [0, 8)

Multi-Fee-Recipients Invariants#

INV-FEE-T1: Config holds exactly 8 treasury recipients#

code

config.treasury_recipients.len() == MAX_TREASURY_RECIPIENTS == 8

The treasury recipient list is a fixed-size array of 8, enforced at compile time by the type system. There are always exactly 8 protocol-fee destination slots.

INV-FEE-T2: Every fee-paying instruction binds the recipient to the configured set#

code

∀ fee-paying ix:
  treasury_token_account.address() == config.treasury_recipients[protocol_treasury_index]
  AND treasury_token_account.mint == config.default_settlement_mint
  AND protocol_treasury_index < 8

An out-of-range index returns TreasuryIndexOutOfRange (0x8009); a mismatched address returns TreasuryRecipientMismatch (0x800A). Both are checked before any fee is moved.

INV-FEE-T3: System-wide solvency reconciliation across all shards#

code

Σ_{i=0..8} balance(config.treasury_recipients[i]) == Σ protocol_fees_collected (lifetime)

INV-FEE-T4: `UpdateTreasuryRecipients` rejects zero pubkeys#

code

update_treasury_recipients(new_recipients):
  ∀ i ∈ [0, 8):
    new_recipients[i] != [0u8; 32]     →   else InvalidTreasuryRecipient (0x800B)

A treasury rotation cannot install a zero (all-zero) address in any slot. Each new recipient must also be owned by the SPL Token program.

INV-FEE-T5: `UpdateTreasuryRecipients` rejects pairwise duplicates#

code

update_treasury_recipients(new_recipients):
  ∀ i, j ∈ [0, 8), i < j:
    new_recipients[i] != new_recipients[j]    →   else DuplicateTreasuryRecipient (0x800C)

No two slots may hold the same address. The same distinctness check runs at config initialization.

INV-REFERRAL-T1: Every `ReferrerEarningsAccount` has a valid bound shard#

∀ ReferrerEarningsAccount r:

r.treasury_index < MAX_TREASURY_RECIPIENTS == 8

INV-REFERRAL-T2: Per-shard credit/transfer pairing at PlaceOrder time#

code

∀ PlaceOrder credit Δ:
  ReferrerEarningsAccount[r].accumulated += Δ
  ⟺  TransferChecked(taker → referrer_treasury_<r.treasury_index>, Δ) succeeds
  AND referrer_treasury_<k> in the triple == derive_referrer_treasury_pda(k)

INV-REFERRAL-T3: System-wide per-shard solvency reconciliation#

code

Σ_{k=0..8} balance(referrer_treasury_k) == Σ_referrer ReferrerEarningsAccount[r].accumulated

Verification#

Runtime Checks#

Property Tests#

Formal Verification Targets#

Property	Method	Status
Solvency	K Framework	Target
Conservation	Certora	Target
No reentrancy	Static analysis	Done
Overflow safety	Clippy + MIRI	Done

Invariant Violations#

Detection#

Invariant violations manifest as:

Transaction failures with specific errors
Inconsistent state (detectable via indexer)
Unexpected account balances

Response#

Operational Notes#

A few behaviors are intentional and worth calling out for integrators so they are not mistaken for bugs:

Treasury recipients are admin-managed SPL token accounts, not PDAs. Protocol fees are sent to one of 8 configured SPL token accounts. Rebalancing funds between those 8 accounts is done by the admin off-chain; the protocol does not move balances between recipient slots automatically. The referrer treasury shards, by contrast, are program-derived and can only be debited by a referrer-signed ClaimReferrerEarnings.
A frozen treasury recipient degrades only its own shard. If a stablecoin issuer freezes one of the 8 protocol-fee token accounts, only orders that select that shard index fail; orders selecting any of the other 7 shards are unaffected. The admin can rotate the affected slot via UpdateTreasuryRecipients (subject to a one-hour rate limit).
Fee-config changes apply to live order flow, not retroactively to a resting order's terms. UpdateFeeConfig does not rewrite the fee owed on already-resting orders. Fees are always charged to the taker at the live curve at fill time, so a maker is never charged a fee for a change made after they posted. This matches the behavior of other on-chain order books and does not violate any invariant.

Price-Band Invariants#

INV-BAND-1: No-panic on any `u16` input#

compute_band never panics for any combination of u16 inputs. All arithmetic is saturating; no branch can produce an unhandled overflow or array out-of-bounds.

forall bid, bid_count, ask, ask_count : u16:

compute_band(bid, bid_count, ask, ask_count) terminates without panic

Verified by Kani proof proof_compute_band_no_panic (src/verification/price_band.rs).

INV-BAND-2: `lo ≤ hi` always#

The returned band is never inverted.

code

forall bid, bid_count, ask, ask_count : u16:
    let (lo, hi) = compute_band(bid, bid_count, ask, ask_count)
    lo <= hi

Verified by Kani proof proof_compute_band_bounds_invariant (src/verification/price_band.rs).

INV-BAND-3: Band width bounded by `2 × MAKER_BAND_BPS` when dynamic#

When the book is two-sided and non-sentinel, the dynamic band is at most 2 × MAKER_BAND_BPS (currently 2 × 1000 = 2000 bps) wide.

code

when bid_count > 0 AND ask_count > 0 AND best_bid > 0 AND best_ask < P_MAX:
    let (lo, hi) = compute_band(best_bid, bid_count, best_ask, ask_count)
    hi - lo <= 2 * MAKER_BAND_BPS

Verified by Kani proof proof_band_width_bounded_by_2x_band_bps (src/verification/price_band.rs).

INV-BAND-4: Midpoint lies within `[lo, hi]` when band is dynamic and unclipped#

When the book is two-sided and the midpoint is far enough from both static clamps that neither endpoint is clipped, the midpoint is contained in the band.

code

when bid_count > 0 AND ask_count > 0 AND best_bid > 0 AND best_ask < P_MAX
    AND mid >= STATIC_MIN_BPS_FOR_BAND + MAKER_BAND_BPS
    AND mid + MAKER_BAND_BPS <= STATIC_MAX_BPS_FOR_BAND:
    let (lo, hi) = compute_band(best_bid, bid_count, best_ask, ask_count)
    lo <= mid <= hi

Verified by Kani proof proof_band_contains_mid_when_not_clamped (src/verification/price_band.rs).

INV-BAND-5: IOC orders bypass the gate unconditionally#

ImmediateOrCancel orders never rest on the book and are therefore exempt from the price-band gate. check_maker_band returns Ok(()) immediately for IOC order types without computing any band.

forall canonical_price_bps : u16, orderbook : OrderbookAccount:

check_maker_band(canonical_price_bps, ImmediateOrCancel, orderbook) == Ok(())

Source: src/processor/place_order.rs::check_maker_band — early return on OrderType::ImmediateOrCancel.

INV-BAND-6: Gate executes after canonical conversion + tick alignment, before matching#

The band gate fires at a fixed point in the place_order flow:

After convert_to_canonical (NO-side prices flipped to YES-book coordinates).
After tick alignment (price rounded to the configured tick size).
Before the match step (rejected orders never touch matching state).

Next Steps#

See Threat Model for attack analysis
Review Architecture Security for implementation

Protocol Invariants#

Overview#

Execution-Path Integrity#

INV-X1: Bounded Order-Placement Account Surface#

INV-X2: No Crossed or Unsorted Book on Commit#

INV-X3: Single Canonical Fill-Accounting Transition#

INV-X4: Emergency Status Fails Closed#

Global Invariants#

INV-G1: Account Ownership#

INV-G2: PDA Authenticity#

INV-G3: Discriminator Integrity#

Market Invariants#

INV-M1: Epoch Alignment#

INV-M2: Snapshot Immutability#

INV-M3: Resolution Determinism#

INV-M4: State Monotonicity#

INV-M5: Resolution Rule#

INV-M6: Oracle Feed-Identity Pinning#

Order Book Invariants#

INV-O1: No Crossed Book#

INV-O2: Price Bounds#

INV-O3: Quantity Positive#

INV-O4: Order Ownership#

INV-O5: Sorted Orders#

Position Invariants#

INV-P1: Non-Negative Shares#

INV-P2: Locked Less Than Total#

INV-P3: Single Settlement#

INV-P4: Collateral Coverage#

Vault Invariants#

INV-V1: Solvency#

INV-V2: Conservation#

INV-V3: Empty at Close#

INV-V4: Share Balance#

Timing Invariants#

INV-T1: Snapshot Timing#

INV-T2: Trading Window#

INV-T3: Settlement After Resolution#

Fee Invariants#

INV-F1: Capped-Linear-Decay Curve#

INV-F2: Three-Way Fee Split#

INV-F3: Referral Attribution Lifetime#

INV-F4: Referrer Earnings Solvency#

Multi-Fee-Recipients Invariants#

INV-FEE-T1: Config holds exactly 8 treasury recipients#

INV-FEE-T2: Every fee-paying instruction binds the recipient to the configured set#

INV-FEE-T3: System-wide solvency reconciliation across all shards#

INV-FEE-T4: UpdateTreasuryRecipients rejects zero pubkeys#

INV-FEE-T5: UpdateTreasuryRecipients rejects pairwise duplicates#

INV-REFERRAL-T1: Every ReferrerEarningsAccount has a valid bound shard#

INV-REFERRAL-T2: Per-shard credit/transfer pairing at PlaceOrder time#

INV-REFERRAL-T3: System-wide per-shard solvency reconciliation#

Verification#

Runtime Checks#

Property Tests#

Formal Verification Targets#

Invariant Violations#

Detection#

Response#

Operational Notes#

Price-Band Invariants#

INV-BAND-1: No-panic on any u16 input#

INV-BAND-2: lo ≤ hi always#

INV-BAND-3: Band width bounded by 2 × MAKER_BAND_BPS when dynamic#

INV-BAND-4: Midpoint lies within [lo, hi] when band is dynamic and unclipped#

INV-BAND-5: IOC orders bypass the gate unconditionally#

INV-BAND-6: Gate executes after canonical conversion + tick alignment, before matching#

Next Steps#

Protocol Invariants#

Overview#

Execution-Path Integrity#

INV-X1: Bounded Order-Placement Account Surface#

INV-X2: No Crossed or Unsorted Book on Commit#

INV-X3: Single Canonical Fill-Accounting Transition#

INV-X4: Emergency Status Fails Closed#

Global Invariants#

INV-G1: Account Ownership#

INV-G2: PDA Authenticity#

INV-G3: Discriminator Integrity#

Market Invariants#

INV-FEE-T4: `UpdateTreasuryRecipients` rejects zero pubkeys#

INV-FEE-T5: `UpdateTreasuryRecipients` rejects pairwise duplicates#

INV-REFERRAL-T1: Every `ReferrerEarningsAccount` has a valid bound shard#

INV-BAND-1: No-panic on any `u16` input#

INV-BAND-2: `lo ≤ hi` always#

INV-BAND-3: Band width bounded by `2 × MAKER_BAND_BPS` when dynamic#

INV-BAND-4: Midpoint lies within `[lo, hi]` when band is dynamic and unclipped#

INV-FEE-T4: `UpdateTreasuryRecipients` rejects zero pubkeys#

INV-FEE-T5: `UpdateTreasuryRecipients` rejects pairwise duplicates#

INV-REFERRAL-T1: Every `ReferrerEarningsAccount` has a valid bound shard#

INV-BAND-1: No-panic on any `u16` input#

INV-BAND-2: `lo ≤ hi` always#

INV-BAND-3: Band width bounded by `2 × MAKER_BAND_BPS` when dynamic#

INV-BAND-4: Midpoint lies within `[lo, hi]` when band is dynamic and unclipped#