CQ-SAT/GCC v0.23.0

Certified causal counterexample analysis

CQ-SAT/GCC v0.23.0 adds a bounded, evidence-producing way to explain input-driven AIGER failures.

• segments the earliest counterexample into maximal constant primary-input waveform events
• computes a replay-checked 1-minimal set that forces the named bad output at the original counterexample frame
• compares the same intervention sequence across fresh CDCL, persistent CDCL, and continuation quotients when statically admitted
• aborts publication on any solver disagreement and uses exact CDCL when CQ is rejected
• publishes a durable, atomic, no-clobber v1 evidence directory with SHA-256-bound certificate, metrics, and manifest
• provides a strict verifier that rederives the earliest counterexample and re-solves sufficiency and every single-event minimality obligation
• includes checked-in verified SPI and infusion-pump evidence bundles, adversarial tests, CI coverage, schema documentation, and a self-contained runner

On the infusion-pump example, four candidate segments reduce to a verified two-segment cause. CQ is 1.30x faster per intervention query in the recorded run, but only 0.031x after compilation; this release therefore does not claim an amortised speed improvement. The SPI example exercises the exact CDCL fallback.

This release combines established counterexample-minimisation, minimal-UNSAT, incremental-SAT, and causal-explanation ideas with continuation-quotient reuse and a strict evidence contract. It is a potentially novel synthesis, not a claim of proven scholarly novelty, a general SAT breakthrough, physical-world causation, or production certification. CQ-SAT/GCC remains an evaluation-ready research prototype pending external design-partner and security assessment.

Validation: 72 Rust tests passed on macOS and Rust 1.97 Linux/arm64; GitHub test, public RTL corpus, and dependency-audit jobs passed; RustSec reported no vulnerable dependencies; both checked-in bundles replay-verified.