diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index b920aaba8f2b..c778561b2650 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -90,3 +90,4 @@ INVARIANTS
     \* DebugInvSuccessfulCommitAfterReconfig
     \* DebugInvAllMessagesProcessable
     \* DebugInvRetirementReachable
+    \* DebugInvUpToDepth
\ No newline at end of file
diff --git a/tla/consensus/SIMccfraft.tla b/tla/consensus/SIMccfraft.tla
index bfacc4e7fda5..916fb2bc1d5f 100644
--- a/tla/consensus/SIMccfraft.tla
+++ b/tla/consensus/SIMccfraft.tla
@@ -48,6 +48,10 @@ StopAfter ==
     (* The smoke test has a time budget of 20 minutes. *)
     IN TLCSet("exit", TLCGet("duration") > timeout)
 
+DebugInvUpToDepth ==
+    \* The following invariant causes TLC to terminate with a counterexample of length
+    \* -depth after generating the first trace.
+    TLCGet("level") < TLCGet("config").depth
 =============================================================================
 
 ------------------------------- MODULE SIMPostCondition -------------------------------