Protocol Invariants#

Protocol invariants, their enforcement layers, and the current verification roadmap for the Seesaw Solana program.

Overview#

Invariants are properties that must remain true across state transitions. Violating an invariant indicates a bug, an attack, or an off-chain reconciliation failure that operators must investigate. The catalog below is the authoritative INV-* list, but not every row has the same enforcement layer: some are enforced on-chain at runtime, some are proven or tested in the pure logic layer, and cross-account aggregate rows are reconciled by the indexer. The Machine-Checked and Exhaustive Verification section names the current evidence and remaining roadmap instead of presenting aspirational formal targets as completed proof.

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#

Disposition: enforced-on-chain

Placing an order never requires arbitrary maker-owned accounts. Every maker is addressed through a slot in the market's bounded trader-ledger account, and PlaceOrder applies the computed maker deltas to those slots synchronously. This keeps the instruction account surface fixed while allowing a taker to match against any resting maker represented in the ledger.

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

Disposition: enforced-on-chain (subset) + accepted (full form)

Before any order is allowed to rest, the matching path performs runtime no-cross, occupied-count, and cached-best rechecks against the committed orderbook state. The full every-occupied-slot ordering scan remains in the test/Kani layer, so the runtime tripwire is the cheap subset of the stronger INV-O1/INV-O5 catalog guarantee.

INV-X3: Single Canonical Maker-Delta Applicator#

Disposition: enforced-on-chain

Every maker fill is represented as a checked MakerFillDelta, and the BPF PlaceOrder apply phase credits that delta through apply_maker_fill_delta_to_slot. Free and locked YES, NO, and quote buckets therefore share one signed-delta applicator instead of duplicating arithmetic across fill branches.

INV-X4: Emergency Status Fails Closed#

Disposition: enforced-on-chain

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.

INV-X5: Maker Fill Credits Are Single-Application#

Disposition: enforced-on-chain

Every fill produces exactly one maker delta in the computation output, and a successful PlaceOrder applies that delta exactly once to the maker's trader-ledger slot. There is no post-fill claim instruction or replayable claim state. If any validation, checked arithmetic, or CPI fails, Solana's transaction atomicity commits none of the delta applications.

forall maker fill F in PlaceOrder output O:
    count(O.maker_fill_deltas, F) = 1
    PlaceOrder commits -> apply_to_trader_ledger(F) occurs exactly once
    PlaceOrder rejects -> apply_to_trader_ledger(F) commits zero times

This is the formal INV-* entry for synchronous maker accounting. The maker's slot key and all six bucket deltas are bound before the ledger mutation, and the slot applicator uses checked signed arithmetic for every bucket.

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#

Disposition: enforced-on-chain

All protocol accounts must be owned by the program.

INV-G2: PDA Authenticity#

Disposition: enforced-on-chain

All PDAs must derive correctly from their seeds.

Market, position, and trader-ledger account slots are explicitly pinned by the shared loaders in program/src/validation/loaders.rs:

• load_market_context first checks program owner and discriminator, then validates the market address against the loaded market seed fields: ["seesaw", "market", pyth_feed_id, duration_seconds, market_id, creator, bump]. This is circular but sound because the owner check proves the bytes are Seesaw-owned state, and the PDA check proves the supplied account address is the unique address for those bytes' seeds.
• load_position_context validates ["seesaw", "position", market, owner, bump] after owner/discriminator checks.
• load_trader_ledger_context validates ["seesaw", "trader_ledger", market, bump] after owner, header, parent-market, and capacity checks.

These loaders are used by both non-hot-path instructions and the order hot paths (PlaceOrder, *WithFreeFunds, cancel, reduce). No hot-path exemption is taken.

How a PDA account is accepted. A PDA account is accepted only when both of the following hold:

1. it is owned by the program — checked by the loader before its stored bump is read; and
2. its address equals create_program_address(seeds ++ [stored_bump], PROGRAM_ID).

Condition (1) is what makes the stored bump trustworthy: only the program can create program-owned accounts, and it always creates them with the canonical bump returned by find_program_address, so a bump read out of program-owned state is canonical by construction. Condition (2) is the load-bearing gate. A wrong or non-canonical bump either fails create_program_address outright (the derived point is on the curve) or reproduces a different address; either way the validate_*_pda address comparison rejects the account. The verification path therefore does not re-run the canonical-bump search: program/src/utils/pda.rs::create_pda performs a single create_program_address syscall (about 1,500 CU under the Solana cost model) where find_program_address would hash once per bump attempted. The unit test pda.rs::bump_verification_tests::non_canonical_bump_never_yields_canonical_address walks all 256 bumps for a representative PDA and confirms that no non-canonical bump reproduces the canonical address.

Accounts that are not yet program-owned carry no trustworthy bump, so first-time creation (position, trader-ledger, and every other derive_*_pda creation path) still uses find_program_address.

Spline vault. SplineAccount stores the canonical bump of its vault PDA in vault_bump (offset 12, carved from _header_reserved on 2026-08-27). InitSpline writes the bump it just used to allocate the vault, so the byte is canonical by construction, and the bump is only read after load_spline_context has already proved program ownership and re-derived the spline's own address. The five vault consumers (spline_vault, attach_spline, settle_spline, close_spline, recover_spline) therefore verify the vault with verify_spline_vault_pda (one create_program_address) and keep the address-equality gate unchanged. A vault_bump of zero identifies a legacy spline created before the carve; those fall back to find_program_address, which is safe for the same reason the pre-carve code was. Zero being the canonical bump is astronomically unlikely rather than impossible — it requires every one of bumps 255..1 to be on-curve, probability about 2^-255 — and a spline that did store a canonical zero would simply take the same search fallback, which reproduces the same address. The zero sentinel is therefore a performance discriminator, not a security one.

Fixed-seed PDAs. PDAs whose seeds are entirely constant — config, the "log" event-recorder authority, the resolver registry, and the eight referrer-treasury shards — skip the syscall altogether. program/src/utils/fixed_pdas.rs const-evaluates their address and canonical bump from the pinned build-time program ID. The two that carry a stored bump, verify_config_pda and verify_referrer_treasury_pda, compare that bump against the const canonical bump via require_canonical_bump; those two verifiers are the only remaining runtime callers of that helper. The rest are pure derivations (derive_config_pda, derive_resolver_registry_pda, derive_referrer_treasury_pda, events::recorder::log_authority_pda) that simply return the constant. For any other program ID (unit tests and fuzz harnesses use arbitrary IDs) the accessors return None and the caller falls back to the create_program_address path above. fixed_pdas::tests::constants_match_runtime_search_for_pinned_program_id re-derives every constant with find_program_address on each cargo test run, and program/tests/security_pda_validation.rs::test_fixed_pda_constants_match_deployed_program re-proves the table against the deployed program.

INV-G3: Discriminator Integrity#

Disposition: enforced-on-chain

All accounts must have correct discriminators.

Market Invariants#

INV-M1: Epoch Alignment#

Disposition: enforced-on-chain

Market timing must align to the configured duration epochs.

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#

Disposition: enforced-on-chain

Once captured, snapshots never change.

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#

Disposition: enforced-on-chain

Same snapshots produce same outcome.

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#

Disposition: enforced-on-chain

States only transition forward.

INV-M5: Resolution Rule#

