diff --git a/tla/MCccfraft.cfg b/tla/MCccfraft.cfg
index 3259fdfff078..99727cc2ef30 100644
--- a/tla/MCccfraft.cfg
+++ b/tla/MCccfraft.cfg
@@ -67,6 +67,7 @@ INVARIANTS
     MonoLogInv
     LogConfigurationConsistentInv
     NoLeaderInTermZeroInv
+    MatchIndexLowerBoundNextIndexInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted
diff --git a/tla/MCccfraftWithReconfig.cfg b/tla/MCccfraftWithReconfig.cfg
index 51e923d61628..a261dc34c1b1 100644
--- a/tla/MCccfraftWithReconfig.cfg
+++ b/tla/MCccfraftWithReconfig.cfg
@@ -67,6 +67,7 @@ INVARIANTS
     MonoLogInv
     LogConfigurationConsistentInv
     NoLeaderInTermZeroInv
+    MatchIndexLowerBoundNextIndexInv
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted
diff --git a/tla/SIMccfraft.cfg b/tla/SIMccfraft.cfg
index 53cb81a2e8b3..9c41f5e85199 100644
--- a/tla/SIMccfraft.cfg
+++ b/tla/SIMccfraft.cfg
@@ -63,7 +63,9 @@ INVARIANTS
     MonoLogInv
     LogConfigurationConsistentInv
     NoLeaderInTermZeroInv
-    
+
+    MatchIndexLowerBoundNextIndexInv
+
     \* DebugInvLeaderCannotStepDown
     \* DebugInvAnyCommitted
     \* DebugInvAllCommitted
diff --git a/tla/ccfraft.tla b/tla/ccfraft.tla
index a7ba67bc7a75..71d0d5b35aea 100644
--- a/tla/ccfraft.tla
+++ b/tla/ccfraft.tla
@@ -312,6 +312,8 @@ CandidateVarsTypeInv ==
 \* The next entry to send to each follower.
 VARIABLE nextIndex
 
+\* nextIndex cannot be zero as its the index of the first log
+\* entry in the AE message (recalling that TLA+ is 1-indexed).
 NextIndexTypeInv ==
     \A i, j \in Servers : i /= j =>
         /\ nextIndex[i][j] \in Nat \ {0}
@@ -952,8 +954,7 @@ HandleAppendEntriesResponse(i, j, m) ==
           /\ nextIndex'  = [nextIndex  EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)]
        \/ /\ \lnot m.success \* not successful
           /\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
-             IN nextIndex' = [nextIndex EXCEPT ![i][j] =
-                               (IF matchIndex[i][j] = 0 THEN tm ELSE min(tm, matchIndex[i][j])) + 1 ]
+             IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(tm, matchIndex[i][j]) + 1 ]
           \* UNCHANGED matchIndex is implied by the following statement in figure 2, page 4 in the raft paper:
            \* "If AppendEntries fails because of log inconsistency: decrement nextIndex and retry"
           /\ UNCHANGED matchIndex
@@ -1233,6 +1234,10 @@ NoLeaderInTermZeroInv ==
     \A i \in Servers :
         currentTerm[i] = 0 => state[i] # Leader
 
+MatchIndexLowerBoundNextIndexInv ==
+    \A i,j \in Servers :
+        state[i] = Leader =>
+            nextIndex[i][j] > matchIndex[i][j]
 ------------------------------------------------------------------------------
 \* Properties