security/releases/2026-06-pq-threshold-stack/CHECKLIST.md

Go / no-go checklist — release 2026-06-pq-threshold-stack

The honest gate. [x] met · [~] in progress · [ ] open. Tests are ONE evidence layer; a [x] here means the chain (math → protocol → impl → artifact → review) holds for that line, not just that a test passed.

• prove-release.sh PASS at pinned commits (gate-results.json verdict PASS)
• gate-results.json committed
• CLAIMS.md maps every claim (35 IDs) to an evidence class
• AXIOM-INVENTORY has no hidden theorem-critical axiom (final cryptographer pass: every C-axiom disclosed; "Discharged in the Wrapper" lie fixed)
• all C assumptions listed in ASSUMPTIONS.md + per-repo BLOCKERS.md
• no repo claims "fully proven" while depending on an open C assumption (gate circular-proof + claims-vs-reality enforce it)
• every EasyCrypt theory machine-checks (easycrypt compile, gate ec-machine-check.sh): pulsar 14/14, corona 14/14 — a non-compiling .ec is never counted green. Fixed under this pass: corona R_q_xi/w_low_t/wrapper intro-counts/RLWE_Functional comment, deleted pulsar V04_Sign_Ctx.ec orphan. Corona wrapper_combine_refines_abs compiles conditional on the disclosed OPEN combine_abs_op_lifted_eq_rlwe (C11) — NOT fully proven.
• unproven-assertion budget is comment-aware (strips (* *)/--//- -/): real admit/abort/sorry tactics counted, prose warned only — magnetar's false ADMIT=4 → 0, pulsar's false AXIOM=89 → 75
• [~] all public verifiers reject malformed bytes without panic (p3q F1/F2 fixed; final red pass confirming across the stack)
• all red PoCs fail closed (consensus TestRedteam_* PASS)
• independent-verifier interop passes (cryptographer EXECUTED CIRCL + pq-crystals on Pulsar — both green)
• [~] transcript-leak reports clean (final red pass producing redteam/transcript-leak-report.md)
• consensus payload roots recomputed internally (QUASAR-C4)
• signer bitmap / cert / signature binding tested (QUASAR-C5, PULSAR-C7)
• P3Q malformed-proof corpus rejects (f1_..f4_)
• [~] Magnetar leaf-reuse / rollback / concurrency: N/A for production (independent sigs, no shared one-time key); THBS-SE research-only DOES reconstruct — disclosed
• Pulsar no-residual-leak tests pass (forbidden-field guard + debug-oracle residual)
• Corona sid / nonce-reuse tests pass (256-bit hedge)
• external review signs claim IDs (EXTERNAL-REVIEW-SIGNOFF.md — the genuine final gate; not self-satisfiable)
• release manifest signed (SIGNATURES.md)
• annotated tags match the manifest (set at merge)

Verdict: review-ready high-assurance release candidate. The remaining open items are external review + signing + tagging — everything self-derivable is green. No "production-certified" / "fully-proven" language until the external sign-off lands and the open C-assumptions are signed-as-accepted or discharged.