Disposition: enforced-on-chain

Outcome determined by price comparison.

INV-M6: Oracle Feed-Identity Pinning#

Disposition: enforced-on-chain

Native markets are pull-only: no oracle account address is persisted. The two oracle entry points that read a price (start snapshot inside create_market, end snapshot in snapshot_end) validate the supplied ephemeral PriceUpdateV2 account against the pinned Pyth Receiver owner and discriminator, require full verification, and re-pin the embedded feed identifier against the market's creation-bound pyth_feed_id before reading any price. A substitute account carrying the same feed id at a different address is accepted by design; a different feed id is rejected. Terminal expiry (expire_market) reads no oracle at all: its trailing price_update slot is a legacy optional account that determine_expire_market_resolution ignores, so expiry always settles neutral (INV-M5 does not apply to expired markets).

Oracle freshness is anchored to publish_time, not PriceUpdateV2.posted_slot: a delayed historical print posted during pull-mode recovery receives a recent posting slot, so a slot-age bound would not detect staleness. The end-snapshot age bound applies only when prev_publish_time == 0 (firstness unprovable); a provably-first print is accepted at any age (spec/ORACLE.md §4.3b/§4.4).

forall market M, oracle entry point E in {start, end}:
    let id_E = feed id embedded in the Receiver-owned PriceUpdateV2 supplied to E
    E proceeds to read a price -> owner == PYTH_RECEIVER_PROGRAM_ID
                              AND id_E == M.pyth_feed_id
    id_E != M.pyth_feed_id -> Err(FeedIdMismatch)
expire_market never reads a price: outcome == Expired regardless of the optional slot

Production sites:

• Start (binding event): program/src/processor/create_market.rs reads the feed id from the validated Receiver account and binds it into the market PDA seed (["seesaw","market", pyth_feed_id, ...]) and market.pyth_feed_id.
• End snapshot: program/src/processor/snapshot.rs — validate_and_read_price (owner/discriminator/verification level) then if actual_feed_id != ctx.pyth_feed_id { FeedIdMismatch }.
• Expiry: program/src/processor/expire_market.rs::determine_expire_market_resolution takes the optional account as _price_update and never dereferences it.

Evidence: program/tests/security_wrong_feed_id.rs (wrong feed id rejected on the end path), program/tests/pyth_pull_lifecycle_adversarial.rs (owner, feed id, firstness, confidence at the account boundary), program/tests/security_late_capture_postfix.rs and program/tests/security_shard3_stage3_oracle_longtail.rs (expiry ignores the optional slot and settles neutral).

External-Market Resolver Invariants#

INV-EXT-1: Core Resolution Is Source-Agnostic#

Disposition: enforced-on-chain

The core never parses a source-specific proof. Native Pyth markets are selected by the all-zero resolver_authority sentinel and use the snapshot/resolve path. An external market commits to a nonzero resolver authority and can enter the external open, halt, resolve, and expiry paths without adding source-specific fields or proof verification to the core.

forall market M:
    M.resolver_authority == [0;32] -> only native Pyth lifecycle may resolve M
    M.resolver_authority != [0;32] -> only external resolver lifecycle may resolve M

The native snapshot/resolve path rejects an externally bound market, and SubmitResolution / ExpireExternalMarket reject a native market, with WrongResolver (0xA001).

INV-EXT-2: External Resolution and Halt Require a Verified Reclaim Claim Bound to the Market#

Disposition: enforced-on-chain

An external market's committed resolver_authority is the Seesaw-owned consumer-authority PDA ["seesaw","reclaim-consumer-v1", market], never a ResolverRegistry entry. ResolveExternalMarketWithReclaimV1 (0x54), HaltExternalMarketWithReclaimV1 (0x55), and ExtendExternalCloseWithReclaimV1 (0x56) are permissionless relays: any reporter may submit, and authorization comes entirely from a verified-claim receipt produced by the compile-time-pinned standalone verifier, which Seesaw CPIs into while signing as that consumer PDA. Before mutating, each route re-derives the consumer PDA from the market address, requires market.resolver_authority() to equal it, re-validates every receipt field returned by the verifier, and consumes a policy operation bit. Every bit except close extension (32) is one-shot; close extension records its bit on first use and stays available while the market is open, because a source market's close time may move more than once. The ResolverRegistry (0x48 / 0x49) is not consulted on any of these paths.

external_transition(M, policy, receipt) succeeds
    -> M.resolver_authority == pda(["seesaw","reclaim-consumer-v1", M])
   AND receipt is Verified by the pinned verifier for this market and claim digest
   AND (policy.operation_bitmap & operation_bit == 0
        OR operation_bit == EXTEND_CLOSE)          // one-shot except extension

Replay protection for a repeated extension does not come from the bitmap: each extension needs its own verified claim whose per-claim receipt PDA [consumer_program, market, signed_claim_digest] is vacant before the CPI, and each new close must be strictly greater than the current one.

INV-EXT-3: External Outcome Is Written Once#

Disposition: enforced-on-chain

External resolution is a one-way write. SubmitResolution and ExpireExternalMarket require both MarketMeta.resolved_marker == 0 and MarketAccount.outcome == None before writing payout numerators, resolved_at, the resolved marker, provenance, resolution template version, and the legacy binary outcome mirror. Proof provenance 0 requires a nonzero template version; admin provenance 1 and permissionless-expiry provenance 2 require version 0. The public callback rejects provenance 2, while expiry always clears any creation-time template value and writes (2, 0) atomically. No later resolver or expiry call may replace those values. HaltMarket is the intentional exception: halting is idempotent and does not write an outcome.

INV-EXT-4: One Market per Resolver, Platform, and External Reference#

Disposition: enforced-on-chain

An external market address is the canonical PDA ["seesaw", "market_ext", resolver_authority, platform_id, external_ref_hash]. Account initialization therefore admits at most one market for each (resolver_authority, platform_id, external_ref_hash) tuple; a duplicate open cannot create a second account. validate_open_external_args additionally requires external_ref_hash == sha256(external_ref[..external_ref_len]) on both public entry points (OpenExternalMarket and BeginExternalMarketPreallocation, matching the binding the native reclaim_create_mirror route already enforced). Without that binding the PDA uniqueness above held only over the hash: a resolver could open two distinct markets on the identical external_ref by supplying two different hashes, fragmenting liquidity and letting an indexer keyed on external_ref merge or mislabel markets that can resolve to contradictory outcomes. With the hash pinned to the reference, this invariant now holds over the external reference itself, not merely over its hash.

INV-EXT-5: Unknown Market Kinds Fail Closed#

Disposition: enforced-on-chain

Core supports market_kind = 0 (Binary) and market_kind = 1 (Scalar) only through the complementary two-leg engine. Binary accepts the two one-hot vectors or the even split; scalar accepts any checked complementary K2 vector. Every kind-sensitive decode rejects unknown values or a non-K2 shape with UnsupportedMarketKind (0xA005). Registry kind bits authorize a supported engine; they never make an unknown engine executable. Scalar bit 1 remains an explicit rollout-disabled policy until a registered adapter and the Phase E consumer/indexer surface bind the full typed scalar contract.

INV-EXT-6: Halt Blocks Placement but Preserves Exits#

Disposition: enforced-on-chain

