feat(formal): add checked Go-trace-to-TLC action replay

A snapshot-only abstraction projects captured RawNode scenarios onto
twelve EPaxosRawNodeRefinement variables; EPaxosTraceCheck replays
every consecutive pair against the model's own action predicates,
dispatched by the audited raw (action,kind) pair, with stutter requiring
exact equality over all twelve mapped variables. Five negative controls
(label swap, paper-value, stutter-value, recovery-evidence, and
choose-execute midpoint corruption) each fail TLC. PaperChooseAndExecute
is the TLC-evaluated relational composition of PaperChoose and
PaperExecute for the atomic commit+execute step Go performs; PaperNext
and RefinementProperty are unchanged. The dispatch inventory extends to
internal mutation sites with an AST-checked 96-pair permission table
mirrored between Go and TLA. tests/trace_refinement_check.sh joins
tests/ci.sh after the fast gate.

Author: metaphorics

.gitignore

@@ -26,6 +26,7 @@ AGENTS.md
 
 # Generated validation artifacts
 states/
+tla/traces/
 jepsen/target/
 jepsen/.lein-failures
 jepsen/store/

tests/ci.sh

@@ -7,6 +7,7 @@ cd "$ROOT"
 bash tests/toolchain_audit.sh
 bash tests/go_coverage.sh
 bash tests/tla_model_check_fast.sh
+bash tests/trace_refinement_check.sh
 bash tests/fuzz_stress_campaign.sh
 bash tests/chaos_fault_campaign.sh
 bash tests/jepsen_remote_preflight_audit.sh