chore: checkpoint all prior work for clean state

Captures all uncommitted work from ha-config-bootstrap,
ha-heartbeat-liveness, and associated spec/tooling updates:

- src: ha.c, ha.h, cluster.c, config_repl.c, myapp.c, raft.c —
  heartbeat liveness, RDHUP integration, committing phase fixes
- tests: test_ha_role.c, test_config_repl.c, test_ha_rdhup_integration.c,
  test_p1_integration.c, test_p3_hardening.c, scheduler test
- specs: election-iomgr-refactor, ha-heartbeat-liveness,
  ha-peer-connection-reuse, raft-library (new); ha-config-bootstrap
  and election-iomgr-refactor task/research updates
- tooling: .wolf/ state, ha/data cluster fixtures, raft/raft.tla,
  src/build symlink, xce-build skill update

src/controller/CLAUDE.md

@@ -25,6 +25,70 @@ Links against `libxce` from `src/lib/`.
 - Component-specific headers in `include/`
 - Shared types defined in `src/include/xce/` (libxce)
 
+## HA Protocol Verification
+
+### Raft TLA+ Formal Specification
+
+The file `raft/raft.tla` contains Diego Ongaro's TLA+ specification of the Raft consensus algorithm. This is the authoritative reference for HA protocol correctness. **All HA protocol changes must be verified against this specification.**
+
+### TLA+ Variable-to-Code Mapping
+
+| TLA+ Variable | XCE Code | Location |
+|--------------|----------|----------|
+| `currentTerm[i]` | `ha->term` (_Atomic uint64_t) | `ha.h:139` |
+| `state[i]` ∈ {Follower,Candidate,Leader} | `ha->role` ∈ {INIT,ELECTING,PRIMARY_COMMITTING,PRIMARY,STANDBY} | `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` |
+| `nextIndex[i,j]` | `standby.join_applied_lsn` (replicator) | `repl.h` |
+| `matchIndex[i,j]` | `standby.acked_lsn` (replicator) | `repl.h` |
+
+### TLA+ Action-to-Code Mapping
+
+| TLA+ Action | XCE Code | Location |
+|------------|----------|----------|
+| `Timeout(i)` | `raft_start_election` via delaymgr | `raft.c:57` |
+| `RequestVote(i,j)` | `raft_on_vote_request` / reply path | `raft.c:106,169` |
+| `BecomeLeader(i)` | `raft_cb_become_leader` | `ha.c:347` |
+| `AdvanceCommitIndex(i)` | `repl_wait_majority_ack` → advance `committed_lsn` | `repl.c:338` |
+| `AppendEntries(i,j)` | `OPCode_nop` heartbeat + WAL streaming | `ha.c:2880`, `config_repl.c:1489` |
+| `ClientRequest(i,v)` | Job submit → WAL append → `repl_wait_majority_ack` | `persist.c`, `repl.c` |
+| `UpdateTerm(i,j,m)` | Term CAS in `handle_request_vote` / vote reply handler | `ha.c:1218-1230` |
+
+### Safety Invariants Verified
+
+**Election Safety** (≤1 leader per term): Enforced by `votedFor` — a server grants at most one vote per term (`raft_on_vote_request` line 145-151). A candidate needs majority votes; each server votes at most once per term.
+
+**Leader Completeness** (committed entries survive): Freshness gate in `RequestVote` — candidate must have `lastLogTerm ≥ voter` AND `lastLogIndex ≥ voter`. Since committed entries are on a majority, the new leader must have all committed entries. `persist_truncate_wal_above(safe_committed_lsn)` removes any divergent entries above the safe commit point.
+
+**State Machine Safety** (no divergent entries): Monotonic `committed_lsn` + truncation on promotion. Entries at or below `committed_lsn` are identical across all servers.
+
+**Commit Rule** (current-term entry required): Each WAL entry is committed individually via `repl_wait_majority_ack()`. Since entries are single-writer (only the current primary writes), every committed entry is implicitly from the current leader's term. Equivalent to Raft's batched commit rule.
+
+### Post-Election Safe Commit Point (Critical)
+
+After winning election, the new primary determines `safe_committed_lsn` from voter state collected during the election. This eliminates a round-trip vs waiting for the first heartbeat reply:
+
+```
+safe_committed_lsn = max(lsn : count of voters with peerLastLogLsn >= lsn) + 1 >= majority)
+```
+
+The `RequestVoteReply` message already carries `peerConfigTag` and `peerLastLogLsn` from each voter. The winning candidate uses these (from `ha_elect_ctx_t.votes[]`) to compute `safe_committed_lsn` immediately in `raft_cb_become_leader`, then calls `persist_truncate_wal_above(safe_committed_lsn)`.
+
+**Never** use `last_known_committed_lsn` from the previous primary's ctrlhello for truncation — it may be stale (the old primary may have committed entries after the last ctrlhello was sent).
+
+### Protocol Verification Checklist
+
+When modifying HA protocol code (election, replication, heartbeat), verify:
+- [ ] `votedFor` is updated atomically with term increment before granting any vote
+- [ ] `currentTerm` is monotonic — never decreases
+- [ ] `commitIndex` never decreases (monotonic)
+- [ ] A leader only commits entries from its current term (or equivalent via per-entry majority ack)
+- [ ] `safe_committed_lsn` is derived from voter replies, not from stale ctrlhello
+- [ ] WAL truncation on promotion only removes entries above the safe commit point
+- [ ] Freshness gate in RequestVote: candidate must have `lastLogTerm >= voter` AND `lastLogIndex >= voter`
+
 ## HA Design Constraints
 
 ### Inbound vs. Outbound Connection Ownership (CRITICAL)
