Seesaw Verification Assurance Report#

Date: 2026-08-03 Program: Seesaw on-chain binary prediction market (Solana), program ID SEEsawgSrxRsgtKRbaThZFEKrVqX3Y64hDipTWyi8F8 Scope: The on-chain program in program/src/ and its formal (formal/verification/), fuzz (fuzz/), property, and integration test suites, as of the verification-suite gap-closure plan (Tasks 1–24, branch verify/proof-sensitivity-inv-m5). Audience: A security-literate stakeholder deciding on mainnet deployment. Prior audit status: The program has not undergone a human third-party security audit. This report synthesizes the internal verification effort; it is not a substitute for external review.

1. How to read this report — the assurance framing#

This report is written against evidence, not intent. Every strong claim below carries its scope, and every "proven" or "tested" statement cites the harness or test file that backs it. Where evidence does not exist, the claim is stated as not verified rather than softened.

The precise and only claim this report makes about the machine-checked properties is:

Under the documented assumptions (docs/security/assumptions.md, FV-ASM-001…021), the listed machine-checked properties hold for the modeled implementation and the explored state space — where "modeled implementation" and "explored state space" are exactly the domain of each cited Kani harness, and no wider.

This report does not claim the program is free of defects, unbreakable, or secure in any absolute sense. Formal proofs here establish properties within bounded models; tests establish behavior on the inputs exercised; neither generalizes beyond its stated envelope. A property proven under #[kani::unwind(4)] is proven for that unwind depth and no deeper. A property "tested" is established for the concrete fixtures run, not for all reachable states.

The evidence base is four committed documents, and this report is their synthesis:

• docs/security/traceability.md — the 75-row INV-* → evidence matrix, with a hand-verified coverage class per invariant (Task 20). It is the spine of Sections 3–6.
• docs/security/assumptions.md — 21 environmental/trust assumptions FV-ASM-001…021 (Task 21). The basis of Section 2's "under which assumptions."
• docs/security/residual-risk.md — 27 residual-risk rows, of which 4 are marked blocks deployment = Y (Task 22). The basis of Sections 7–8.
• docs/internal/mutation-baseline-2026-08-03.md — the first executable mutation baseline (Task 2). The basis of Section 9.

Coverage-class distribution (75 invariants)#

These classes are deliberately not collapsed into a single percentage. A percentage would destroy exactly the distinction between "proven full-type," "proven only within a bound," and "not verified" — which is the entire point of an honest assurance statement.

2. Deployment-blocking items (read before deciding)#

The residual-risk register (Task 22) marks four items as blocks deployment = Y — meaning each should be closed, or formally waived by the deployer, before mainnet. They are surfaced here first, deliberately, because the rest of this report's positive results do not offset them.

Beyond these four, two operational dependencies from the assumptions registry are effectively launch prerequisites even though they are not program defects: the upgrade authority must be under the documented Squads multisig custody (FV-ASM-007/008), and the deployed seesaw.so must be verified byte-reproducible against the reviewed commit (FV-ASM-015/017). Neither is verifiable from source; both are release-evidence obligations.

3. What was PROVEN — and under which assumptions#

Seven invariants carry a proven class in the traceability matrix: a Kani harness explores the full input type (every value CBMC can enumerate). Each is listed below with its named harness(es) — all confirmed present in docs/kani-inventory.yaml — and the assumptions the proof rests on.

