myxce/.kiro/specs/ha-repl-hardening/raft-tla-audit.md

Raft TLA+ Specification Audit

Comparing XCE HA implementation against the formal Raft TLA+ specification (ongardie/raft.tla).

State Variable Mapping

TLA+ Variable	XCE Implementation	Location	Status
currentTerm[i]	ha->term (_Atomic uint64_t)	ha.h:139	✅
votedFor[i]	ha->voted_for_name[XCE_MAXNAME_LEN]	ha.h:161	✅
log[i]	WAL segments in persist->wal_path	persist.c	✅
commitIndex[i]	persist->committed_lsn (_Atomic uint64_t)	persist.h	✅
lastApplied[i]	ha->applied_lsn (_Atomic uint64_t)	ha.h:141	✅
state[i] ∈ {Follower,Candidate,Leader}	ha->role ∈ {INIT,ELECTING,COMMITTING,PRIMARY,STANDBY}	ha.h:139	✅
leaderId[i]	ha->primary_host / primary_port	ha.h:142-143	✅
nextIndex[i, j]	standby.join_applied_lsn (where to start sending)	repl.h	⚠️ Implicit
matchIndex[i, j]	standby.acked_lsn (highest replicated)	repl.h	⚠️ Implicit

Gap: nextIndex/matchIndex are implicit in the replicator, not exposed as first-class per-standby state. The heartbeat-driven design (standby_reported_lsn) makes matchIndex explicit and visible to the convergence check.

Action Mapping

TLA+ Action	XCE Implementation	Location	Status
RequestVote(i, j)	raft_on_vote_request()	raft.c:106	✅
RequestVoteReply(i, j)	raft_on_vote_reply()	raft.c:169	✅
AppendEntries(i, j)	OPCode_nop heartbeat + WAL streaming	ha.c, config_repl.c	⚠️ No follower state in reply
AppendEntriesReply(i, j)	Heartbeat reply (currently empty nodata)	cluster.c:225	⚠️ Missing success + matchIndex
BecomeLeader(i)	raft_cb_become_leader()	ha.c:347	✅
AdvanceCommitIndex(i)	committed_lsn advancement after repl_wait_majority_ack	repl.c:408	✅
ClientRequest(i, v)	Job submit → WAL append → repl_wait_majority_ack	persist.c, repl.c	✅
Timeout(i)	raft_cb_schedule_timeout via delaymgr	ha.c	✅

Key gap: AppendEntries in Raft is bidirectional — leader sends (term, prevLogIndex, prevLogTerm, entries[], leaderCommit), follower replies (term, success, matchIndex). Our heartbeat (OPCode_nop) is unidirectional. This spec fixes exactly this gap by adding stateReport to the heartbeat reply.

Safety Property Audit

Election Safety (at most one leader per term)

TLA+: ∀ i,j ∈ servers : state[i] = Leader ∧ state[j] = Leader ⇒ currentTerm[i] ≠ currentTerm[j]

XCE: ✅ Enforced through votedFor — a server grants at most one vote per term (raft_on_vote_request line 145-151). To become leader, a candidate must receive votes from a majority, and each server votes at most once per term. Therefore at most one leader per term.

Log Matching (logs identical up to matching index+term)

TLA+: ∀ i,j, index : log[i][index].term = log[j][index].term ⇒ ∀ k ≤ index : log[i][k] = log[j][k]

XCE: ✅ Enforced through election freshness gate. A candidate must have config_tag ≥ voter's config_tag and applied_lsn ≥ voter's applied_lsn to receive a vote. This guarantees the winner has the most complete log. persist_truncate_wal_above(committed_lsn) on promotion removes any divergent uncommitted entries.

Leader Completeness (committed entries survive leader changes)

TLA+: ∀ i, index, term : committed(log[i][index], term) ⇒ ∀ j, futureTerm : leader(j, futureTerm) ⇒ log[j][index].term = term

XCE: ✅ A newly elected leader truncates WAL entries above last_known_committed_lsn (from CtrlHelloReply). The freshness gate ensures the winner has at least the committed entries of any voter. Since the winner needs a majority, and any committed entry was on a majority, the winner must have all committed entries.

State Machine Safety (same index → same entry)

TLA+: ∀ i, j, index : applied(log[i][index]) ∧ applied(log[j][index]) ⇒ log[i][index] = log[j][index]

XCE: ✅ committed_lsn advances monotonically and WAL entries are applied in order. The truncation on leader change removes divergent entries above committed_lsn, and the freshness gate ensures the new leader has all entries at or below committed_lsn.

Commit Rule (current-term entry required)

TLA+: A leader can commit log[i][index] when:

• index > commitIndex[i]
• log[i][index].term = currentTerm[i]
• A majority of servers have matchIndex[j] ≥ index

XCE: ✅ Equivalent achieved through per-entry majority ack. Each WAL entry is committed individually via repl_wait_majority_ack() — the commit only succeeds after a majority have durably written the entry AND replied with an ACK. Since entries are written by the current leader (single-writer), every committed entry is implicitly from the current leader's term. The "entry from current term" requirement is satisfied because persist_truncate_wal_above removes any uncommitted entries from previous terms before the new leader writes its own.

Findings Summary

Correctly Implemented

1. Term management and monotonicity ✅
2. One-vote-per-term enforcement ✅
3. Election freshness gate (equivalent to Raft's log completeness check) ✅
4. Committed entry durability through majority ack ✅
5. WAL truncation on leader change ✅
6. Leader completeness through election gate ✅

Gaps Being Addressed by This Spec

7. AppendEntries bidirectional state: Missing follower state in heartbeat reply → fixed by stateReport in this spec
8. matchIndex visibility: Implicit in replicator → made explicit via standby_reported_lsn[N] in this spec

Not Applicable (Intentional Differences)

9. nextIndex decrement on inconsistency: Not needed — we truncate uncommitted entries on leader change, so there are no divergent entries for the consistency check to catch
10. No-op commit of current-term entry: Not needed — we use per-entry synchronous majority ack instead of batched commit

Recommendation

No safety gaps found. The two items this spec addresses (heartbeat state reporting, matchIndex visibility) close the remaining protocol gaps vs the formal Raft specification. The per-entry majority ack model is functionally equivalent to Raft's batched commit rule for our append-only single-writer WAL.