@@ -51,10 +115,12 @@ All inter-controller communication uses iomgr (epoll-based) and vtaskmgr:
 - Blocking I/O (e.g., `fetch_config_from_primary`, `ha_find_and_connect_to_primary`) is only permitted from `delaymgr` worker threads, **never** from iomgr/vtask context.
 
 ### Heartbeat Model
-XCE uses an asymmetric heartbeat model — different from standard Raft:
-- The **standby** arms a watchdog timer (`ha_arm_heartbeat_timeout_vtask`) when it enters `CTRL_STANDBY`. If no message arrives from the primary within `heartbeat_timeout_ms`, it triggers re-election.
-- The **primary does not send periodic heartbeats** to standbys. Instead, WAL replication entries, config pushes, and ctrlhello messages serve as liveness signals.
-- `raft.c` (the election library) has no heartbeat loop — it is election-only. Do not add heartbeat callbacks to `raft_cbs_t`; that belongs in the HA layer.
+
+XCE uses a bidirectional heartbeat model aligned with Raft's AppendEntries:
+- The **primary** sends periodic heartbeats (`OPCode_nop`) to all standbys via `ha_start_primary_heartbeat` (delaymgr task, interval=3s). During `CTRL_PRIMARY_COMMITTING`, this also serves as the replication driver — the primary evaluates standby state from heartbeat replies and pushes config/WAL/snapshot as needed.
+- The **standby** replies to each heartbeat with its current `(applied_lsn, config_tag)` in `RequestReply.stateReport`. This gives the primary continuous visibility into standby convergence.
+- The **standby** also arms a liveness watchdog (`ha_arm_heartbeat_timeout_vtask`) when entering `CTRL_STANDBY`. If no message arrives from the primary within `heartbeat_timeout_ms` (10s), it triggers re-election via `ha_on_primary_ctrl_fd_rdhup`.
+- `raft.c` (the election library) is election-only. Heartbeat and replication logic belongs in the HA layer (`ha.c`, `config_repl.c`).
 
 ### Connection Ownership
 - Promoted vote connections (`ha->standby_endpoints`): owned by `vote_ep_err_handler`; freed when the standby disconnects.