diff --git a/certora/specs.js b/certora/specs.js
index 94b443e69..aac07123c 100644
--- a/certora/specs.js
+++ b/certora/specs.js
@@ -53,7 +53,7 @@ module.exports = [].concat(
   product(
     [
       ...product(['GovernorHarness'], ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates']),
-      ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateHarness']),
+      ...product(['GovernorPreventLateHarness'], ['GovernorPreventLateQuorum']),
     ],
     ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
   ).map(([contract, spec, token]) => ({
diff --git a/certora/specs/GovernorBaseRules.spec b/certora/specs/GovernorBaseRules.spec
index 436fc273d..40e0ca2a4 100644
--- a/certora/specs/GovernorBaseRules.spec
+++ b/certora/specs/GovernorBaseRules.spec
@@ -77,11 +77,12 @@ rule againstVotesDontCountTowardsQuorum(uint256 pId, env e, method f)
     filtered { f -> voting(f) }
 {
     address voter;
-    uint8   support = 0; // Against
 
-    helperVoteWithRevert(e, f, pId, voter, support);
+    bool quorumReachedBefore = quorumReached(pId);
 
-    assert quorumReached(pId) == quorumBefore, "quorum must not be reached with an against vote";
+    helperVoteWithRevert(e, f, pId, voter, 0); // support 0 = against
+
+    assert quorumReached(pId) == quorumReachedBefore, "quorum must not be reached with an against vote";
 }
 
 /*
@@ -137,14 +138,9 @@ rule noExecuteBeforeDeadline(uint256 pId, env e, method f, calldataarg args)
 │ Invariant: The quorum numerator is always less than or equal to the quorum denominator                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant quorumRatioLessThanOne(env e, uint256 blockNumber)
-    quorumNumerator(e, blockNumber) <= quorumDenominator()
+invariant quorumRatioLessThanOne(uint256 blockNumber)
+    quorumNumerator(blockNumber) <= quorumDenominator()
     filtered { f -> !skip(f) }
-    {
-        preserved {
-            require clockSanity(e);
-        }
-    }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec
index 25cc03888..0af3be925 100644
--- a/certora/specs/GovernorPreventLateQuorum.spec
+++ b/certora/specs/GovernorPreventLateQuorum.spec
@@ -24,7 +24,7 @@ rule deadlineChangeToPreventLateQuorum(uint256 pId, env e, method f, calldataarg
     filtered { f -> !skip(f) }
 {
     requireInvariant proposalStateConsistency(pId);
-    requireInvariant votesImplySnapshotPassed(pId);
+    requireInvariant votesImplySnapshotPassed(e, pId);
 
     // This is not (easily) provable as an invariant because the prover think `_totalSupplyCheckpoints`
     // can arbitrarily change, which causes the quorum() to change. Not sure how to fix that.
diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec
index 9488163cd..eb44ae28b 100644
--- a/certora/specs/GovernorStates.spec
+++ b/certora/specs/GovernorStates.spec
@@ -139,11 +139,11 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
 {
     require clockSanity(e);
 
-    bool quorumReachedBefore = quorumReached(e, pId);
+    bool quorumReachedBefore = quorumReached(pId);
 
     f(e, args);
 
-    assert quorumReached(e, pId) != quorumReachedBefore => (
+    assert quorumReached(pId) != quorumReachedBefore => (
         !quorumReachedBefore &&
         votingAll(f)
     );