Add trace validation

[FedericoPonzi]

TLA+ Trace Validation for raft-rs

Validates raft-rs execution traces against the Raft safety invariants using
the TLC model checker, following the methodology from "Smart Casual
Verification of the Confidential Consortium Framework" (NSDI'25).

How it works

1. Randomized Rust tests drive 3- and 5-node clusters through elections,
   proposals, partitions, and recoveries — with both default and
   pre_vote + check_quorum configurations. After every action the full
   cluster state is captured as an ndjson line.

2. A TLA+ spec (Traceraft.tla) reads each trace and checks 12 safety
   invariants on every state snapshot. The invariants are adapted from the
   raft-rs–specific TLA+ specification (raft-tla/consensus/RaftRs.tla):

   Invariant	Source
   ElectionSafetyInv	RaftRs.tla:951
   LeaderAppendOnlyInv	RaftRs.tla:960
   LogMatchingInv	RaftRs.tla:970
   MonotonicCurrentTermInv	RaftRs.tla:998
   MonotonicCommitIdxInv	RaftRs.tla:1000
   MonotonicMatchIdxInv	RaftRs.tla:1002
   CommittedLogDurableInv	RaftRs.tla:1008
   CommitIdxLELogLenInv	RaftRs.tla:1070
   NextIdxGtZeroInv	RaftRs.tla:1043
   LeaderCommitCurrentTermInv	RaftRs.tla:1073
   PersistedAppliedOrderingInv	impl-specific
   CommittedLogReplicatedMajorityInv	RaftRs.tla:1018

3. TLC validates each trace in BFS mode with a single worker.

Running

./tla-trace-validation/run_trace_validation.sh

Prerequisites: Java 11+, Rust toolchain. TLC and CommunityModules jars are
downloaded automatically on first run.

Step-by-step:

# Generate traces
cargo test --package harness --test trace_validation

# Validate a single trace
cd tla-trace-validation
RAFT_TRACE="traces/rand3n_0.ndjson" \
  java -XX:+UseParallelGC \
  -cp "lib/tla2tools.jar:lib/CommunityModules-deps.jar" \
  tlc2.TLC -workers 1 -config Traceraft.cfg Traceraft.tla

Files

Path	Description
harness/tests/trace_validation.rs	Randomized tests that emit ndjson traces
tla-trace-validation/Traceraft.tla	TLA+ trace validator (12 invariants)
tla-trace-validation/Traceraft.cfg	TLC configuration
tla-trace-validation/run_trace_validation.sh	End-to-end runner
raft-tla/	raft-rs TLA+ specification (source)

References

• H. Howard et al., "Smart Casual Verification of the Confidential Consortium
  Framework," NSDI'25, 2025.
• pingcap/tla-plus PR #43 —
  raft-rs TLA+ specification.