Once MarketAccount.halted is set, all new order placement through the shared place-order loader rejects with MarketHalted (0xA006). Halting is not a funds freeze: owner cancellation, withdrawal, redemption after resolution, and permissionless external expiry remain available under their ordinary guards. This asymmetry lets keepers stop new exposure while users drain existing custody. A Reclaim V1 LeftOpen halt also leaves resolution available: it writes no outcome, so a later finalized claim that clears the unchanged close_ts + finality_delay_s bound resolves the market and the halt flags remain as history. Halting again and extending the close stay rejected.

INV-EXT-7: External Payouts Come Only from Authenticated Numerators#

Disposition: enforced-on-chain

For an external market, MarketMeta.payout_numerators is the sole settlement rate authority. The sidecar owner, PDA, stored market binding, resolved marker, leg count, market kind, complementary sum, and inactive zero suffix validate before mutation. Redeem, MarkPositionSettled, and terminal ask forfeiture in ReclaimExpiredOrder never convert the legacy Expired outcome mirror into 50/50 rates. Each leg payout is floored independently:

payout(amount, leg) = floor(amount * payout_numerators[leg] / 10_000)

External vault-originating transfers use the vault-self PDA signer; terminal ask forfeiture burns via the YES/NO escrow-self signer and performs no vault transfer. Terminal bid forfeiture releases the collateral lock and credits the full collateral to the maker's quote_free bucket; no resting-order principal is ever forfeited to the creator. AttachSpline and SettleSpline reject external markets before mutation because their native Pyth series contract has no external identity.

Canonical Reclaim invariant family: INV-RECLAIM-1 through INV-RECLAIM-4 apply to the standalone verifier V1 program and Seesaw's 0x52–0x56 CPI consumers. The legacy Ed25519 bridge tags 0x38–0x3F, 0x4A–0x4C, and 0x4F are permanently frozen.

INV-RECLAIM-1: Claim Identity Is Fully Bound#

Disposition: enforced-on-chain

The verifier recomputes the complete Reclaim identifier and EIP-191 signing digest from the submitted provider, parameters, canonical context, owner, timestamp, and epoch. Its receipt PDA binds the consumer program, market, signed-claim digest, and immutable proof buffer. Seesaw reparses the same proof, requires the exact deployment, program, market, source reference, operation, and reviewed condition hash committed by ExternalMarketPolicyV1, and derives the terminal transition and fact hash onchain.

INV-RECLAIM-2: Attestor Signature Policy Is Exact#

Disposition: enforced-on-chain

Epoch snapshots contain an ordered, unique attestor set (up to eight strictly ascending 20-byte addresses, zero-tailed beyond member_count) and an explicit threshold. Selection algorithm 1 is the single-member case (member_count == threshold == 1); algorithm 2 is threshold-of-set (1 <= threshold <= member_count <= 8). Any other snapshot shape - unknown algorithm, algorithm 1 with a multi-member set, zero or out-of-range threshold, unsorted, duplicated, zero or non-zero-tailed members - fails closed at both staging and decode.

Verification requires exactly threshold low-S recoverable signatures, reconstructs the digest internally, recovers each secp256k1 signer through the syscall, rejects duplicates, and requires every recovered Ethereum address to be a snapshot member. It records the members that signed in the receipt's signer_bitmap (bit i selects members[i]) and commits to sha256("seesaw-reclaim-signer-set-v1" || selected members in ascending index order), so wire signature order cannot change the commitment and a 1-of-1 snapshot produces exactly the single-member value.

The consumer re-verifies membership independently: Seesaw recomputes that commitment after the CPI from its own read of the active snapshot plus receipt.signer_bitmap, and rejects the claim unless popcount(signer_bitmap) == threshold, signer_bitmap < 1 << member_count, and the recomputed hash equals receipt.recovered_set_hash. A verifier that recovered too few, too many, or non-member signatures therefore cannot produce a receipt Seesaw accepts.

There is no Instructions sysvar, signature-precompile instruction, or multi-call witness bitmap.

INV-RECLAIM-3: Epoch Snapshot Rotation Fails Closed#

Disposition: enforced-on-chain

Governance stages a new immutable epoch snapshot whose epoch increases, whose previous-snapshot hash equals the active hash, and whose activation observes the configured timelock. A claim binds one exact snapshot and must fall within its validity interval and submission grace. Activation never rewrites an older snapshot or receipt.

INV-RECLAIM-4: Verifier Receipt Consumption Is One Shot#

Disposition: enforced-on-chain

External open, resolve, halt, and close-time extension accept only a verified, timely receipt for their exact proof buffer, consumer program, market, operation, and condition. The verifier atomically advances both receipt and proof buffer to Consumed; Seesaw then records the operation bit in the market policy in the same transaction. Replay fails because neither state can return to its prior status. Cleanup returns rent only to the recorded payer after the configured retention interval.

Event Recorder Invariants#

INV-EVENT-SEQ-1: A Sequence Number Is Consumed Only When a Batch Is Emitted#

Disposition: enforced-on-chain

The optional two-account recorder tail (self_program, log_authority) may be omitted from any instruction that carries it. When it is omitted, every recorder call in that instruction is a no-op, and the subject's event_sequence MUST NOT advance. event_sequence counts EMITTED RECORDER BATCHES, not transactions.

forall instruction I touching subject S:
    batches_emitted(I) = 0  ->  S.event_sequence' = S.event_sequence
    batches_emitted(I) = n  ->  S.event_sequence' = S.event_sequence + n
    and the n emitted batch headers carry exactly
        {S.event_sequence + 1, ..., S.event_sequence + n}

Subject S is the market (MarketAccount.event_sequence) for market-scoped events and the spline (SplineAccount.event_sequence) for detached spline-scoped events.

Why it is load-bearing. Off-chain consumers enforce strict contiguity: the indexer's market_event_sequences cursor admits a batch only when its header sequence equals last_sequence + 1 (apps/indexer/src/indexer/binaryEventProjection.ts). Before this invariant was enforced, the program advanced the counter on every market-touching instruction and only then discovered it had no tail to emit through. The consumed number named a batch that existed nowhere on chain, so a single tail-less transaction — an admin action through a builder that omitted the tail, a raw SDK caller, or an attacker deliberately submitting a stripped account list — permanently stalled that market's indexing with no on-chain artifact that could ever fill the gap. Enforcing the gate on chain removes both the operational failure mode and the denial-of-service vector.

Enforcement: bump_market_event_seq(market, recording) in program/src/processor/shared/settlement.rs returns 0 and leaves the counter untouched when recording is false; recording is events::recorder::recorder_tail_present(self_program, log_authority) for the exact pair the caller hands to the recorder. The spline paths apply the same guard around SplineAccount::bump_event_sequence. PlaceOrder composes the gate with its per-block emission predicates (program/src/processor/place_order.rs, program/src/processor/place_order/event_projection.rs).

Tests: program/tests/security_event_sequence_tail_gate.rs (LiteSVM: (a) tail-less PlaceOrder consumes nothing, (b) tailed PlaceOrder advances by exactly the batches emitted and every consumed number is carried by a real batch, (c) tail-less between two tailed transactions leaves the indexer-visible sequence contiguous); program/tests/security_event_recorder.rs (MintShares: economic deltas are identical across both paths while event_sequence advances only on the tailed one); program/tests/agentflow_fresh_16_reduce_events.rs (ReduceOrder).

