diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 489d5ad182fe..e22e218e0f02 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -451,7 +451,7 @@ CommittedTermPrefix(i, x) ==
 AppendEntriesBatchsize(i, j) ==
     \* The Leader is modeled to send zero to one entries per AppendEntriesRequest.
      \* This can be redefined to send bigger batches of entries.
-    {sentIndex[i][j]}
+    {sentIndex[i][j] + 1}
 
 
 PlausibleSucessorNodes(i) ==