[Spec Bug] TLA+ Raft model permits split-brain during joint/membership changes due to missing log guard

[CharlieQiu2017]

Hello, while I was auditing this Raft implementation I noticed a safety bug in the current TLA+ specification of Raft, specifically in the member change logic. This issue does not affect the actual Go code, which already contains necessary guards to prevent it. The issue is due to the TLA+ model not accurately representing the current implementation.

In more detail: recall that the current member config change is implemented as follows:

1. Unlike the standard Raft algorithm, in the etcd implementation a reconfig entry does not take effect until it is committed.
   In the TLA+ model this occurs in two steps.
   First the follower receives a heartbeat message and updates its commitIndex (see AppendEntriesAlreadyDone() and CommitTo()).
   Then the follower executes ApplySimpleConfChange() to update the config.
2. When any follower times out and initiates a leader campaign, the config it uses to count votes is the latest config it has applied,
   which is in general not the same as the latest config it its local log. In fact, the latest applied config could lag behind the latest
   config entry by several versions.
3. In the actual etcd implementation, when a follower initiates a leader campaign, it needs to check whether there exists committed but
   unapplied reconfig entries in its local log. See hup() which calls hasUnappliedConfChanges() in raft.go.
   If so, the campaign is abandoned. Since the leader enforces that there can be at most one uncommitted reconfig entry,
   this effectively means the config used by the follower can lag behind the latest config by at most one version.
   However, this check seems to be not reflected in the TLA+ model. Notice that neither Timeout() nor RequestVote() has any checks over reconfig entries in the local log.

This leads the following possible sequence of events in the TLA+ model:

1. Initially, the system consists of s1, s2, s3, and leader is s1.
2. The leader proposes a reconfig entry so the system now consists of s1, s2, s3, s4, and the reconfig is committed but not applied.
3. The leader proposes a second reconfig entry so the system now consists of s1, s2, s3, s4, s5, and this second reconfig is also committed but not applied.
4. s2 now applies the second reconfig entry. However s3 applies neither of the reconfig entries.
5. Both s2 and s3 now initiate a leader campaign using the latest log (which contains both reconfig entries).
   Remember that the config of s2 is {s1, s2, s3, s4, s5}, and the config of s3 is {s1, s2, s3}.
   Now s2 collects votes from {s2, s4, s5}, but meanwhile s3 collects votes from {s1, s3}. Both nodes now have a quorum of votes under their respective active configs.
6. We now have two leaders in the same term, which is a split-brain.

I asked GPT-5.4 to generate a driver spec that replicates the above event sequence, and the result does confirm that it is possible to violate MoreThanOneLeaderInv under the current spec. See the BugDriver.tla and BugDriver.cfg files in the attached BugDriver.zip. To run the counterexample:

java -cp "$absolute_path_to_tla2tools.jar:$absolute_path_to_CommunityModules-deps.jar" tlc2.TLC -config BugDriver.cfg BugDriver.tla

You will see TLC reporting that MoreThanOneLeaderInv is violated.

This perhaps reflects two issues with the current TLA+ verification methodology:

1. The spec is not fully correct, and because the counterexample is somewhat lengthy and tricky, the state space search of TLC missed it;
2. Because the implementation is actually more restrictive than the formal model, the trace validation method missed it also, since any valid trace of the impl is also a valid trace of the model.

BugDriver.zip