diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
index eeec32e9c..aac38a018 100644
--- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
@@ -522,6 +522,15 @@ AgreementOnValue ==
             /\ decision[p] = Decision(v, t, r1)
             /\ decision[q] = Decision(v, t, r2)
 
+\* [PBTS-INV-VALID.0]
+ConsensusValidValue ==
+    \A p \in Corr:
+        \* decision[p] = Decision(v, t, r)
+        LET dec == decision[p] IN dec /= NilDecision => IsValid(dec[1])
+
+\* [PBTS-INV-MONOTONICITY.0]
+\* TODO: we would need to compare timestamps of blocks from different height
+
 \* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
     \A p \in Corr, t \in Timestamps : 
diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
index 863ddbf19..f50b87196 100644
--- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
+++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla
@@ -789,6 +789,15 @@ DisagreementOnValue ==
     /\ decision[p] = Decision(p1, r1)
     /\ decision[q] = Decision(p2, r2) 
 
+\* [PBTS-INV-VALID.0]
+ConsensusValidValue ==
+    \A p \in Corr:
+        \* decision[p] = Decision(Proposal(v,t,pr), r)
+        LET prop == decision[p][1] IN prop /= NilProposal => IsValid(prop[1])
+
+\* [PBTS-INV-MONOTONICITY.0]
+\* TODO: we would need to compare timestamps of blocks from different height
+
 \* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
     \A p \in Corr: