The five invariants — proof and refinement

The five safety invariants are not five things to remember — they are one proof chain: the refined election restriction (§5.4.1) plus the current-term commit rule (§5.4.2) imply Leader Completeness, and Leader Completeness plus deterministic in-order apply gives State Machine Safety.

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

Watch
Try it
Predict
Capture

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 →

What to watch for

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

Highlighted lines are the ones running in the diagram right now.

Voter.isAtLeastAsUpToDate(candidateLast, voterLast) — §5.4.1

the precise election-restriction predicate

1def isAtLeastAsUpToDate(cLast, vLast):
2    # cLast = (lastTerm, lastIndex) of candidate's log
3    # vLast = (lastTerm, lastIndex) of voter's log
4    if cLast.term != vLast.term:
5        return cLast.term > vLast.term
6    # equal lastTerm: longer (or equal) wins
7    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 term
4        # by counting replicas — prior-term entries commit
5        # transitively via Log Matching.
6        if self.log[N - 1].term != self.currentTerm:
7            continue
8        replicas = 1 + sum(
9            1 for p in peers if self.matchIndex[p] >= N
10        )
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 is
8#         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 apply
13# up to commitIndex on identical committed prefixes.

Sources

Where this sits in Build Raft — consensus you can defend

Scene 06 of 12. 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.

Up next. The safety chain you just walked holds for a cluster whose membership never changes. Scene 7 asks the next question: how do you add or remove servers without breaking the very first link — Election Safety — and why the naive 'each server swaps to the new config at its own pace' answer is wrong.

All 12 scenes in Build Raft — consensus you can defend · Every curriculum

Built with Arqly

Every scene in Build Raft — consensus you can defend builds on the one before it.All 12 Build Raft — consensus you can defend scenes