test both modes

certora/harnesses/ERC20VotesBlocknumberHarness.sol

@@ -3,7 +3,7 @@ pragma solidity ^0.8.0;
 
 import "../patched/token/ERC20/extensions/ERC20Votes.sol";
 
-contract ERC20VotesHarness is ERC20Votes {
+contract ERC20VotesBlocknumberHarness is ERC20Votes {
     constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
 
     function mint(address account, uint256 amount) external {

certora/harnesses/ERC20VotesTimestampHarness.sol

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+import "../patched/token/ERC20/extensions/ERC20Votes.sol";
+
+contract ERC20VotesTimestampHarness is ERC20Votes {
+    constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {}
+
+    function mint(address account, uint256 amount) external {
+        _mint(account, amount);
+    }
+
+    function burn(address account, uint256 amount) external {
+        _burn(account, amount);
+    }
+
+    // inspection
+    function ckptFromBlock(address account, uint32 pos) public view returns (uint32) {
+        return checkpoints(account, pos).fromBlock;
+    }
+
+    function ckptVotes(address account, uint32 pos) public view returns (uint224) {
+        return checkpoints(account, pos).votes;
+    }
+
+    function maxSupply() public view returns (uint224) {
+        return _maxSupply();
+    }
+
+    // clock
+    function clock() public view override returns (uint48) {
+        return uint48(block.timestamp);
+    }
+
+    // solhint-disable-next-line func-name-mixedcase
+    function CLOCK_MODE() public view virtual override returns (string memory) {
+        return "mode=timestamp";
+    }
+}

certora/specs.js

@@ -1,4 +1,3 @@
-/// This helper will be handy when we want to do cross product. Ex: all governor specs on all variations of the clock mode.
 const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi => [ai, bi].flat())));
 
 module.exports = [
@@ -49,15 +48,18 @@ module.exports = [
     "contract": "InitializableHarness",
     "files": ["certora/harnesses/InitializableHarness.sol"]
   },
-  ...[ "GovernorBase", "GovernorInvariants", "GovernorStates", "GovernorFunctions" ].map(spec => ({
+  ...product(
+    [ "GovernorBase", "GovernorInvariants", "GovernorStates", "GovernorFunctions" ],
+    [ "ERC20VotesBlocknumberHarness", "ERC20VotesTimestampHarness" ],
+  ).map(([ spec, token ]) => ({
     spec,
     "contract": "GovernorHarness",
     "files": [
       "certora/harnesses/GovernorHarness.sol",
-      "certora/harnesses/ERC20VotesHarness.sol"
+      `certora/harnesses/${token}.sol`
     ],
     "options": [
-      "--link GovernorHarness:token=ERC20VotesHarness",
+      `--link GovernorHarness:token=${token}`,
       "--optimistic_loop",
       "--optimistic_hashing"
     ]