A universal caveat applies to every row: these are proofs about the modeled logic layer, and they inherit the whole-program assumptions FV-ASM-001 (SPL Token v1 is 1:1, no hooks), FV-ASM-014 (Solana's Ed25519/secp256k1/SHA-256 primitives are sound), FV-ASM-016/017 (the build is un-tampered and reproducible), and FV-ASM-018 (the Solana runtime provides transaction-scoped locking and no re-entrant CPI). A proof over compute_outcome says nothing if the deployed bytecode is not the audited source.

Honest count: 7 invariants carry the proven label; 6 of them are full-type value proofs (INV-G2, INV-M3, INV-M5, INV-T2, INV-T3, INV-F2); the 7th (INV-BAND-1) is a no-panic smoke proof. Every harness named above was grep-confirmed to exist in docs/kani-inventory.yaml.

4. What was BOUNDED — proven, but only within a model#

Thirty-nine invariants are boundedly-verified: a Kani proof over a protocol-bounded, representative, or unwind-/capacity-bounded domain. These are faithful but non-exhaustive envelopes. Over-reading them as full-type proofs would overstate assurance (RR-FV-03). The load-bearing bounds a deployer must understand:

4.1 Order-book conservation and no-crossed-book (the most important bound)#

INV-V2 (Conservation), INV-O1 (No Crossed Book), INV-X2, INV-O2/O3/O5 — the order-book solvency, conservation, and sort/no-cross properties are proven only within a shallow fill envelope, not as a theorem over the full book:

• Conservation (INV-V2, partially-covered) runs at #[kani::unwind(2)] (one fill) through #[kani::unwind(4)] (two fills), with match_limit = 3 (≤ 3 maker crosses), against a book capacity of MAX_BIDS = MAX_ASKS = 63. A PlaceOrder crossing 4+ makers in one instruction is outside the verified envelope (FV-ASM-021) and relies on the runtime solvency tripwire (processor_flow.rs::place_order_post_cpi_solvency_gate_matches_market_check, which executes on every fill and fails the transaction closed) plus fuzz/property tests — not on proof. The bounded 3-fill fixture lives in formal/verification/conservation_multifill_widening.rs (match_limit = 3).
• The no-crossed-book harnesses run deeper than conservation — at unwind(8) and unwind(33) (orderbook_invariants.rs::crossed_book_rejected_by_invariant_checker, ::insert_bid_no_crossing; processor_flow.rs::apply_orderbook_updates_resting_bid_preserves_sort_or_rejects_cross) — but this is still a different, finite bound, not a full-depth proof.

This is disclosed at INV-O1 in docs/security/invariants.md and tracked as RR-OB-01. Deep-fill assurance rests on the differential/deep-orderbook fuzz drivers and property tests.

4.2 Other representative bounds worth naming#

• INV-V1 Solvency — solvency_fee_inclusive.rs::solvency_fee_inclusive_redeem + the post-CPI gate, plus security_solvency_stateful_fuzz.rs. Proven fee-inclusive on redeem; deep-book solvency inherits the §4.1 maker-cross bound.
• INV-P3 Single Settlement — single_settlement.rs::redeem_settled_byte_monotone_full_symbolic proves the settled byte is monotone over its full symbolic u8 domain; ::redeem_two_call_replay_is_idempotent is the inductive replay step. Strong, but share/collateral counters are u16-widened.
• INV-EXT-1..7 / INV-RECLAIM-1..4 — external-market and Reclaim binding are covered by the current native/LiteSVM lifecycle and security suites; external_halt.rs::external_halt_live_applier_is_idempotent additionally proves the live halt mutation. The Ed25519-via-instructions-sysvar path is a runtime-trust boundary (FV-ASM-019), not a Kani target.
• INV-EXT-7 external payouts — settlement_conservation.rs::scalar_paired_payout_conserves_collateral proves bounded live payout arithmetic; authenticated-numerator binding remains covered by the native/LiteSVM lifecycle and security suites.
• INV-M2 Snapshot Immutability — snapshot_write_path.rs::snapshot_write_captured_different_value_rejected and the start-write variant; bounded rejection of re-capture.
• INV-V3 Empty at Close — empty_at_close_convergence.rs::closed_state_implies_zero_supply_floor + the close-gate rejects-unresolved proof; supply axes u32-symbolic.
• INV-F1 fee curve, INV-FEE-T1/T4/T5, INV-BAND-2/3/4 — capped-decay bounds, treasury-slot replace/reject-zero/reject-duplicate, and price-band lo ≤ hi / width-bound / midpoint-containment proofs, each over a bounded price grid or representative domain.
• INV-DOB-V3-1/5/9 — dob_v3_proofs.rs::dob_lane_total_involution, ::dob_structural_best_fail_closed, ::dob_structural_worst_fail_closed — the only DOB-v3 invariants with any proof; the other seven are unverified (see §6).

All harnesses named in this section were grep-confirmed present in docs/kani-inventory.yaml (except conservation_multifill_widening.rs, which is a test fixture rather than a named symbolic proof, and was confirmed present as a source file with match_limit = 3).

5. What was only TESTED#

Fifteen invariants are tested: runtime, property, or unit tests exercise them, with no machine-checked proof. Assurance here is exactly the concrete fixtures run — it does not generalize to unexercised states. Representative rows (each cites its test file(s) from the traceability matrix):

Two partially-covered (INV-V2, INV-V4): the per-instruction slice is proven/tested, but the composed all-instruction balance-sheet (V2) and the closed cross-position share aggregate (V4) are explicit release-test/proof obligations, not runtime scans. V4's aggregate reconciliation is gated on OPS-02.

Two assumption-dependent (INV-F4 Referrer earnings solvency, INV-FEE-T3 System-wide shard solvency): these are cross-account totals no single instruction can check. The hourly reconcileTreasuryShards job records drift but only logs it; the paged alert is gated on OPS-02. The stated aggregate form holds only under that off-chain reconciliation (the on-chain per-shard subset is enforced via INV-REFERRAL-T3, INV-FEE-T4/T5). This is a monitoring obligation, not a proven property — see §10.

6. What was NOT verified#

6.1 Nine invariants with zero targeted proof or test (not-yet-verified)#

INV-X4 (Emergency status fails closed), INV-X5 (Maker fill credits single-application), and seven of the ten DOB-v3 invariants: INV-DOB-V3-2, -3, -4, -6, -7, -8, -10 (lane/capacity aggregate accounting, single-lane slot reachability, lane authority, merged canonical price-time order, order-ID formula, mutation rollback byte-parity, account-version/layout). These are enforced on-chain but carry neither a Kani harness nor a targeted runtime test in the current suite. Absence of evidence is not a defect claim — it is an absence of assurance.

6.2 One invariant not practically formalizable (not-practically-formalizable)#

INV-M6 (Oracle feed-identity pinning): a Kani harness over the [u8;32] feed-equality helper would re-prove a one-liner against a copy of itself (semantically vacuous, per the H-01 finding). The security-relevant assurance — every call site passes the creation-bound expected value — is verified at the instruction level by security_wrong_feed_id.rs and the expire-market late-capture unit tests. The deleted P-LOADER-01 harness (Task 17) is the same vacuity class (see §7, item 3).

6.3 The Clock fail-to-zero path — unproved AND untested#

traits/solana_context.rs:1266-1268 implements ProcessorContext::current_timestamp as match Clock::get() { Ok(clock) => clock.unix_timestamp, Err(_) => 0 } — a silent zero on Clock failure in live (non-cfg-gated) code. Every processor consuming current_timestamp() flows through this fail-to-zero path (a second, wrapper-level Clock::get()? error-propagation pattern coexists, e.g. halt_market.rs:41, close_market.rs:609).

The fail-safe rationale — market_id = floor(0/duration) = 0 matches no PDA, and lifecycle gates (TradingNotStarted/EpochNotEnded) reject a zero clock — is the code author's design-comment assertion (solana_context.rs:1258-1265), NOT an audited or machine-checked fact (FV-ASM-011, RR-CLK-01). No adversarial test forces Clock::get() to fail, and no harness proves every current_timestamp() consumer rejects 0. If a single consumer treats 0 as a valid early/boundary time, a sysvar-failure transaction could take an unintended path. RR-CLK-01's blocks-deployment = N rating explicitly rests on the unverified author claim; it would need re-rating if any consumer accepts a zero clock.

6.4 Coverage gaps in instruction execution and formal scope#

• ~8 live instructions have zero runtime coverage (RR-COV-01): the four spline fund-movers SettleSpline/DepositSplineVault/WithdrawSplineVault/CloseSpline (0x44–0x47) and TopUpCloserRewards (0x35) — all fund-movers, deployment-blocking — plus the builderless-governance UpdateOperationalParams (0x2F), InitResolverRegistry (0x48), UpdateResolverRegistry (0x49). The former prelaunch UpdateMarketDefaults (0x32) surface is now retired; 0x32 is reserved and rejected rather than an uncovered live instruction.
• 22+ instruction discriminants have zero Kani coverage (RR-KANI-01); the "13+ invariants with zero Kani coverage" figure in traceability §honest-bounds is the invariant-level view of the same long tail. Formal proofs were scoped to the highest-value invariants (solvency, no-crossed-book, seat sizing, payout); the tail is covered by runtime/property/fuzz tests or not at all.

7. Formal-model boundaries carried as explicit assumptions#

Beyond the coverage classes, four formal-scope boundaries are load-bearing and were promoted into the assumption registry (docs/security/assumptions.md, "harness-buried" flags):

1. Resolution shares a symbolic exponent. INV-M3/INV-M5 (compute_outcome_*) are proven full-width (i64) only when the two price samples share one exponent (compute_outcome_equal_expo_full_i64, assumptions: "equal exponents only"). The unequal-exponent normalize_prices path is proven only at i32/i8 width. Resolution is not proven for mismatched exponents at production width.
2. FV-ACCT-001 seat-size whitelist (RR-FV-01). The seat-size whitelist proof's model restates the gate's own loop (same table), so it cannot catch a wrong constant inside the whitelist itself — a mis-entered byte size would pass both gate and proof. Whitelist values are also exercised by the runtime account_layout_registry tests. Strengthening (FV-ACCT-001-strengthen: an independent hardcoded oracle) is a tracked follow-up.
3. P-LOADER-01 deleted as SHA-256-intractable (RR-FV-02). The PDA-binding proof was removed because create_program_address runs SHA-256 and CBMC cannot symbolically execute it. FV-PDA-001 (INV-G2 above) proves the canonical-bump comparison only, not the derivation (the hash is out of formal reach). PDA derivation is covered by runtime PDA-validation tests instead, and PDA collision resistance is an assumption (FV-ASM-014), not a proof.
4. Oracle normalize no-panic (FV-ASM-020) is proven only for i32/i8-bounded inputs; production accepts full i64/i32 (checked arithmetic fails closed on the unproven range — a liveness/UX issue, not solvency). Order-book solvency (FV-ASM-021) bounds PlaceOrder to ≤ 3 maker crosses (the §4.1 bound).

8. Assumptions the whole edifice rests on#

The 21 assumptions in docs/security/assumptions.md are the trust and environmental preconditions under which every result above holds. The ones a deployer must weigh most heavily:

The full statement, consequence, monitoring, and eliminability of each is in the registry. Note the ~469 Assumptions: lines inside the Kani harnesses are overwhelmingly proof-scoping preconditions (each mirroring a production guard and carrying a Non-vacuity: witness), not real-world trust assumptions — only the environmental/runtime/scope-boundary handful above are promoted.

9. Mutation testing — the suite fails its own gate#

This is deployment-blocker RR-MUT-01 and must be stated plainly: the test suite does not meet its own declared mutation-sensitivity target.

The first executable mutation baseline (Task 2, docs/internal/mutation-baseline-2026-08-03.md) measured:

kill rate = caught * 10_000 / (caught + missed + timeout)
          = 1318 * 10_000 / (1318 + 531 + 0)
          = 7128 bps          (policy floor: 9000 bps → FAIL, short by 1872 bps)

2125 mutants (deduplicated), 1318 caught, 531 survivors. The honest, narrow claim: under its own declared configuration (--lib + three killer targets, not the full 636-file suite), the mutation gate fails its own floor. Some survivors are plausibly killed by integration/SBF tests the policy never invokes (annotated [ELSEWHERE] in the triage), but the declared number is below floor.

Survivors concentrate in validation guards — exactly the defensive code whose weakening is hardest to observe. 434 of 531 (82%) sit in five files (place_order.rs 212, deep-orderbook view.rs/tree.rs 123, solana_context.rs 54, matching.rs 45). The highest-value gap classes (RR-MUT-03, and the baseline's §7 priority list) include:

• referral_rollup.rs::referrer_treasury_covers_accumulated — referral-treasury solvency check removable/invertible, no executing cargo-test coverage found anywhere ([NOWHERE]);
• settle_processor.rs settle guards (validate_settle→Ok(()), is_already_settled→false) — double-settlement / solvency-bypass mutants survive the policy set;
• trader_ledger.rs::v2_find_or_allocate_slot probe arithmetic — duplicate-trader-slot allocation;
• place_order.rs::init_place_order_position_if_needed — position-PDA / owner checks inverted;
• deep-orderbook validator predicates (validate_pointer/validate_slot/validate_live_slot) — corruption-detector guards whose corruption shapes have no fixture; these are proven in formal/verification/dob_v3_proofs.rs and unreachable from legal inputs (RR-MUT-03), but unkilled by tests.

Only 27 of 531 survivors are equivalent, each with an input-domain proof; the other 504 are gap. Two harness bugs were also found: the policy's testArgs sit after -- (restricting only the test phase, leaving the build phase to compile all 636 targets — mandatory -C workaround used), and deep_orderbook/view.rs was double-enumerated (dedup is sound; it changes counts, never conclusions). The policy-schema verifier was not run — the campaign produced cargo-mutants' raw layout with no summary.json, so the FAIL is asserted from the numbers, not demonstrated by the tool. RR-MUT-01 must be green or explicitly waived before mainnet.

10. Residual risk and Workstream C findings#

The full ledger is docs/security/residual-risk.md (27 rows). The four deployment-blockers are in §2. The remaining rows are documented, low-severity, already-mitigated, or design assumptions. Notably, the six liveness properties L-1…L-6 are recorded as dependencies, not proofs — none is claimed proven, because each depends on scheduling, validator behavior, liquidity, or an off-chain actor; the degraded-mode table (spec/STATE.md §5.3) ensures every liveness failure degrades to a safe, no-fund-loss state, which is why all six are blocks deployment = N.

Workstream C findings (all documented, all currently unpatched by design). The security review found no exploitable fund-loss gap, and the double-payout class was runtime-cleared. The four open findings are:

Other tracked residuals of note: RR-DIST-01 (~49 processors lack explicit writable-account distinctness checks; no aliasing exploit demonstrated, high-value mutators do carry guards), RR-COV-02/RR-REF-01 (ClaimReferrerEarnings conservation and RollupReferralFees double-payout guard are source-verified but lack a runtime witness), RR-REC-01 (account-revival tolerance shown via simulation, not program-driven; the more dangerous inheritance half is runtime-demonstrated to be rejected on the exercised drain-to-zero paths).

11. Verification-tooling status (what is and isn't running)#

Two infrastructure facts materially affect what "the suite passes" means today:

1. The ABI discriminant-range scan (abi_range_scan) passes on this branch. The live-Reclaim 0x3C–0x3F expectations were updated in commit 93aa16b69, so this check no longer halts make verify-all at stage 1. make verify-all now builds target/deploy/seesaw.so with cargo-build-sbf immediately before the suite, preventing LiteSVM from consuming a stale artifact.
2. GitHub Actions has been disabled on this repo since February 2026. The verification.yml workflow (Task 23, confirmed present at .github/workflows/verification.yml) is ready but not running. CI-env drift is separately tracked (RR-CI-01: cargo-mutants 27.1.0 vs 24.11.1 pinned, python3 3.14.3 vs 3.12.x pinned) and will hard-fail the lean-gate on re-enable.

For completeness and to avoid overclaiming in the other direction: kani_evidence.py verify-inventory PASSES on the committed tree — the Kani source-digest manifest is not stale. (A separate, pre-existing run-kani.sh record-from-log subcommand divergence exists but does not affect the manifest's integrity.)

Also carried forward (RR-FUZZ-01, deployment-blocker #3): the lifecycle fuzz campaign fuzz_market_lifecycle_real (600 s) never ran — macOS ASan × dyld livelock before main. A 20 000-iteration deterministic sweep passed as fallback (no coverage feedback). The real coverage-guided campaign must run on Linux/CI before mainnet; both the local verify-all target and the ready workflow now codify the same 600-second obligation.

12. Required post-deployment monitoring#

The results in Sections 3–5 hold only while the assumptions in Section 8 hold. Several assumptions and residual rows are enforceable only by off-chain monitoring; these are launch-critical operational obligations, not optional dashboards. Derived from the assumption registry's monitoring column and the residual register's mitigation/next-step fields:

13. Bottom line#

Under the documented assumptions (docs/security/assumptions.md), the machine-checked properties listed in Sections 3–4 hold for the modeled implementation and the explored state space — 6 full-type value proofs (INV-G2, INV-M3, INV-M5, INV-T2, INV-T3, INV-F2), one no-panic smoke proof (INV-BAND-1), and 39 boundedly-verified invariants whose proofs are faithful but non-exhaustive envelopes (most importantly, order-book conservation is proven only to ≤ 3 maker crosses / unwind(4), with runtime tripwires and fuzz/property tests covering deeper fills). Fifteen further invariants are established by tests on their exercised fixtures; four are aggregate/off-chain-reconciled; nine are not-yet-verified and one is not-practically-formalizable (INV-M6, backed by instruction-level tests), and the Clock fail-to-zero path is neither proved nor tested.

The internal review found no exploitable fund-loss gap, and the double-payout class was runtime-cleared. But four items block deployment until closed or formally waived: the mutation suite fails its own 9000 bps floor (7128 bps); five fund-moving instructions have zero executed tests; the real lifecycle fuzz campaign never ran; and a cross-resolver substitution surface is unprobed. The ABI scan is green on this branch, while CI remains disabled.

This report does not assert that the program is free of defects or secure in any absolute sense. It asserts exactly what the cited evidence supports, and names precisely where assurance ends. A deployer should come away knowing what is established, what is bounded, what rests on operational monitoring, and what remains open.

Appendix: source documents#

• docs/security/traceability.md — 75-row INV-* → evidence matrix (coverage classes)
• docs/security/assumptions.md — 21 assumptions FV-ASM-001…021
• docs/security/residual-risk.md — 27 residual rows, 4 deployment-blockers
• docs/security/invariants.md — the invariant catalog these rows trace to
• docs/kani-inventory.yaml — proof names, property text, domains (every harness cited above was confirmed present here)
• docs/internal/mutation-baseline-2026-08-03.md — mutation baseline + survivor triage
• spec/STATE.md §5 — liveness assumptions L-1…L-6 and the degraded-mode table