INV-EVENT-SEQ-2: Emitted Sequences Are Strictly Increasing Per Subject#

Disposition: enforced-on-chain

Within a subject, every emitted batch carries a strictly larger sequence than every batch emitted before it, and the counter fails closed rather than wrapping.

forall subject S, emitted batches B1 before B2:
    B1.event_sequence < B2.event_sequence
    S.event_sequence = u64::MAX  ->  the instruction rejects (MathOverflow)

Ordering within one transaction is by event_sequence, NOT by log-emission order. PlaceOrder deliberately allocates the LOWER number to the placement batch and the higher one to the referral batch even though the referral block is recorded first in code order, because placement causes the fee that causes the referral accrual. Consumers must order by (slot, event_sequence).

Enforcement: MarketAccount::bump_event_sequence and SplineAccount::bump_event_sequence use checked_add and return MathOverflow at u64::MAX. The PlaceOrder pre-bump ordering lives in program/src/processor/place_order.rs.

Tests: program/tests/agentflow_fresh_14_event_sequence.rs; program/tests/agentflow_fresh_16_reduce_events.rs (reduce_success_fails_closed_when_event_sequence_would_overflow); apps/indexer/src/__tests__/binaryEventProjection.test.ts (the consumer side of the ordering contract).

Order Book Invariants#

INV-O1: No Crossed Book#

Disposition: enforced-on-chain

Best bid must be less than best ask.

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

Formal-proof bound (disclosure): The Kani no-crossed-book and aggregate PlaceOrder-conservation harnesses are BOUNDED over book depth, not exhaustive. The crossing/fill taker traversal is explored under #[kani::unwind(2)] (single fill) through #[kani::unwind(4)] (two fills) in formal/verification/processor_flow.rs, plus a concrete three-fill fixture (match_limit = 3) in formal/verification/conservation_multifill_widening.rs, against the bounded shallow-book fixture (capacity 63 per side) used by that formal harness, not the live deep RBT tiers. Conservation and no-crossing are therefore proven only for crossing sequences of at most three resting makers; a PlaceOrder that crosses four or more makers is outside the verified envelope and relies on the runtime book-consistency tripwire plus the sequence fuzzers (fuzz_market_lifecycle_real, fuzz_orderbook_operations). See formal/verification/mod.rs § "Bounded exploration disclosure".

INV-O2: Price Bounds#

Disposition: enforced-on-chain (subset) + accepted (full form)

Placement validates the candidate order's price. The full scan of all occupied slots is retained as test/Kani evidence; adding touched-slot assertions to the runtime book-consistency tripwire remains owner-gated on a measured CU cost.

All prices within valid range.

INV-O3: Quantity Positive#

Disposition: enforced-on-chain

All orders have positive quantity.

INV-O4: Order Ownership#

Disposition: accepted (test/proof-only)

Cancel and reduce bind the requested order to the caller's authoritative trader-ledger slot, so foreign-order mutation fails structurally. The stronger existential statement across every occupied order is an O(book) aggregate and is covered by formal/verification/order_ownership_reconciliation.rs, not by a full runtime scan.

All orders have valid owner positions.

INV-O5: Sorted Orders#

Disposition: enforced-on-chain (subset) + accepted (full form)

The mutation path enforces the no-cross/count/cache subset described by INV-X2. Complete ordering over every occupied slot remains test/Kani coverage because a hot-path full-book scan would regress compute cost.

Bids sorted descending, asks sorted ascending.

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

Position Invariants#

INV-P1: Non-Negative Shares#

Disposition: enforced-on-chain

No negative share balances.

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

INV-P2: Locked Less Than Total#

Disposition: accepted (test/proof-only)

Locked shares cannot exceed total.

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

Here yes_shares and no_shares are the available buckets; production accessors compute total shares as available plus locked with checked addition. The full accessor-domain property is covered by formal/verification/order_ownership_reconciliation.rs.

INV-P3: Single Settlement#

Disposition: enforced-on-chain

Positions settle at most once.

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

INV-P4: Collateral Coverage#

Disposition: enforced-on-chain (subset) + accepted (full form)

Each order transition uses checked collateral-lock deltas and authoritative trader-ledger slots. Recomputing the aggregate over every live order is retained as test/proof evidence rather than an instruction-path scan.

Locked collateral covers buy orders.

Vault Invariants#

INV-V1: Solvency#

Disposition: enforced-on-chain

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
             + M.accumulated_referral_fees

The max(total_yes_shares, total_no_shares) form above is the pre-resolution (Outcome::None) worst case: before resolution either side could win, so the vault must cover the larger. The runtime guard verify_solvency_after_share_change is outcome-aware once a market is resolved — the redeemable liability is only the winning side (Up → total_yes_shares, Down → total_no_shares, Expired → floor((total_yes_shares + total_no_shares) / 2)), plus accumulated_creator_fees and accumulated_referral_fees. This is a tightening of the liability estimate, not a loosening of the invariant: post-resolution, losing-side shares have zero claim on the vault, so counting them (as the pre-resolution max does) would spuriously flag insolvency as winning shares are burned and the vault drains during Redeem. The guard fails closed on an invalid/undecodable outcome and uses floor rounding for the expired split (any dust stays in the vault), so it can never under-reserve.

External settlement paths instead authenticate MarketMeta and compute floor(total_yes_shares * yes_rate / 10_000) + floor(total_no_shares * no_rate / 10_000) from its exact complementary numerators. Paths whose frozen account ABI has no metadata slot use the conservative max(total_yes_shares, total_no_shares) bound and may defer fee movement; they never substitute the legacy outcome mirror's 50/50 rate for a graded scalar vector.

Once an external market's resolution is committed, the exact graded liability is the floor for every vault debit, not just for redemption. The single rule is logic::redeem::resolved_external_liability_floor:

required = Σ_leg floor(total_shares_leg * numerator_leg / 10_000)
         + accumulated_creator_fees
         + referral_pending
         + spline_committed_collateral

logic::redeem::check_post_resolution_solvency{,_with_referral_pending} dispatches on the availability of that authenticated vector. Holding a post-resolution debit to max(total_yes_shares, total_no_shares) is NOT a safety margin: the losing leg's numerator is authenticated as zero, its shares are worth nothing, and nobody has any incentive to burn them — so the conservative floor never sheds and the creator's and referrers' accrued revenue becomes permanently unclaimable (platform E2E lane B, finding B-F6).

The split follows the availability of an authenticated payout vector, not the instruction:

