diff --git a/certora/specs.js b/certora/specs.js
index 7caf78c06..ac0dce088 100644
--- a/certora/specs.js
+++ b/certora/specs.js
@@ -38,9 +38,9 @@ module.exports = [].concat(
   },
   // Security
   {
-    "spec": "Pausable",
-    "contract": "PausableHarness",
-    "files": ["certora/harnesses/PausableHarness.sol"]
+    spec: 'Pausable',
+    contract: 'PausableHarness',
+    files: ['certora/harnesses/PausableHarness.sol'],
   },
   // Proxy
   {
@@ -77,29 +77,26 @@ module.exports = [].concat(
       '--optimistic_hashing',
     ],
   })),
-  /// WIP part
-  process.env.CI
-    ? []
-    : product(
-        ['GovernorHarness'],
-        ['GovernorFunctions'],
-        ['ERC20VotesBlocknumberHarness'],
-        ['propose', 'castVote', 'queue', 'execute', 'cancel'],
-      ).map(([contract, spec, token, fn]) => ({
-        spec,
-        contract,
-        files: [
-          `certora/harnesses/${contract}.sol`,
-          `certora/harnesses/${token}.sol`,
-          `certora/harnesses/TimelockControllerHarness.sol`,
-        ],
-        options: [
-          `--link ${contract}:token=${token}`,
-          `--link ${contract}:_timelock=TimelockControllerHarness`,
-          '--optimistic_loop',
-          '--optimistic_hashing',
-          '--rules',
-          ['liveness', 'effect', 'sideeffect'].map(rule => `${fn}_${rule}`).join(' '),
-        ],
-      })),
+  product(
+    ['GovernorHarness'],
+    ['GovernorFunctions'],
+    ['ERC20VotesBlocknumberHarness'], // 'ERC20VotesTimestampHarness'
+    ['propose', 'castVote', 'queue', 'execute', 'cancel'],
+  ).map(([contract, spec, token, fn]) => ({
+    spec,
+    contract,
+    files: [
+      `certora/harnesses/${contract}.sol`,
+      `certora/harnesses/${token}.sol`,
+      `certora/harnesses/TimelockControllerHarness.sol`,
+    ],
+    options: [
+      `--link ${contract}:token=${token}`,
+      `--link ${contract}:_timelock=TimelockControllerHarness`,
+      '--optimistic_loop',
+      '--optimistic_hashing',
+      '--rules',
+      ...['liveness', 'effect', 'sideeffect'].map(kind => `${fn}_${kind}`),
+    ],
+  })),
 );
diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec
index 3f3c80736..1f03f2dac 100644
--- a/certora/specs/GovernorFunctions.spec
+++ b/certora/specs/GovernorFunctions.spec
@@ -3,7 +3,7 @@ import "Governor.helpers.spec"
 import "GovernorInvariants.spec"
 
 use invariant proposalStateConsistency
-use invariant queuedImplyVoteOver
+use invariant queuedImplyDeadlineOver
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -235,7 +235,7 @@ rule execute_sideeffect(uint256 pId, env e, uint256 otherId) {
 rule cancel_liveness(uint256 pId, env e) {
     require nonpayable(e);
     require clockSanity(e);
-    requireInvariant queuedImplyVoteOver(e, pId);
+    requireInvariant queuedImplyDeadlineOver(e, pId);
 
     uint8 stateBefore = state(e, pId);
 
diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec
index 364bf9a1d..b4257f209 100644
--- a/certora/specs/GovernorInvariants.spec
+++ b/certora/specs/GovernorInvariants.spec
@@ -36,18 +36,19 @@ invariant proposalStateConsistency(uint256 pId)
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Invariant: votes recorded => proposal snapshot is in the past                                                       │
+│ Invariant: votes recorded => created                                                                                │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-invariant votesImplySnapshotPassed(env e, uint256 pId)
+invariant votesImplyCreated(uint256 pId)
     (
         getAgainstVotes(pId) > 0 ||
         getForVotes(pId)     > 0 ||
         getAbstainVotes(pId) > 0
-    ) => proposalSnapshot(pId) < clock(e)
+    ) => proposalCreated(pId)
     {
-        preserved with (env e2) {
-            require clock(e) == clock(e2);
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
         }
     }
 
@@ -93,7 +94,25 @@ invariant queuedImplyCreated(uint pId)
         }
     }
 
-invariant queuedImplyVoteOver(env e, uint pId)
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: timmings                                                                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant votesImplySnapshotPassed(env e, uint256 pId)
+    (
+        getAgainstVotes(pId) > 0 ||
+        getForVotes(pId)     > 0 ||
+        getAbstainVotes(pId) > 0
+    ) => proposalSnapshot(pId) < clock(e)
+    {
+        preserved with (env e2) {
+            require clock(e) == clock(e2);
+        }
+    }
+
+invariant queuedImplyDeadlineOver(env e, uint pId)
     isQueued(pId) => proposalDeadline(pId) < clock(e)
     {
         preserved {