INV-* -> Evidence Traceability Matrix#

Generated by scripts/security/build_traceability.py then hand-reviewed. The Coverage class column is hand-verified against what each cited harness/test actually proves — re-running the generator emits provisional classes (a mechanical grep heuristic) that must be re-reviewed. CI runs build_traceability.py --check, which validates only that every INV-* in docs/security/invariants.md has a row here (ID-set coverage), never cell content.

Reading the classes. proven = a Kani proof whose domain is full-type (CBMC explores every value of the input type). boundedly-verified = a Kani proof whose domain is protocol-bounded / representative / unwind- or capacity-bounded (a faithful but non-exhaustive envelope — e.g. price ∈ (0, P_MAX), an unwind(2)–unwind(4) crossing sequence, or a symbolic-tag address model). tested = runtime/property/unit tests exercise it with no machine-checked proof. partially-covered = the per-instruction slice is proven/tested but the full aggregate/composed form the invariant states is deferred (release-test/proof obligation, not a runtime scan). assumption-dependent = the stated form is a cross-account aggregate that holds only under an off-chain reconciliation currently gated on OPS-02. not-yet-verified = enforced on-chain but with no targeted proof or test evidence yet. not-practically-formalizable = a proof would be semantically vacuous or out of scope (documented rationale). The classes are deliberately not collapsed to a single percentage — a percentage destroys exactly the distinction between "proven full-type", "proven only within a bound", and "not verified".

Honest-bounds callouts (this plan's frozen A–C state). Orderbook no-cross/conservation is boundedly-verified — the crossing/fill traversal is explored under #[kani::unwind(2)] (one fill) through #[kani::unwind(4)] (two fills) plus a concrete three-fill fixture, never exhaustively; a place-order crossing ≥4 makers is outside the verified envelope. INV-M6 oracle feed-identity pinning is not-practically-formalizable — a unit proof over the [u8;32] equality helper would re-prove a one-liner against a copy of itself, so it is backed by instruction-level tests instead (H-01 rationale; the deleted P-LOADER-01 harness is the same class of vacuity). Several DOB-v3 and spline invariants remain not-yet-verified or tested-only: ~9 instructions have zero targeted runtime coverage and 13+ invariants have zero Kani coverage.

Coverage-class distribution (75 invariants)#

proven (full-type Kani domain, 5 value proofs): INV-M3, INV-M5, INV-T2, INV-T3, INV-F2. INV-BAND-1 also carries the proven label but in the narrower no-panic-over-all-u16 sense — a smoke-domain proof (absence of panics), not a value property — so the "5 full-type value proofs" figure is not overstated by the 6th row. The not-yet-verified set is INV-X4, INV-X5, and INV-DOB-V3-{2,3,4,6,7,8,10}.

Notes on specific rows#

• INV-G2 (tested, downgraded from proven on 2026-08-26). PDA verification no longer re-runs the canonical bump search on non-creation paths: verify_*_pda recomputes the address from the stored bump with create_program_address and the caller compares it against the account's actual address. account_validation.rs::canonical_bump_required_biconditional still proves the bump comparison, but that comparison now guards only the fixed-seed PDA fast path and the creation paths — it is no longer the load-bearing gate for INV-G2. The load-bearing gate is address equality, and it is runtime-tested, not proven: a full-u8 sweep in program/src/utils/pda.rs::bump_verification_tests::non_canonical_bump_never_yields_canonical_address shows every non-canonical bump either errors or yields a different address, and security_pda_validation.rs plus adversarial_account_aliasing.rs exercise the same gate through the real loaders on BPF. A Kani proof of the address-equality form would have to model SHA-256, which is not tractable — the two create_market_pda.rs harnesses that remain prove seed-layout emission only.
• INV-M6 (not-practically-formalizable). docs/security/invariants.md states a Kani harness over validate_pyth_feed_address/validate_pyth_feed_id would only re-prove a one-line [u8;32] equality 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.
• INV-V2, INV-V4 (partially-covered). The per-instruction post-CPI conservation tripwire (V2) and per-mutation supply-reconciliation deltas (V4) are proven, 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 job is still gated on OPS-02.
• INV-F4, INV-FEE-T3 (assumption-dependent). The system-wide referrer-treasury and protocol-shard sums 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, so the stated aggregate form holds only under that off-chain reconciliation. The on-chain per-shard subset is enforced (INV-REFERRAL-T3, INV-FEE-T4/T5).
• Orderbook / DOB-v3 bounds. INV-O1/O2/O3/O5 and INV-X2 are boundedly-verified: the invariant checker and placement-gate proofs are exhaustive only within the orderbook array bounds and the crossing traversal's unwind envelope; the full every-occupied-slot scan is validate_full release evidence. INV-DOB-V3-{2,3,4,6,7,8,10} have neither a Kani harness nor a targeted runtime test yet.