diff --git a/specifications/dag-consensus/Sailfish.tla b/specifications/dag-consensus/Sailfish.tla
index d80499b6..658ac741 100644
--- a/specifications/dag-consensus/Sailfish.tla
+++ b/specifications/dag-consensus/Sailfish.tla
@@ -43,6 +43,10 @@ ASSUME GSTIsARoundNumber == GST \in Nat
 \* have to form a quorum, or else no round could ever be entered:
 ASSUME CorrectNodesFormQuorum == IsQuorum(N \ F)
 
+\* An additional vote cannot turn a quorum into a non-quorum.
+ASSUME QuorumsAreMonotone ==
+    \A Q, S \in SUBSET N : IsQuorum(Q) /\ Q \subseteq S => IsQuorum(S)
+
 \* Removing the Byzantine nodes from a quorum leaves a blocking set:
 ASSUME QuorumMinusByzantineIsBlocking ==
     \A Q \in SUBSET N : IsQuorum(Q) => IsBlocking(Q \ F)
diff --git a/specifications/dag-consensus/TLCSailfish1.tla b/specifications/dag-consensus/TLCSailfish1.tla
index 9f70d278..03784603 100644
--- a/specifications/dag-consensus/TLCSailfish1.tla
+++ b/specifications/dag-consensus/TLCSailfish1.tla
@@ -36,6 +36,7 @@ ASSUME RoundsStartAtOne
 ASSUME LeadersAreNodes
 ASSUME GSTIsARoundNumber
 ASSUME CorrectNodesFormQuorum
+ASSUME QuorumsAreMonotone
 ASSUME QuorumMinusByzantineIsBlocking
 ASSUME BlockingSetsIntersectQuorums
 
diff --git a/specifications/dag-consensus/TLCSailfish2.tla b/specifications/dag-consensus/TLCSailfish2.tla
index 2a3facdc..28e02b12 100644
--- a/specifications/dag-consensus/TLCSailfish2.tla
+++ b/specifications/dag-consensus/TLCSailfish2.tla
@@ -34,6 +34,7 @@ ASSUME RoundsStartAtOne
 ASSUME LeadersAreNodes
 ASSUME GSTIsARoundNumber
 ASSUME CorrectNodesFormQuorum
+ASSUME QuorumsAreMonotone
 ASSUME QuorumMinusByzantineIsBlocking
 ASSUME BlockingSetsIntersectQuorums