Qian-Cheng-nju · Oct 10, 2026 · Oct 10, 2026
diff --git a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftDefs.tla
@@ -4,8 +4,6 @@ EXTENDS etcd_raftModel
 
 MaxOrZero(s) == IF s = {} THEN 0 ELSE Max(s)
 
-CurrentLeaders == {i \in Server : state[i] = Leader}
-
 Committed(i) == SubSeq(log[i],1,commitIndex[i])
 
 LogInv ==
@@ -46,17 +44,9 @@ MoreUpToDateCorrectInv ==
            /\ Len(log[i]) >= Len(log[j])) =>
        IsPrefix(Committed(j), log[i])
 
-LeaderCompletenessInv == 
-    \A i \in Server :
-        LET committed == Committed(i) IN
-        \A idx \in 1..Len(committed) :
-            LET entry == log[i][idx] IN 
-
-            \A l \in CurrentLeaders :
-
-                currentTerm[l] > entry.term =>
-
-                log[l][idx] = entry
+LeaderCompletenessInv ==
+    \A c \in commitHistory, e \in electionHistory :
+        c.term < e.term => IsPrefix(c.entries, e.entries)
 
 CommittedIsDurableInv ==
     \A i \in Server :

diff --git a/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla b/benchmark/proof-from-scratch-module/etcd_raft/etcd_raftModel.tla
@@ -84,7 +84,7 @@ configVars == <<config, reconfigCount>>
 VARIABLE 
     durableState
 
-vars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
+protocolVars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
 
 Quorum(c) == {i \in SUBSET(c) : Cardinality(i) * 2 > Cardinality(c)}
 
@@ -164,7 +164,7 @@ InitDurableState ==
         config |-> config[i]
     ]]
 
-Init == /\ InitMessageVars
+ProtocolInit == /\ InitMessageVars
         /\ InitServerVars
         /\ InitCandidateVars
         /\ InitLeaderVars
@@ -508,10 +508,27 @@ NextUnreliable ==
         /\ messages[m] = 1
         /\ DropMessage(m)
 
-Next == \/ NextAsync
+ProtocolNext == \/ NextAsync
         \/ NextCrash
         \/ NextUnreliable
 
+VARIABLE commitHistory, electionHistory
+historyVars == <<commitHistory, electionHistory>>
+vars == <<protocolVars, historyVars>>
+
+Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {}
+
+RecordEvents ==
+    /\ commitHistory' = commitHistory \cup
+         {[server |-> s, term |-> currentTerm'[s],
+           entries |-> SubSeq(log'[s], 1, commitIndex'[s])] :
+            s \in {i \in Server : commitIndex'[i] > commitIndex[i]}}
+    /\ electionHistory' = electionHistory \cup
+         {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] :
+            s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}}
+
+Next == ProtocolNext /\ RecordEvents
+
 Spec == Init /\ [][Next]_vars
 
 ASSUME InitServerSubset == InitServer \subseteq Server

