diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg index ce630df2b577..61acf564d01f 100644 --- a/tla/consensus/MCccfraft.cfg +++ b/tla/consensus/MCccfraft.cfg @@ -77,6 +77,7 @@ INVARIANTS NoLeaderInTermZeroInv MatchIndexLowerBoundNextIndexInv CommitCommittableIndices + CommittableIndicesAreKnownSignaturesInv \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg index 914298be1e05..c53bf13bc2d3 100644 --- a/tla/consensus/MCccfraftWithReconfig.cfg +++ b/tla/consensus/MCccfraftWithReconfig.cfg @@ -77,6 +77,7 @@ INVARIANTS NoLeaderInTermZeroInv MatchIndexLowerBoundNextIndexInv CommitCommittableIndices + CommittableIndicesAreKnownSignaturesInv \* DebugInvLeaderCannotStepDown \* DebugInvAnyCommitted \* DebugInvAllCommitted