• Redeem, MarkPositionSettled, and SettleSpline all carry the read-only MarketMeta slot on an external market, so all three preflight the exact graded liability through logic::redeem::ensure_external_redeem_post_transfer_solvency (floor per leg, then sum, plus creator fees, referral fees, and any remaining spline commitment). SettleSpline obtains both rates through redemption_numerator_for_leg, so it reproduces Redeem's resolved / leg-count / K=2 / complementary / zero-trailing validation before the array is used.
• ClaimCreatorFees (0x23) and RollupReferralFees (0x36) each grew an optional read-only MarketMeta slot, placed after their fixed head (and, for the rollup, after the position list) and before the optional recorder tail. Supplying it on a resolved external market takes the graded arm; omitting it preserves the legacy account shape and the conservative bound. processor::shared::settlement::load_resolved_external_numerators owns the shape contract: a native market must NOT supply the slot (InvalidInstructionData), and an unresolved external market that supplies it is rejected MarketNotResolved.
• AttachSpline and RecoverSpline operate only while the market is unresolved (compute_attach_spline requires MarketState::Trading; compute_recover_spline rejects market.is_resolved()), so no authenticated vector exists and either side could still take the full liability. They keep check_market_kind_solvency, whose external arm is the conservative max(total_yes_shares, total_no_shares) bound — the correct worst case there.
• ResolveMarket (0x05) and ExpireMarket (0x06) reject non-native markets outright, so the external arm of their shared creator-fee sweep (processor::shared::settlement::settle_creator_fees_or_defer) is unreachable and deliberately left conservative.

Per-leg flooring (never ceiling) is required, not merely permitted: for any partition of a leg's supply into individual positions Σ floor(position_i * rate / 10_000) <= floor(total * rate / 10_000), so the aggregate floor already dominates every possible sequence of per-position redemptions. Rounding a liability up would over-reserve relative to what holders can actually withdraw and strand 1–2 atoms of collateral permanently — a liveness failure with no solvency benefit.

INV-V2: Conservation#

Disposition: enforced-on-chain (subset) + accepted (full form)

Post-CPI token-delta checks reject local transfer drift. The composed all-instruction balance-sheet form is test/proof evidence and is tracked by V4/VER-03; it is not recomputed over every protocol account at runtime.

Trading preserves total value.

The composed form is reconciled against authoritative on-chain state by the invariant watchdog under INV-V4 (market.total_* == {yes,no}_mint.supply), not by summing Position mirrors. The one-sided indexed solvency assertion remains a separate, independently-reported check.

INV-V3: Empty at Close#

Disposition: enforced-on-chain

Vault empty when market closes.

INV-V4: Share Balance#

Disposition: enforced-on-chain (per-instruction subset) + monitored (composed form)

Runtime monitor: apps/indexer/src/jobs/invariantWatchdog.ts.

The invariant#

Market share totals are backed by the SPL supply of the market's own share mints plus the inventory held inside the market's attached market-maker spline. Every term is authoritative on-chain state:

forall market M:
    M.total_yes_shares == yes_mint(M).supply + sum(S.yes_inventory for S attached to M)
    M.total_no_shares  == no_mint(M).supply  + sum(S.no_inventory  for S attached to M)

A market has at most one attached spline — the creator-owned PDA derived from the market's own immutable identity (pyth_feed_id, duration_seconds, creator) (program/src/utils/pda.rs::derive_creator_spline_pda) — so the sums have at most one term. With no spline attached both inventories are zero and the statement collapses to plain supply equality M.total_side == side_mint.supply.

The share mints are canonical PDAs seeded from the market (["seesaw", "yes_mint", market] / ["seesaw", "no_mint", market]), each is its own mint authority, and neither has a freeze authority (program/src/processor/create_market.rs). MintShares mints and Redeem burns; both mutate the market total and the mint supply in the same instruction with checked arithmetic. Every other instruction that moves shares — escrow deposit on a resting ask, escrow release on cancel/reduce, taker fill transfer, WithdrawShares promotion from the trader ledger — is a transfer, so it conserves the inventory-inclusive total.

The spline terms are what make this a circulating-token reconciliation rather than a pure supply equality. A delivered sell-side share is burned as it moves into spline inventory, so the mint supply falls while the market total stays put; terminal SettleSpline / RecoverSpline then decrement the market totals by the full inventories and clear them, with no second burn (program/src/processor/settle_spline_trait.rs, program/src/state/market.rs::settle_spline_commitment). WithdrawShares carries the same statement inline: "The aggregate may already include spline inventory" (program/src/processor/withdraw_shares.rs). This is the same reconciliation stated under INV-SPLINE-5; see also INV-SPLINE-1 for the paired collateral aggregate. Treating INV-V4 as pure supply equality would flag every spline-attached market.

The per-instruction subset is what the program enforces; the composed equality across the whole market lifetime is what the watchdog monitors.

Position mirrors are local diagnostics, never aggregate custody#

UserPositionAccount.{yes,no}_shares and locked_{yes,no}_shares are a per-Position analytics mirror. They do not sum to the market total, and the retired M.total_yes_shares == sum(P.yes_shares + P.locked_yes_shares) form was never an invariant — every legitimate mint or fill flow violates it:

1. MintShares raises market.total_yes_shares and the mint supply with no Position account in the instruction at all (program/src/processor/mint_shares.rs:185-215). Minted supply is therefore permanently absent from every mirror until some later placement primes one.
2. A maker locks q YES; the maker Position records locked_yes = q.
3. A taker fills that order. The SPL tokens move from escrow to the taker, and the maker's proceeds are credited through MakerFillDelta into the TraderLedger (program/src/utils/trader_ledger.rs:48-73) — the maker Position is not even loaded, so it retains a stale locked_yes = q.
4. Ordinary taker fills deliberately carry a zero Position delta (program/src/logic/place_order_processor/types.rs:383-400).
5. The taker now rests a sell of that same q. Placement reads authoritative ATA/ledger custody, primes a fresh mirror to q, and moves it into locked state (program/src/processor/place_order_trait/mod.rs:831-855,917-961; place_order_trait/position_delta.rs:165-213).

Two Position rows now report 2q locked against q outstanding shares. An ordinary SPL transfer between wallets produces the same structural result. So neither exact equality nor an aggregate sum(P.locked_*) <= M.total_* bound is a settlement invariant, and neither may be used as an alert. WithdrawShares already treats the mirror as untrusted and clamps with saturating_sub (program/src/processor/withdraw_shares.rs:88-113).

What remains true is local: a resting Position's locked mirror agrees with that Position's own live orders.

forall market M, forall position P in M:
    P.locked_yes_shares == sum(o.remaining_quantity
                               for o in live_orders(M, P.owner)
                               if o is a canonical ask with original_side = SellYes)
    P.locked_no_shares  == sum(o.remaining_quantity
                               for o in live_orders(M, P.owner)
                               if o is a canonical ask with original_side = BuyNo)

Canonical bids lock quote collateral, not shares, so they contribute nothing to either sum. This property is scoped to a single Position and is never summed across Positions.

How it is monitored#

apps/indexer/src/jobs/invariantWatchdog.ts samples the market account, both share mints, and — when the market's SPLINE_FEATURE_BIT is set — its attached spline, in one RPC context per market. Single-context sampling is required, not merely tidy: SettleSpline decrements the market totals and clears the spline inventories atomically, so reading the two sides at different slots would manufacture drift. The mints are authenticated as the market's canonical self-authority PDAs; the spline is authenticated as the creator PDA derived from the market's own identity, bound to this market, with a commitment mirroring market.spline_committed_collateral (the INV-SPLINE-1 pairing that RecoverSpline itself enforces). Tolerance is zero: every term is an exact integer with no rounding.

The feature bit is the sole attachment marker, and settle_spline_commitment clears the bit, the commitment, and both inventories together — so a set bit means the spline account must exist and still be bound, and a clear bit means the inventory contribution is exactly zero.

