Build Raft — consensus you can defend (12 scenes)
Scene 06 · The five invariants — proof and refinement
Election Safety, Leader Append-Only, Log Matching, Leader Completeness, State Machine Safety. Election restriction (sharpened to §5.4.1) plus current-term commit imply Leader Completeness, which reduces State Machine Safety to deterministic apply.
Previously
Scene 5 added the one clause that closed the Figure 8 hole: a leader counts replicas only on entries from its own current term; prior-term entries commit transitively via Log Matching. With that clause in hand, every invariant the paper names finally has the mechanism that maintains it — so we can stop listing rules and start showing why they compose.
Scene 06
The five invariants — proof and refinement
Diagram
Five Raft servers (S1..S5) in a row. Each cell shows the server's id, role badge (FOLLOWER/CANDIDATE/LEADER), currentTerm, votedFor, and a horizontal log strip whose entries are colored by the term that created them. The caption beneath the cluster names which step of the proof chain is on screen; the highlighted server (e.g. the intersection witness in Leader Completeness) and the highlighted log index (e.g. the committed entry being traced) are picked out by the topology's highlight ring.
S5 is stale — its last log entry is term 1; everyone else has term 3 →
first clause of the §5.4.1 predicate kills S5's candidacy →
The paper names five safety invariants. Each gets a plain-English line first, then the formal statement in parentheses. (1) **Election Safety** — only one leader exists at any term. (Formal: at most one server can be elected leader in any given term — §5.2.) Maintained by majority quorum + one-vote-per-server-per-term. (2) **Leader Append-Only** — a leader never edits or deletes its own log entries; it only adds new ones at the end. (Formal: a leader never overwrites or deletes entries in its log — §5.3.) (3) **Log Matching** — if two servers have an entry with the same index and term, their logs are identical up to and including that entry. (Formal: from scene 4 — same (index, term) implies identical preceding prefix.) Maintained by the AppendEntries consistency check. (4) **Leader Completeness** — every entry that has been committed survives in every future leader's log forever. (Formal: if a log entry is committed in a given term, it is present in the logs of all leaders for higher terms — §5.4.) (5) **State Machine Safety** — no two replicas ever apply different commands at the same log position. (Formal: if any server has applied a log entry at a given index to its state machine, no other server will ever apply a different log entry for the same index — §5.4.) Then we sharpen the election restriction. Scene 3 gave you the gist — a candidate with a stale log can't win. Here is the precise version Raft actually checks, the **§5.4.1 up-to-date predicate**: a voter grants its vote only if the candidate's lastLogTerm > voter's lastLogTerm, OR (lastLogTerm equal AND candidate's lastLogIndex ≥ voter's lastLogIndex). The diagram highlights step 0 of the proof chain: S5 is stale (lastTerm = 1), the others have advanced through term 3 — by the first clause of the predicate, S5 cannot win.
Implementation
Voter.isAtLeastAsUpToDate(candidateLast, voterLast) — §5.4.1
the precise election-restriction predicate
1def isAtLeastAsUpToDate(cLast, vLast):2 # cLast = (lastTerm, lastIndex) of candidate's log3 # vLast = (lastTerm, lastIndex) of voter's log4 if cLast.term != vLast.term:5 return cLast.term > vLast.term6 # equal lastTerm: longer (or equal) wins7 return cLast.index >= vLast.index
Leader.tryAdvanceCommitIndex() — §5.4.2
the current-term commit rule, in code
1def tryAdvanceCommitIndex():2 for N in range(self.commitIndex + 1, len(self.log) + 1):3 # ONLY commit entries from the leader's current term4 # by counting replicas — prior-term entries commit5 # transitively via Log Matching.6 if self.log[N - 1].term != self.currentTerm:7 continue8 replicas = 1 + sum(9 1 for p in peers if self.matchIndex[p] >= N10 )11 if replicas >= majority(self.cluster):12 self.commitIndex = N
Theorem.LeaderCompleteness — proof skeleton
majority intersection + election restriction + commit rule
1# Suppose: entry E committed in term T on majority M.2# Suppose: leader L' wins term T' > T with majority M'.3# Goal: L'.log contains E.4#5# Step 1: M ∩ M' is non-empty (any two majorities intersect).6# Pick witness s in M ∩ M'.7# Step 2: s voted for L' → by §5.4.1, L'.log is8# at-least-as-up-to-date as s.log.9# Step 3: s in M → s.log contains E.10# Step 4: by §5.4.1 + Log Matching, L'.log contains E. ∎11#12# State Machine Safety follows: deterministic in-order apply13# up to commitIndex on identical committed prefixes.