AMAGI Supplementary SCC Verification Package v3 (scc_amagi_v3): Promela Models, SPIN Logs, Trails

Verification package for the corrected Promela model scc_amagi_v3 (SPIN 6.5.2, exhaustive searches, -DCOLLAPSE). Contents: model sources (scc_amagi_v3.pml — watchdog counter inside SCC_Core, exclusive hw_emergency guard; fa1off_driver.pml — FA1-ablation driver), run script, full verification logs (15 LTL properties: SCC-S01…S09 safety PASS; SCC-S10‣S11 architectural assumptions satisfied by hardware construction; SCC-L01‣L04 verified with fairness FA1/FA2; FA2 as a theorem), FA1-ablation liveness results (expected counterexamples through the emergency path), counterexample trails, the FA1 guard-lift iteration-1 evidence log, honest results table (including the vacuous-property marking S09), README, and SHA-256 checksums. The package closes TCAD R1 Major 3 (liveness terminology) and Open Problem 1 for the Promela model; the L04 latch-up trap is closed by the FSM chain-reset correction with all 9 safety properties preserved (per NIPU v1.1 §5.1, CCR-02 of VC v1.1, TM v1.1 §6.2). License: CC BY-NC 4.0 (see LICENSE in the package).