diff --git a/benchmark/proof-from-scratch-module/manifest.json b/benchmark/proof-from-scratch-module/manifest.json
@@ -997,7 +997,7 @@
       "spec": {
         "format_version": 1,
         "task_id": "etcd_raft/etcd_raft.tla",
-        "source_sha256": "5a8441bde8cd7051dad1c59be8b9ec7870a26ce99d28002ff3ccf83387fd35db",
+        "source_sha256": "e6aa5a22b17d9556f7cb97a659cdae152d2b9b038d56739068697d8cd3aa3d3f",
         "proof_units": [
           {
             "task_id": "etcd_raft/etcd_raft_LogInv.tla",

diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raftModel.tla
@@ -84,7 +84,7 @@ configVars == <<config, reconfigCount>>
 VARIABLE 
     durableState
 
-vars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
+protocolVars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
 
 Quorum(c) == {i \in SUBSET(c) : Cardinality(i) * 2 > Cardinality(c)}
 
@@ -164,7 +164,7 @@ InitDurableState ==
         config |-> config[i]
     ]]
 
-Init == /\ InitMessageVars
+ProtocolInit == /\ InitMessageVars
         /\ InitServerVars
         /\ InitCandidateVars
         /\ InitLeaderVars
@@ -508,10 +508,27 @@ NextUnreliable ==
         /\ messages[m] = 1
         /\ DropMessage(m)
 
-Next == \/ NextAsync
+ProtocolNext == \/ NextAsync
         \/ NextCrash
         \/ NextUnreliable
 
+VARIABLE commitHistory, electionHistory
+historyVars == <<commitHistory, electionHistory>>
+vars == <<protocolVars, historyVars>>
+
+Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {}
+
+RecordEvents ==
+    /\ commitHistory' = commitHistory \cup
+         {[server |-> s, term |-> currentTerm'[s],
+           entries |-> SubSeq(log'[s], 1, commitIndex'[s])] :
+            s \in {i \in Server : commitIndex'[i] > commitIndex[i]}}
+    /\ electionHistory' = electionHistory \cup
+         {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] :
+            s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}}
+
+Next == ProtocolNext /\ RecordEvents
+
 Spec == Init /\ [][Next]_vars
 
 ASSUME InitServerSubset == InitServer \subseteq Server

diff --git a/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla b/benchmark/proof-from-scratch/etcd_raft/etcd_raft_LeaderCompletenessDefs.tla
@@ -2,21 +2,9 @@
 
 EXTENDS etcd_raftModel
 
-CurrentLeaders == {i \in Server : state[i] = Leader}
-
-Committed(i) == SubSeq(log[i],1,commitIndex[i])
-
-LeaderCompletenessInv == 
-    \A i \in Server :
-        LET committed == Committed(i) IN
-        \A idx \in 1..Len(committed) :
-            LET entry == log[i][idx] IN 
-
-            \A l \in CurrentLeaders :
-
-                currentTerm[l] > entry.term =>
-
-                log[l][idx] = entry
+LeaderCompletenessInv ==
+    \A c \in commitHistory, e \in electionHistory :
+        c.term < e.term => IsPrefix(c.entries, e.entries)
 
 ===============================================================================
 
diff --git a/source/etcd_raft/README.md b/source/etcd_raft/README.md
@@ -1,6 +1,6 @@
 # etcd Raft benchmark model
 
-The model is derived from the etcd Raft example distributed with Specula. Its eight selected safety theorem statements are preserved.
+The model is derived from the etcd Raft example distributed with Specula. Its eight selected safety theorem statements and task IDs are preserved; the definition of `LeaderCompletenessInv` is corrected below.
 
 The local constant-domain and pending-message repairs remain in place. The crash-recovery repair stores `logEntries` alongside the existing numeric `durableState[i].log` field in `InitDurableState` and `PersistState`. `Restart` restores the saved entries directly.
 
@@ -9,3 +9,30 @@ Previously, recovery took a prefix of the current volatile log using the last pe
 Implementation reference: `etcd-io/raft` at `3cbf6a74be3fa392edd8b64253fcd11c3ce5649b`. `raftLog.storage` and `raftLog.unstable` hold stable and volatile entries separately; `newLogWithSize` reconstructs the log from storage, while `append` updates the unstable portion. See [log.go](https://github.com/etcd-io/raft/blob/3cbf6a74be3fa392edd8b64253fcd11c3ce5649b/log.go) and the [persistence contract](https://github.com/etcd-io/raft/blob/3cbf6a74be3fa392edd8b64253fcd11c3ce5649b/README.md).
 
 `tests/fixtures/etcd_raft/DurableLogRecovery.tla` follows real model actions through an election, persistence, a conflicting newer-term append, and a restart. Three cases check recovery after truncation, after an unpersisted same-length replacement, and after persisting the replacement. Each trace also checks all eight benchmark safety predicates and its transition relation against the original `Next` relation. These regression traces validate the repair; they are not proofs of all eight unbounded theorems.
+
+## Leader completeness
+
+An entry created in term 1 can remain uncommitted until term 3. A disconnected
+term-2 leader need not contain that entry. The previous predicate compared each
+current leader's term with the entry's creation term and incorrectly rejected
+this legal execution. Raft's [Leader Completeness property](https://raft.github.io/raft.pdf)
+(Figure 3 and sections 5.4.2-5.4.3) instead concerns entries committed in an
+earlier term.
+
+`commitHistory` records the current term and full log prefix whenever a server's
+commit index advances, including when a follower learns a committed prefix.
+`electionHistory` records each leader's term and log at election time. The
+corrected predicate requires every later-term election to contain each earlier
+committed prefix. Both histories survive restart. They are passive observers:
+`ProtocolInit`, `ProtocolNext` and the protocol actions preserve the previous
+state-machine behavior and assumptions; `Init` and `Next` add history updates.
+`NextAsyncCrash` and `NextDynamic` also update the observers.
+
+`tests/fixtures/etcd_raft/LeaderCompleteness.tla` replays the late commit, elects
+a term-4 leader, and restarts servers. The creation-term predicate fails on the
+same execution; the corrected predicate holds, with its later-election condition
+actually exercised. A fault control removes vote log-freshness checking and is
+rejected when an incomplete log wins the later election. These finite
+regressions do not constitute an unbounded proof. Frozen experiments using the
+old context retain their original results and must be distinguished from runs
+against the corrected model.
diff --git a/source/etcd_raft/etcd_raft.tla b/source/etcd_raft/etcd_raft.tla
@@ -143,8 +143,8 @@ VARIABLE
 \* End of per server variables.
 ----
 
-\* All variables; used for stuttering (asserting state hasn't changed).
-vars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
+\* Protocol variables, before adding passive history observers below.
+protocolVars == <<messageVars, serverVars, candidateVars, leaderVars, logVars, configVars, durableState>>
 
 
 ----
@@ -263,7 +263,7 @@ InitDurableState ==
         config |-> config[i]
     ]]
 
-Init == /\ InitMessageVars
+ProtocolInit == /\ InitMessageVars
         /\ InitServerVars
         /\ InitCandidateVars
         /\ InitLeaderVars
@@ -722,7 +722,7 @@ NextAsync ==
 
 NextCrash == \E i \in Server : Restart(i)
 
-NextAsyncCrash ==
+ProtocolNextAsyncCrash ==
     \/ NextAsync
     \/ NextCrash
 
@@ -737,20 +737,40 @@ NextUnreliable ==
         /\ DropMessage(m)
 
 \* Most pessimistic network model
-Next == \/ NextAsync
+ProtocolNext == \/ NextAsync
         \/ NextCrash
         \/ NextUnreliable
 
 \* Membership changes
-NextDynamic ==
-    \/ Next
+ProtocolNextDynamic ==
+    \/ ProtocolNext
     \/ \E i, j \in Server : AddNewServer(i, j)
     \/ \E i, j \in Server : AddLearner(i, j)
     \/ \E i, j \in Server : DeleteServer(i, j)
     \/ \E i \in Server : ApplySimpleConfChange(i)
 
-\* The specification must start with the initial state and transition according
-\* to Next.
+\* Observers retain commit and election events across crashes. Protocol actions
+\* never read these variables or use them as guards.
+VARIABLE commitHistory, electionHistory
+historyVars == <<commitHistory, electionHistory>>
+vars == <<protocolVars, historyVars>>
+
+Init == ProtocolInit /\ commitHistory = {} /\ electionHistory = {}
+
+RecordEvents ==
+    /\ commitHistory' = commitHistory \cup
+         {[server |-> s, term |-> currentTerm'[s],
+           entries |-> SubSeq(log'[s], 1, commitIndex'[s])] :
+            s \in {i \in Server : commitIndex'[i] > commitIndex[i]}}
+    /\ electionHistory' = electionHistory \cup
+         {[server |-> s, term |-> currentTerm'[s], entries |-> log'[s]] :
+            s \in {i \in Server : state[i] # Leader /\ state'[i] = Leader}}
+
+Next == ProtocolNext /\ RecordEvents
+NextAsyncCrash == ProtocolNextAsyncCrash /\ RecordEvents
+NextDynamic == ProtocolNextDynamic /\ RecordEvents
+
+\* The specification includes the observers without restricting protocol steps.
 Spec == Init /\ [][Next]_vars
 
 (***************************************************************************)
@@ -862,21 +882,13 @@ MoreUpToDateCorrectInv ==
            /\ Len(log[i]) >= Len(log[j])) =>
        IsPrefix(Committed(j), log[i])
 
-\* If a log entry is committed in a given term, then that
-\* entry will be present in the logs of the leaders
-\* for all higher-numbered terms
-\* See: https://github.com/uwplse/verdi-raft/blob/master/raft/LeaderCompletenessInterface.v
-LeaderCompletenessInv == 
-    \A i \in Server :
-        LET committed == Committed(i) IN
-        \A idx \in 1..Len(committed) :
-            LET entry == log[i][idx] IN 
-            \* if the entry is committed 
-            \A l \in CurrentLeaders :
-                \* all leaders with higher-number terms
-                currentTerm[l] > entry.term =>
-                \* have the entry at the same log position
-                log[l][idx] = entry
+\* A commit observation uses the server's term when its commit index advances,
+\* including when a follower learns a committed prefix. Entry creation terms
+\* can precede commitment; only later-term elections must contain that prefix.
+\* See Raft Figure 3 and sections 5.4.2-5.4.3: https://raft.github.io/raft.pdf
+LeaderCompletenessInv ==
+    \A c \in commitHistory, e \in electionHistory :
+        c.term < e.term => IsPrefix(c.entries, e.entries)
 
 \* Any entry committed by leader shall be persisted already
 CommittedIsDurableInv ==