diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index bed562294..512230d71 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv
diff --git a/tla/consensus/MCccfraftAtomicReconfig.cfg b/tla/consensus/MCccfraftAtomicReconfig.cfg
index 41d42c891..c1193ce4d 100644
--- a/tla/consensus/MCccfraftAtomicReconfig.cfg
+++ b/tla/consensus/MCccfraftAtomicReconfig.cfg
@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
index 6d15ecbb9..c6bde4cc5 100644
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -71,7 +71,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
     TypeInv
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index bcf1faddb..381a5ab5e 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -73,7 +73,6 @@ INVARIANTS
     ElectionSafetyInv
     LogMatchingInv
     QuorumLogInv
-    MoreUpToDateCorrectInv
     LeaderCompletenessInv
     SignatureInv
 
@@ -101,4 +100,5 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
-    \* DebugInvUpToDepth
\ No newline at end of file
+    \* DebugInvUpToDepth
+    \* DebugMoreUpToDateCorrectInv
\ No newline at end of file
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 6ed49e9af..32f598df4 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -1195,7 +1195,10 @@ UpToDateCheck(i, j) ==
 
 \* If a server i might request a vote from j, receives it and counts it then i 
 \* has all of j's committed entries
-MoreUpToDateCorrectInv ==
+\* This is not an invariant, it is possible for j to vote for i despite i not
+\* having all of j's committed entries. What isn't possible is for i to win
+\* an election without having all of j's committed entries.
+DebugMoreUpToDateCorrectInv ==
     \A i \in { s \in Servers : leadershipState[s] = Candidate } :
         \A j \in GetServerSet(i) :
             /\ i /= j