A market advertising a spline whose account is missing or unbound is an integrity violation, never a silent zero-inventory pass. A skipped market is never counted as a pass either: the equality is simply unverified until RPC health is restored.

share_supply_integrity has two causes with different repairs, so the job logs a reason alongside the counter:

The counter and the alert are identical for both — a stale row keeps paging every sweep until it is repaired, which is the intended fail-closed direction. Only the log copy differs, so the operator is not sent looking for chain drift behind a row the chain has already finished with. The local mirror diagnostic is published on its own gauge precisely so that it can never page — the drift alert matches every label of seesaw_invariant_watchdog_violations.

The heartbeat table's market_conservation_violations column predates this redefinition and is retained because shipped migrations are immutable; it now carries the authoritative share-supply violation count.

INV-V5: Settlement/Share Decimal Identity#

Disposition: enforced-on-chain

The configured settlement mint and both market share mints use exactly 6 decimals, so one share base unit always has the same display scale as one settlement-token base unit.

config.default_settlement_mint.decimals
    == market.yes_mint.decimals
    == market.no_mint.decimals
    == SETTLEMENT_MINT_DECIMALS
    == 6

InitializeConfig rejects any settlement mint with a different decimal count before allocating the config PDA (InvalidSettlementMintDecimals, 0x7006). CreateMarket initializes YES and NO mints from the same production constant.

Timing Invariants#

INV-T1: Snapshot Timing#

Disposition: enforced-on-chain

Snapshots captured after boundaries.

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

INV-T2: Trading Window#

Disposition: enforced-on-chain

Trading only during trading period.

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

INV-T3: Settlement After Resolution#

Disposition: enforced-on-chain

Settlement only after outcome determined.

Fee Invariants#

INV-F1: Capped-Linear-Decay Curve#

Disposition: enforced-on-chain

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

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: Four-Way Fee Allocation#

Disposition: enforced-on-chain

Collected fees are conserved across protocol, creator, referral and credited maker rebates. The four configured shares are bps of fee and sum to 10_000. The shipped allocation is 50% protocol / 5% creator / 5% referral / 40% maker rebate. Eligible maker fills credit the maker's free quote balance; ineligible maker allocation and rounding dust go to protocol, as does the referral allocation without an eligible referrer. See fee constants and allocation details.

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

INV-F3: Referral Attribution Lifetime#

Disposition: enforced-on-chain

Referral attribution is first-touch and immutable for the configured lifetime. First-touch referral binding is permanent: after the 365-day active window expires, the ReferralAccount PDA persists, SetReferrer continues to reject with ReferrerAlreadySet, and no close/rebind path exists (rent remains locked). This is intentional anti-re-attribution-churn behavior.

INV-F4: Referrer Earnings Solvency#

Disposition: accepted (test/proof-only)

The on-chain per-referrer/per-shard coverage subset is enforced by INV-REFERRAL-T3. The hourly reconcileTreasuryShards job in apps/indexer/src/jobs/reconcileTreasuryShards.ts also records each shard's on-chain-versus-indexed drift, but a nonzero drift currently produces only a warning log and reconciliation row. infra/alerting/rules.yml pages when that job is stale, not when its drift is nonzero, so this row must not claim enforced-off-chain-with-alerting until OPS-02 wires a drift metric and alert.

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.

Σ_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. The program enforces the local liability and rollup coverage checks below; system-wide shard totals are also suitable for off-chain reconciliation.

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

Disposition: enforced-on-chain

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#

Disposition: enforced-on-chain

For every fee-paying instruction (PlaceOrder), the supplied treasury_token_account MUST equal one configured recipient in config.treasury_recipients[0..8). The instruction arg protocol_treasury_index is the requested shard; if that shard is unhealthy or the caller supplies a different healthy configured shard, load_place_order_context records the matching configured slot as the effective shard used for transfer and events. The token account MUST be a valid initialized SPL Token v1 account whose mint equals the configured settlement mint.

∀ fee-paying ix:
  ∃ effective_index ∈ [0, 8):
    treasury_token_account.address() == config.treasury_recipients[effective_index]
  AND treasury_token_account.mint == config.default_settlement_mint
  AND protocol_treasury_index < 8
  AND OrderFilled.effective_protocol_treasury_index == effective_index

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

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

Disposition: accepted (test/proof-only)

