diff --git a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch
index 776a15394..05f72f8a9 100644
--- a/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch
+++ b/certora/diff/governance_extensions_GovernorPreventLateQuorum.sol.patch
@@ -1,4 +1,4 @@
---- governance/extensions/GovernorPreventLateQuorum.sol	2023-03-07 10:48:47.733488857 +0100
+--- governance/extensions/GovernorPreventLateQuorum.sol	2023-03-15 17:13:06.879632860 +0100
 +++ governance/extensions/GovernorPreventLateQuorum.sol	2023-03-15 14:14:59.121060484 +0100
 @@ -84,6 +84,11 @@
          return _voteExtension;
diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec
index 40e0ca2a4..2bcaa0839 100644
--- a/certora/specs/GovernorBaseRules.spec
+++ b/certora/specs/GovernorBaseRules.spec
@@ -141,6 +141,9 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args)
 invariant quorumRatioLessThanOne(uint256 blockNumber)
     quorumNumerator(blockNumber) <= quorumDenominator()
     filtered { f -> !skip(f) }
+    {
+        require quorumNumeratorLength() < max_uint256;
+    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec
index d66bd591b..4d9de20ef 100644
--- a/certora/specs/GovernorInvariants.spec
+++ b/certora/specs/GovernorInvariants.spec
@@ -41,9 +41,9 @@ invariant proposalStateConsistency(uint256 pId)
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 invariant votesImplySnapshotPassed(env e, uint256 pId)
-    getAgainstVotes(pId) == 0 => proposalSnapshot(pId) < clock(e) &&
-    getForVotes(pId)     == 0 => proposalSnapshot(pId) < clock(e) &&
-    getAbstainVotes(pId) == 0 => proposalSnapshot(pId) < clock(e)
+    getAgainstVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e) &&
+    getForVotes(pId)     > 0 => proposalSnapshot(pId) <= clock(e) &&
+    getAbstainVotes(pId) > 0 => proposalSnapshot(pId) <= clock(e)
     {
         preserved {
             require clockSanity(e);
diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec
index eb44ae28b..d601fc996 100644
--- a/certora/specs/GovernorStates.spec
+++ b/certora/specs/GovernorStates.spec
@@ -4,6 +4,7 @@ import "Governor.helpers.spec"
 import "GovernorInvariants.spec"
 
 use invariant proposalStateConsistency
+use invariant votesImplySnapshotPassed
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -138,6 +139,7 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
     filtered { f -> !skip(f) }
 {
     require clockSanity(e);
+    requireInvariant votesImplySnapshotPassed(e, pId);
 
     bool quorumReachedBefore = quorumReached(pId);
 
diff --git a/certora/specs/methods/IGovernor.spec b/certora/specs/methods/IGovernor.spec
index f44c2f065..6cc25599f 100644
--- a/certora/specs/methods/IGovernor.spec
+++ b/certora/specs/methods/IGovernor.spec
@@ -50,4 +50,5 @@ methods {
     getAgainstVotes(uint256)            returns uint256 envfree
     getForVotes(uint256)                returns uint256 envfree
     getAbstainVotes(uint256)            returns uint256 envfree
+    quorumNumeratorLength()             returns uint256 envfree
 }