Σ_{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. The hourly reconcileTreasuryShards job records protocol-shard on-chain-versus-indexed drift and logs nonzero values, but the checked-in alert rules only cover reconciler staleness. Until OPS-02 exports nonzero drift to a paged alert, the job is useful reconciliation evidence but does not qualify as enforced-off-chain-with-alerting.

INV-FEE-T4: UpdateTreasuryRecipients rejects zero pubkeys#

Disposition: enforced-on-chain

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

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#

Disposition: enforced-on-chain

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

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#

Disposition: enforced-on-chain

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: Market-local deferred liabilities reconcile#

Disposition: enforced-on-chain

PlaceOrder retains active referral fees in the market vault. Each amount is recorded both on the taker's position and in the market aggregate, so the new liability fields reconcile exactly:

∀ market M:
  M.accumulated_referral_fees
    == Σ P.pending_referral_fees for positions P belonging to M

PlaceOrder defer Δ:
  P.pending_referral_fees += Δ
  M.accumulated_referral_fees += Δ

RollupReferralFees batch amount Δ:
  each included P.pending_referral_fees = 0
  M.accumulated_referral_fees -= Δ

After the seven-day terminal grace window, ClosePosition may perform the same local liability reduction while adding the forfeited amount to M.accumulated_creator_fees. Checked arithmetic rejects aggregate drift with ReferralLiabilityMismatch.

INV-REFERRAL-T3: Rollup preserves treasury coverage#

Disposition: enforced-on-chain

Before extending a referrer's earnings liability, RollupReferralFees requires the bound treasury shard to cover the referrer's existing accumulated earnings. It then transfers and credits the same batch amount atomically:

∀ referrer r bound to shard k:
  balance(referrer_treasury_k) >= ReferrerEarningsAccount[r].accumulated

RollupReferralFees batch amount Δ:
  TransferChecked(market.vault → referrer_treasury_k, Δ)
  ReferrerEarningsAccount[r].accumulated += Δ

The supplied treasury must be the PDA derived from the earnings account's immutable treasury_index; a mismatch returns ReferrerTreasuryMismatch (0x8005). Because the transfer and credit share one atomic instruction, the coverage inequality remains true after a successful rollup.

Verification#

Disposition Summary#

The disposition vocabulary is closed: enforced-on-chain, enforced-on-chain (subset) + accepted (full form), enforced-off-chain-with-alerting, dormant activation requirement, and accepted (test/proof-only). An on-chain failure rejects the transaction atomically. “Accepted” means the full aggregate is a release-test/proof obligation; it does not mean operators may ignore a detected violation. No current row claims enforced-off-chain-with-alerting: the indexed invariant watchdog has real alerts for its own projections, but the aggregate share and treasury rows below still lack the finalized-account or nonzero-drift alert required to use that label.

Runtime Checks#

The on-chain program now enforces a cheap fail-closed subset of the expensive invariant helpers on mutation paths:

• Solvency: Funds and trading paths reject if vault.amount < max(total_yes_shares, total_no_shares) + accumulated_creator_fees + accumulated_referral_fees (or the resolved/expired equivalent from MarketAccount::check_solvency). Within the selected funds/trading paths covered by FUNDS-08, the frozen public error mappings are:

  Code	Variant	Semantics and emitters
  0x5005	InsolvencyDetected	Pre-transfer vault-coverage guard in WithdrawFunds.
  0x7004	SolvencyViolation	Post-mutation tripwire in WithdrawFunds, WithdrawShares, and DepositFunds.
  0x7005	SolvencyInvariantViolated	Post-mutation tripwire in MintShares, Redeem, and PlaceOrder.

  These emitter lists are deliberately scoped to the FUNDS-08 funds/trading family and are not a globally exhaustive inventory of every instruction that may return these shared variants.

  New instructions MUST standardize on one post-check variant; existing codes are frozen and MUST NOT be renumbered.

• Orderbook consistency: the place-order applicator rejects if occupied bid/ask counts drift from the written slots, if cached best bid/ask prices do not match the first matchable slot, or if a matchable complementary bid/ask pair remains crossed. Count/cache failures return BookConsistencyInvariantViolated (0x301B); crossed-book failures return CrossedBookInvariantViolated (0x301C).

• Transfer conservation: settlement and redemption paths still verify post-CPI vault deltas exactly where tokens move, so a successful transfer must reduce the vault by the expected payout.

The full verify_orderbook_invariants helper additionally checks complete ordering and price bounds across every occupied slot; that broader scan remains test/Kani coverage rather than a release hot-path scan. Solvency is also enforced structurally by escrowed collateral, SPL token transfer failure, checked share-supply mutations, and max-share caps; the runtime check is a post-mutation tripwire, not the only solvency mechanism.

Property Tests#

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

Machine-Checked and Exhaustive Verification#

The formal-verification surface for this Solana program is Rust-native: Kani proofs, Lean refinement notes, golden-vector conformance, fuzzing, and runtime tripwires. Non-Solana formal tooling is not part of the current verification plan.

The authoritative machine-readable inventory is docs/kani-inventory.yaml, with tractability notes in docs/kani-tractable-inventory.yaml. Claims in this document should be updated from those inventories rather than from stale proof counts or aspirational tooling lists.

qedsvm Scope#

The qedsvm lane is an early-reject parity smoke check for compiled SBF fixtures, not a full terminal-instruction replay proof. Successful terminal Redeem and MarkPositionSettled replay remain out of scope until the harness models the required clock/sysvar controls and complete SPL Token CPI setup. Treat qedsvm evidence as complementary to Kani, property tests, fuzzing, and runtime tripwires rather than as end-to-end settlement proof. The executable scope banner and exact runnable fixture classes are documented in tools/qedsvm/README.md; release evidence must categorize these artifacts as parity-smoke, never as terminal or settlement evidence.

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 reroutes to a configured healthy shard. If a stablecoin issuer freezes one of the 8 protocol-fee token accounts, callers can provide any other live recipient from config.treasury_recipients[0..8). The order records the effective shard in OrderFilled.effective_protocol_treasury_index, and the indexer stores that effective value in trades.protocol_treasury_index for reconciliation. No fallback may route fees to a non-configured account.
• 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 program/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 program/src/verification/price_band.rs.

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

Disposition: accepted (test/proof-only)

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.

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

INV-BAND-2: lo ≤ hi always#

Disposition: accepted (test/proof-only)

The returned band is never inverted.

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 (program/src/verification/price_band.rs).

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

Disposition: accepted (test/proof-only)

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.

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 (program/src/verification/price_band.rs).

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

Disposition: accepted (test/proof-only)

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.

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 (program/src/verification/price_band.rs).

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

Disposition: enforced-on-chain

ImmediateOrCancel orders never rest on the book and are therefore exempt from the price-band gate. The header-based gate returns Ok(()) immediately when its IOC flag is set, without computing any band.

forall canonical_price_bps : u16, best_bid : u16, best_ask : u16,
       bid_count : u16, ask_count : u16:
    check_maker_band_from_header(
        canonical_price_bps, true, best_bid, bid_count, best_ask, ask_count
    ) == Ok(())

Source: program/src/processor/place_order.rs::check_maker_band_from_header.

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

Disposition: enforced-on-chain

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

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

Source: program/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 program/tests/concurrency_price_band.rs and program/tests/determinism_price_band.rs.

Market-maker spline invariants#

INV-SPLINE-1: Aggregate commitment conservation#

Disposition: enforced-on-chain

The market aggregate equals the checked sum of attached spline commitments. Attach adds the exact transferred amount, each fill subtracts the exact maker collateral spent (and may add an exact rebate), and settlement removes the exact remainder. The aggregate never exceeds the market vault balance available above other liabilities.

INV-SPLINE-2: Shape exposure is commitment-bounded#

Disposition: enforced-on-chain

Attachment and every attached shape update compute worst-case exposure using the frozen attachment tick size and require committed_collateral >= max(config_minimum, exposure). Region counts, order, overlap, density, and nonempty-side rules are validated before commit.

INV-SPLINE-3: Extended solvency and pair mint#

Disposition: enforced-on-chain (subset) + accepted (full form)

vault >= max(total_yes_shares, total_no_shares)
         + spline_committed_collateral
         + accumulated_creator_fees
         + accumulated_referral_fees

Pair-mint routes increase YES and NO liabilities together and mint/credit only the taker's selected side. Delivered-share routes move real taker inventory into the spline and never double-debit or double-count the delivered side.

INV-SPLINE-4: Virtual quotes never cross#

Disposition: enforced-on-chain (subset) + accepted (full form)

For every valid active shape, the best generated bid is strictly below the best generated ask. Unified matching preserves price priority with deterministic book-before-spline tie breaks. The bounded shape domain is also covered by formal proof.

INV-SPLINE-5: Settlement retires both full inventories#

Disposition: enforced-on-chain

Terminal settlement decrements the market's YES and NO totals by the spline's full corresponding inventories exactly once, performs no second token burn, clears both inventories and all attachment fields, and removes the registry slot. A repeated detached settlement is a no-op.

The circulating-token reconciliation is therefore:

total_side = circulating SPL(side) + sum(attached spline inventory(side))

Trader-ledger free shares remain outside total_side. In particular, an SPL sell-side share burned while transferred into spline inventory leaves the inventory-inclusive total unchanged until settlement.

This is the same statement as INV-V4, which is defined on it and which the invariant watchdog checks per market. INV-V4 is not a pure total_side == side_mint.supply equality; asserting that form would flag every spline-attached market.

Deep Orderbook v3 Four-Lane Invariants#

These invariants govern the version-1 deep-orderbook account layout, which replaces the mixed-original-side tree per canonical arena with four independent logical price-time lanes over the same two physical arenas. Full rationale lives in docs/superpowers/specs/2026-07-15-deep-orderbook-v3-four-lane-design.md; the implementation is program/src/logic/deep_orderbook/{lane,tree,view,order_id,cursor}.rs.

INV-DOB-V3-1: Four Logical Lanes, Two Shared Physical Arenas#

Disposition: enforced-on-chain

Each canonical arena hosts exactly two logical lanes — the arena's primary (namesake) lane and a secondary lane holding the complementary original side normalized onto that arena. The two lanes of an arena share its free list, node array, order array, and aggregate capacity; they never share a tree.

canonical bid arena: primary lane = BuyYes,  secondary lane = SellNo
canonical ask arena: primary lane = SellYes, secondary lane = BuyNo

DeepOrderbookLane (program/src/logic/deep_orderbook/lane.rs) is the single source of truth for this mapping; from_order_side is total over every OrderSide variant and callers must not thread loose (CanonicalSide, bool) pairs in its place.

INV-DOB-V3-2: Lane and Capacity Aggregate Accounting#

Disposition: enforced-on-chain

Per arena, the two lane lengths sum to the account-header occupied count, and occupied plus free slots equal the shared capacity:

forall arena A in {bid, ask}:
    A.primary_len + A.secondary_len == account_header.{bid_count|ask_count}
    A.occupied + A.free == A.capacity

Checked by DeepOrderbookView::validate_side_boundary (program/src/logic/deep_orderbook/view.rs), which rejects any header whose primary_len + secondary_len disagrees with the aggregate count, whose declared capacity disagrees with the account's shared capacity, or whose free-slot presence disagrees with total_len < capacity.

INV-DOB-V3-3: Single-Lane Slot Reachability#

Disposition: enforced-on-chain (subset) + accepted (full form)

No occupied physical slot is reachable from both lane roots of an arena, and every occupied slot is reachable from exactly one lane root. Root/best pointer consistency is checked on every mutation; the full reachable-set disjointness scan across every occupied slot is validate_full (DeepOrderbookView::validate_full, program/src/logic/deep_orderbook/view.rs) release/test evidence rather than a hot-path scan.

forall arena A, occupied slot S in A:
    exists exactly one lane L in {A.primary, A.secondary}:
        S reachable from L.root

INV-DOB-V3-4: Lane Authority Is the Stored Order, Never the Caller#

Disposition: enforced-on-chain

Insertion derives the lane from the order being inserted; removal, topology mutation, and cursor resumption derive it from the stored order's original_side before touching any link. A caller-supplied canonical side is read for arena addressing only — it is never sufficient authority to choose which lane root a slot belongs to.

forall stored order O at physical slot (side, slot):
    lane(O) == DeepOrderbookLane::from_order_side(O.original_side)
    -- never a function of a caller-provided side alone

Enforced at every mutation site that derives a lane from a stored order, e.g. program/src/logic/deep_orderbook/tree.rs (removal/topology change) and program/src/logic/deep_orderbook/view.rs (matching traversal, cursor resume).

INV-DOB-V3-5: Exact-Complementary Matching Only#

Disposition: enforced-on-chain

The matcher derives the exact maker lane once from the taker's original side and traverses only that lane; it is a fixed-point-free involution over the four lanes, so a taker never matches its own lane or a non-complementary lane.

BuyYes taker -> SellYes maker lane
SellNo taker -> BuyNo   maker lane
SellYes taker -> BuyYes  maker lane
BuyNo taker  -> SellNo   maker lane

forall lane L: L.complementary_maker().complementary_maker() == L
forall lane L: L.complementary_maker() != L

DeepOrderbookLane::complementary_maker (program/src/logic/deep_orderbook/lane.rs) is the sole complement mapping; noncomplementary liquidity consumes neither the match counter nor traversal CU.

INV-DOB-V3-6: Merged Canonical Reads Preserve Strict Price-Time Order#

Disposition: enforced-on-chain (subset) + accepted (full form)

The two-way merged canonical cursor advances only the selected lane and always returns the globally next candidate by (sort_price_bps, order_id) across both lanes of an arena, so public decoded bids/asks remain a single globally ordered stream. Per-mutation checks enforce the merge step; the full-traversal strict-ordering property across every occupied slot is validate_full release/test evidence.

forall arena A, consecutive candidates (C1, C2) from the merged cursor over A:
    (C1.sort_price_bps, C1.order_id) is strictly before
    (C2.sort_price_bps, C2.order_id) in canonical priority order

INV-DOB-V3-7: Order-ID Formula Is Lane-Free and Byte-Compatible#

Disposition: enforced-on-chain

The opaque order-ID codec is unchanged by the four-lane rewrite: it encodes only (sequence, CanonicalSide, slot, capacity) and carries no lane bit.

id = sequence * (2 * capacity) + canonical_side_offset + slot + 1

OrderHandle::encode/decode (program/src/logic/deep_orderbook/order_id.rs) is the sole codec; OrderLocator remains (canonical_side, physical_slot) and a slot's lane is always re-derived from the stored order's original_side at read time, never packed into the ID.

INV-DOB-V3-8: Mutation Rollback Restores Every Lane Byte-for-Byte#

Disposition: enforced-on-chain

Insertion, removal, and topology mutation across both lanes of an arena run under one rollback journal per instruction. On any failure the journal restores both lane triples (root/free_head/len/capacity/best_slot/ secondary_root/secondary_len/secondary_best_slot), nodes, orders, aggregate counts, and the next-order-sequence byte exactly to their pre-mutation values.

forall mutation batch M on arena A:
    M fails -> A.bytes_after == A.bytes_before  (exact, both lanes)

Enforced by with_rollback_journal (program/src/logic/deep_orderbook/tree.rs), which rolls back data from the journal whenever the wrapped body returns Err.

INV-DOB-V3-9: Reclaim-Gated Structural Best/Worst Fails Closed#

Disposition: enforced-on-chain

Structural best/worst lookups never scan the arena and never cache a clock-based "active" result (time can invalidate a cache without an account mutation). If a structural lane-worst or lane-best candidate is active but expired-claimable or TTL-reclaimable, the operation that depends on it (eviction, new-resting-order admission) fails closed until permissionless reclaim removes that node. An inactive-but-occupied candidate is never treated as reclaimable — it is tree corruption and rejects immediately via OrderbookTreeCorruption.

forall lane-worst or lane-best candidate S:
    S.active AND (S.expired_claimable OR S.ttl_reclaimable)
        -> dependent operation fails-closed (reclaim-required), does not evict/rest
    NOT S.active AND S.occupied
        -> OrderbookTreeCorruption (never classified reclaimable)

This trades bounded liveness (a stale node can transiently block admission until reclaimed) for an O(1) structural safety check instead of a full-book scan; see program/src/logic/deep_orderbook/view.rs and program/src/processor/place_order_trait/mod.rs (ReclaimRequired, OrderbookTreeCorruption).

INV-DOB-V3-10: Account Version 1, Layout Sizes Unchanged#

Disposition: enforced-on-chain

DeepOrderbookAccountHeader::VERSION is 1. Any other value fails closed in the program and every decoder — pre-four-lane bytes are never reinterpreted in place, because their two side-header fields encode one combined tree rather than a primary/secondary lane pair. Every tier's serialized size is unchanged by the rewrite:

account_size = 192 + 224 * capacity
capacity in {64, 128, 256, 512, 1024, 2048, 4096}

DeepOrderbookAccountHeader::VERSION: u8 = 1 (program/src/state/deep_orderbook.rs) gates every loader; the 32-byte side header is reinterpreted without resizing (primary root/free_head/len/capacity/ best_slot at the same offsets 0/4/8/12/16, secondary root/len/best_slot at offsets 20/24/28, reserve reduced to zero).

Next Steps#

• See Threat Model for attack analysis
• Review Architecture Security for implementation