diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
index 6e9067725..a29a34a9a 100644
--- a/certora/applyHarness.patch
+++ b/certora/applyHarness.patch
@@ -1,6 +1,12 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1969-12-31 16:00:00.000000000 -0800
++++ .gitignore	2022-05-27 01:31:23.000000000 -0700
+@@ -0,0 +1,2 @@
++*
++!.gitignore
 diff -ruN access/AccessControl.sol access/AccessControl.sol
---- access/AccessControl.sol	2022-05-25 15:36:58.849363940 -0400
-+++ access/AccessControl.sol	2022-05-25 16:07:31.897814961 -0400
+--- access/AccessControl.sol	2022-05-25 09:38:35.000000000 -0700
++++ access/AccessControl.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -93,7 +93,7 @@
       *
       * _Available since v4.6._
@@ -10,29 +16,9 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol
          _checkRole(role, _msgSender());
      }
  
-diff -ruN .gitignore .gitignore
---- .gitignore	1969-12-31 19:00:00.000000000 -0500
-+++ .gitignore	2022-05-25 16:07:31.901816357 -0400
-@@ -0,0 +1,2 @@
-+*
-+!.gitignore
-diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
---- governance/extensions/GovernorPreventLateQuorum.sol	2022-05-25 15:36:58.849363940 -0400
-+++ governance/extensions/GovernorPreventLateQuorum.sol	2022-05-25 16:07:31.901816357 -0400
-@@ -21,8 +21,8 @@
-     using SafeCast for uint256;
-     using Timers for Timers.BlockNumber;
- 
--    uint64 private _voteExtension;
--    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
-+    uint64 internal _voteExtension;
-+    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;
- 
-     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
-     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/Governor.sol governance/Governor.sol
---- governance/Governor.sol	2022-05-25 15:36:58.849363940 -0400
-+++ governance/Governor.sol	2022-05-25 16:07:31.901816357 -0400
+--- governance/Governor.sol	2022-05-25 09:38:35.000000000 -0700
++++ governance/Governor.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -44,7 +44,7 @@
  
      string private _name;
@@ -43,8 +29,8 @@ diff -ruN governance/Governor.sol governance/Governor.sol
      // This queue keeps track of the governor operating on itself. Calls to functions protected by the
      // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute},
 diff -ruN governance/TimelockController.sol governance/TimelockController.sol
---- governance/TimelockController.sol	2022-05-25 15:36:58.849363940 -0400
-+++ governance/TimelockController.sol	2022-05-25 16:07:31.901816357 -0400
+--- governance/TimelockController.sol	2022-05-25 09:38:35.000000000 -0700
++++ governance/TimelockController.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -28,10 +28,10 @@
      bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE");
      bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE");
@@ -58,9 +44,35 @@ diff -ruN governance/TimelockController.sol governance/TimelockController.sol
  
      /**
       * @dev Emitted when a call is scheduled as part of operation `id`.
+diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol
+--- governance/extensions/GovernorCountingSimple.sol	2022-05-25 09:38:35.000000000 -0700
++++ governance/extensions/GovernorCountingSimple.sol	2022-05-27 03:15:40.000000000 -0700
+@@ -27,7 +27,7 @@
+         mapping(address => bool) hasVoted;
+     }
+ 
+-    mapping(uint256 => ProposalVote) private _proposalVotes;
++    mapping(uint256 => ProposalVote) internal _proposalVotes;
+ 
+     /**
+      * @dev See {IGovernor-COUNTING_MODE}.
+diff -ruN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol
+--- governance/extensions/GovernorPreventLateQuorum.sol	2022-05-25 09:38:35.000000000 -0700
++++ governance/extensions/GovernorPreventLateQuorum.sol	2022-05-27 01:31:23.000000000 -0700
+@@ -21,8 +21,8 @@
+     using SafeCast for uint256;
+     using Timers for Timers.BlockNumber;
+ 
+-    uint64 private _voteExtension;
+-    mapping(uint256 => Timers.BlockNumber) private _extendedDeadlines;
++    uint64 internal _voteExtension;
++    mapping(uint256 => Timers.BlockNumber) internal _extendedDeadlines;
+ 
+     /// @dev Emitted when a proposal deadline is pushed back due to reaching quorum late in its voting period.
+     event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline);
 diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
---- governance/utils/Votes.sol	2022-05-25 15:36:58.849363940 -0400
-+++ governance/utils/Votes.sol	2022-05-25 16:07:31.901816357 -0400
+--- governance/utils/Votes.sol	2022-05-25 09:38:35.000000000 -0700
++++ governance/utils/Votes.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -35,7 +35,25 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -134,8 +146,8 @@ diff -ruN governance/utils/Votes.sol governance/utils/Votes.sol
 +    function _getVotingUnits(address) public virtual returns (uint256); // HARNESS: internal -> public
  }
 diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
---- token/ERC1155/ERC1155.sol	2022-05-25 15:36:58.853363841 -0400
-+++ token/ERC1155/ERC1155.sol	2022-05-25 16:07:31.901816357 -0400
+--- token/ERC1155/ERC1155.sol	2022-05-25 09:38:35.000000000 -0700
++++ token/ERC1155/ERC1155.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -268,7 +268,7 @@
          uint256 id,
          uint256 amount,
@@ -191,8 +203,8 @@ diff -ruN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol
              try IERC1155Receiver(to).onERC1155BatchReceived(operator, from, ids, amounts, data) returns (
                  bytes4 response
 diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
---- token/ERC20/ERC20.sol	2022-05-25 15:36:58.853363841 -0400
-+++ token/ERC20/ERC20.sol	2022-05-25 16:19:02.895813907 -0400
+--- token/ERC20/ERC20.sol	2022-05-25 09:38:35.000000000 -0700
++++ token/ERC20/ERC20.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -277,7 +277,7 @@
       * - `account` cannot be the zero address.
       * - `account` must have at least `amount` tokens.
@@ -203,8 +215,8 @@ diff -ruN token/ERC20/ERC20.sol token/ERC20/ERC20.sol
  
          _beforeTokenTransfer(account, address(0), amount);
 diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol
---- token/ERC20/extensions/ERC20FlashMint.sol	2022-05-25 15:36:58.853363841 -0400
-+++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-25 16:07:31.901816357 -0400
+--- token/ERC20/extensions/ERC20FlashMint.sol	2022-05-25 09:38:35.000000000 -0700
++++ token/ERC20/extensions/ERC20FlashMint.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -40,9 +40,11 @@
          require(token == address(this), "ERC20FlashMint: wrong token");
          // silence warning about unused variable without the addition of bytecode.
@@ -219,8 +231,8 @@ diff -ruN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20
       * @dev Returns the receiver address of the flash fee. By default this
       * implementation returns the address(0) which means the fee amount will be burnt.
 diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol
---- token/ERC20/extensions/ERC20Votes.sol	2022-03-02 13:56:14.831535075 -0500
-+++ token/ERC20/extensions/ERC20Votes.sol	2022-05-25 16:14:01.137717224 -0400
+--- token/ERC20/extensions/ERC20Votes.sol	2022-05-06 13:43:21.000000000 -0700
++++ token/ERC20/extensions/ERC20Votes.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -33,8 +33,8 @@
      bytes32 private constant _DELEGATION_TYPEHASH =
          keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)");
@@ -242,8 +254,8 @@ diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vote
  
          _writeCheckpoint(_totalSupplyCheckpoints, _subtract, amount);
 diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol
---- token/ERC20/extensions/ERC20Wrapper.sol	2022-05-25 15:36:58.853363841 -0400
-+++ token/ERC20/extensions/ERC20Wrapper.sol	2022-05-25 16:07:31.909819153 -0400
+--- token/ERC20/extensions/ERC20Wrapper.sol	2022-05-25 09:38:35.000000000 -0700
++++ token/ERC20/extensions/ERC20Wrapper.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -55,7 +55,7 @@
       * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal
       * function that can be exposed with access control if desired.
@@ -254,8 +266,8 @@ diff -ruN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wr
          _mint(account, value);
          return value;
 diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/draft-ERC721Votes.sol
---- token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-25 15:36:58.853363841 -0400
-+++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-25 16:07:31.909819153 -0400
+--- token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-25 09:38:35.000000000 -0700
++++ token/ERC721/extensions/draft-ERC721Votes.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -34,7 +34,7 @@
      /**
       * @dev Returns the balance of `account`.
@@ -266,8 +278,8 @@ diff -ruN token/ERC721/extensions/draft-ERC721Votes.sol token/ERC721/extensions/
      }
  }
 diff -ruN utils/Address.sol utils/Address.sol
---- utils/Address.sol	2022-05-25 15:36:58.853363841 -0400
-+++ utils/Address.sol	2022-05-25 16:07:31.909819153 -0400
+--- utils/Address.sol	2022-05-25 09:38:35.000000000 -0700
++++ utils/Address.sol	2022-05-27 01:31:23.000000000 -0700
 @@ -131,6 +131,7 @@
          uint256 value,
          string memory errorMessage
diff --git a/certora/harnesses/GovernorPreventLateQuorumHarness.sol b/certora/harnesses/GovernorPreventLateQuorumHarness.sol
index 773d2ef54..84858c710 100644
--- a/certora/harnesses/GovernorPreventLateQuorumHarness.sol
+++ b/certora/harnesses/GovernorPreventLateQuorumHarness.sol
@@ -31,19 +31,34 @@ contract GovernorPreventLateQuorumHarness is Governor, GovernorCountingSimple, G
         return _voteExtension;
     }
 
-    function getExtendedDeadlineIsUnset(uint256 id) public view returns(bool) {
-        return _extendedDeadlines[id].isUnset();
+    function getExtendedDeadlineIsUnset(uint256 proposalId) public view returns(bool) {
+        return _extendedDeadlines[proposalId].isUnset();
     }
 
-    function getExtendedDeadlineIsStarted(uint256 id) public view returns(bool) {
-        return _extendedDeadlines[id].isStarted();
+    function getExtendedDeadlineIsStarted(uint256 proposalId) public view returns(bool) {
+        return _extendedDeadlines[proposalId].isStarted();
     }
 
-    function getExtendedDeadline(uint256 id) public view returns(uint64) {
-        return _extendedDeadlines[id].getDeadline();
+    function getExtendedDeadline(uint256 proposalId) public view returns(uint64) {
+        return _extendedDeadlines[proposalId].getDeadline();
     }
 
     // Harness from GovernorCountingSimple // 
+
+    function getAgainstVotes(uint256 proposalId) public view returns(uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.againstVotes;
+    }
+
+    function getAbstainVotes(uint256 proposalId) public view returns(uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.abstainVotes;
+    }
+
+    function getForVotes(uint256 proposalId) public view returns(uint256) {
+        ProposalVote storage proposalvote = _proposalVotes[proposalId];
+        return proposalvote.forVotes;
+    }
     
     function quorumReached(uint256 proposalId) public view returns(bool) {
         return _quorumReached(proposalId);
diff --git a/certora/harnesses/InitializableBasicHarness.sol b/certora/harnesses/InitializableBasicHarness.sol
new file mode 100644
index 000000000..08ecbe971
--- /dev/null
+++ b/certora/harnesses/InitializableBasicHarness.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/proxy/utils/Initializable4.6.sol";
+
+contract InitializableBasicHarness is Initializable {
+
+    uint256 public unchangeable;
+    
+    modifier version1() {
+        require(_initialized == 1);
+        _;
+    }
+
+    modifier version2() {
+        require(_initialized == 2);
+        _;
+    }
+
+    function initialize(uint256 val) public initializer {
+        unchangeable = val;
+    }
+
+    function reinitialize(uint256 val) public reinitializer(2) {
+        unchangeable = val;
+    }
+
+    function returnsV1() public view version1 returns(uint256) {
+        return unchangeable/2;
+    }
+
+    function returnsV2() public view version2 returns(uint256) {
+        return unchangeable/3;
+    }
+}
diff --git a/certora/harnesses/InitializablrComplexHarness.sol b/certora/harnesses/InitializablrComplexHarness.sol
new file mode 100644
index 000000000..7a4de57c2
--- /dev/null
+++ b/certora/harnesses/InitializablrComplexHarness.sol
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../munged/proxy/utils/Initializable4.6.sol";
+
+contract InitializableBasicHarness is Initializable {
+
+    uint256 public unchangeable;
+
+    function initialize(uint256 _val) public initializer {
+        unchangeable = _val;
+    }
+    
+    function reinitialize(uint256 _val) public reinitializer(2) {
+        unchangeable = _val;
+    }
+    
+}
diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh
index f15e67219..64952a1d8 100644
--- a/certora/scripts/verifyGovernorPreventLateQuorum.sh
+++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh
@@ -1,12 +1,13 @@
 certoraRun \
     certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
-    --solc solc8.13 \
+    --solc solc \
     --optimistic_loop \
-    --disable_auto_cache_key_gen \
     --staging \
+    --settings -optimisticFallback=true \
     --send_only \
     --loop_iter 1 \
+    --rule $1 \
     --msg "$1" \
 
 
diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 9f331fb56..c7727a3d3 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -38,7 +38,9 @@ methods {
 
 
 // proposal was created - relation proved in noStartBeforeCreation
-definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0;
+definition proposalCreated(uint256 pId) returns bool = 
+    proposalSnapshot(pId) > 0
+    && proposalDeadline(pId) > 0;
 
 
 //////////////////////////////////////////////////////////////////////////////
diff --git a/certora/specs/GovernorPreventLateQuorum.spec b/certora/specs/GovernorPreventLateQuorum.spec
index bcadf76da..f6d3e1718 100644
--- a/certora/specs/GovernorPreventLateQuorum.spec
+++ b/certora/specs/GovernorPreventLateQuorum.spec
@@ -12,6 +12,9 @@ methods {
     getExtendedDeadlineIsUnset(uint256) returns bool envfree
     getExtendedDeadlineIsStarted(uint256) returns bool envfree
     getExtendedDeadline(uint256) returns uint64 envfree
+    getAgainstVotes(uint256) returns uint256 envfree
+    getAbstainVotes(uint256) returns uint256 envfree
+    getForVotes(uint256) returns uint256 envfree
     
     // more robust check than f.selector == _castVote(...).selector
     latestCastVoteCall() returns uint256 envfree 
@@ -22,6 +25,8 @@ methods {
     hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true)
     executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => CONSTANT
     scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) => CONSTANT
+    // checkpoint length ERC721
+    numCheckpoints(address) returns uint32
 }
 
 
@@ -54,27 +59,55 @@ function helperFunctionsWithRevertOnlyCastVote(uint256 proposalId, method f, env
 
 // proposal deadline can be extended (but isn't)
 definition deadlineExtendable(env e, uint256 pId) returns bool = 
-    getExtendedDeadlineIsUnset(pId)
+    getExtendedDeadlineIsUnset(pId) // deadline == 0
     && !quorumReached(e, pId);
 
 // proposal deadline has been extended
 definition deadlineExtended(env e, uint256 pId) returns bool = 
-    getExtendedDeadlineIsStarted(pId)
+    getExtendedDeadlineIsStarted(pId) // deadline > 0
     && quorumReached(e, pId);
 
+definition proposalNotCreated(env e, uint256 pId) returns bool = 
+    proposalSnapshot(pId) == 0
+    && proposalDeadline(pId) == 0
+    && getExtendedDeadlineIsUnset(pId)
+    && getAgainstVotes(pId) == 0
+    && getAbstainVotes(pId) == 0
+    && getForVotes(pId) == 0
+    && !quorumReached(e, pId);
+
 
 //////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////// Invariants /////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////
 
 /*
- * I1: A propsal must be in state deadlineExtendable or deadlineExtended.
- * --INVARIANT PASSING // fails for updateQuorumNumerator
- * --ADVANCED SANITY PASSING // can't sanity test failing rules, not sure how it works for invariants
+ * I1: If a proposal has reached quorum then the proposal snapshot (start block.number) must be non-zero
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN
+ */ 
+invariant quorumReachedEffect(env e, uint256 pId)
+    quorumReached(e, pId) => proposalCreated(pId) // bug: 0 supply 0 votes => quorumReached
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+
+/*
+ * I2: A non-existant proposal must meet the definition of one.
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN
  */
-invariant proposalInOneState(env e, uint256 pId)
-    deadlineExtendable(e, pId) || deadlineExtended(e, pId)
-    { preserved { require proposalCreated(pId); } }
+invariant proposalNotCreatedEffects(env e, uint256 pId)
+    !proposalCreated(pId) => proposalNotCreated(e, pId)
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+
+/*
+ * I3: A created propsal must be in state deadlineExtendable or deadlineExtended.
+ * INVARIANT NOT PASSING // fails for updateQuorumNumerator and in the initial state when voting token total supply is 0 (causes quoromReached to return true)
+ * ADVANCED SANITY NOT RAN 
+ */
+invariant proposalInOneState(env e, uint256 pId) 
+    proposalNotCreated(e, pId) || deadlineExtendable(e, pId) || deadlineExtended(e, pId)
+    // filtered { f -> f.selector != updateQuorumNumerator(uint256).selector } // * fails for this function
+    { preserved { requireInvariant proposalNotCreatedEffects(e, pId); }}
 
 
 //////////////////////////////////////////////////////////////////////////////
@@ -92,7 +125,7 @@ invariant proposalInOneState(env e, uint256 pId)
 rule deadlineChangeEffects(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
 
-    require (proposalCreated(pId));
+    requireInvariant quorumReachedEffect(e, pId);
     
     uint256 deadlineBefore = proposalDeadline(pId);
     f(e, args);
@@ -110,12 +143,12 @@ rule deadlineChangeEffects(method f) filtered {f -> !f.isView} {
 rule deadlineCantBeUnextended(method f) 
     filtered {
         f -> !f.isView
-        && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function
+        // && f.selector != updateQuorumNumerator(uint256).selector // * fails for this function
     } {
     env e; calldataarg args; uint256 pId;
 
     require(deadlineExtended(e, pId));
-    require(proposalCreated(pId));
+    requireInvariant quorumReachedEffect(e, pId);
     
     f(e, args);
     
@@ -125,14 +158,14 @@ rule deadlineCantBeUnextended(method f)
 
 /*
  * R3: A proposal's deadline can't change in deadlineExtended state.
- * RULE PASSING*
+ * RULE PASSING
  * ADVANCED SANITY PASSING 
  */ 
 rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
 
     require(deadlineExtended(e, pId));
-    require(proposalCreated(pId)); 
+    requireInvariant quorumReachedEffect(e, pId); 
     
     uint256 deadlineBefore = proposalDeadline(pId);
     f(e, args);
@@ -145,7 +178,7 @@ rule canExtendDeadlineOnce(method f) filtered {f -> !f.isView} {
 //////////////////////////// second set of rules ////////////////////////////
 
 // HIGH LEVEL RULE R6: deadline can only extended if quorum reached w/ <= timeOfExtension left to vote
-// I1, R4 and R5 are assumed in R6 so we prove them first
+// I3, R4 and R5 are assumed in R6 so we prove them first
 
 /*
  * R4: A change in hasVoted must be correlated with an increasing of the vote supports, i.e. casting a vote increases the total number of votes.
@@ -163,7 +196,7 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.
 
     bool hasVotedBefore = hasVoted(e, pId, acc);
 
-    helperFunctionsWithRevertOnlyCastVote(pId, f, e);
+    helperFunctionsWithRevertOnlyCastVote(pId, f, e); // should be f(e, args)
 
     uint256 againstAfter = votesAgainst();
     uint256 forAfter = votesFor();
@@ -175,11 +208,11 @@ rule hasVotedCorrelationNonzero(uint256 pId, method f, env e) filtered {f -> !f.
     assert 
         (!hasVotedBefore && hasVotedAfter) => 
         (againstBefore <= againstAfter && forBefore <= forAfter && abstainBefore <= abstainAfter), 
-        "no correlation: some category decreased"; // currently vacous but keeping for CI tests
+        "after a vote is cast, the number of votes for each category must not decrease"; // currently vacous but keeping for CI tests
     assert 
         (!hasVotedBefore && hasVotedAfter) => 
         (againstBefore < againstAfter || forBefore < forAfter || abstainBefore < abstainAfter),
-        "no correlation: no category increased";
+        "after a vote is cast, the number of votes of at least one category must increase";
 }
 
 
@@ -200,7 +233,7 @@ rule againstVotesDontCount(method f) filtered {f -> !f.isView} {
     bool quorumAfter = quorumReached(e, pId);
     uint256 againstAfter = votesAgainst();
 
-    assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum reached with against vote"; 
+    assert (againstBefore < againstAfter) => quorumBefore == quorumAfter, "quorum must not be reached with an against vote"; 
 }
 
 /*
@@ -211,9 +244,9 @@ rule againstVotesDontCount(method f) filtered {f -> !f.isView} {
 rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
 
-    // need invariant that proves that a propsal must be in state deadlineExtendable or deadlineExtended
-    require(deadlineExtended(e, pId) || deadlineExtendable(e, pId));
-    require(proposalCreated(pId));
+    requireInvariant proposalInOneState(e, pId);
+    requireInvariant quorumReachedEffect(e, pId); 
+    requireInvariant proposalNotCreatedEffects(e, pId);
 
     bool wasDeadlineExtendable = deadlineExtendable(e, pId);
     uint64 extension = lateQuorumVoteExtension();
@@ -221,8 +254,8 @@ rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
     f(e, args);
     uint256 deadlineAfter = proposalDeadline(pId);
     
-    assert(deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline was not extendable");
-    assert(deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used");
+    assert deadlineAfter > deadlineBefore => wasDeadlineExtendable, "deadline must have been extendable for the deadline to be extended";
+    assert deadlineAfter > deadlineBefore => deadlineBefore - e.block.number <= extension, "deadline extension should not be used";
 }
 
 /*
@@ -232,7 +265,8 @@ rule deadlineExtenededIfQuorumReached(method f) filtered {f -> !f.isView} {
  */
 rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
-    require(deadlineExtended(e, pId) || deadlineExtendable(e, pId));
+
+    requireInvariant proposalInOneState(e, pId);
     
     bool extendedBefore = deadlineExtended(e, pId);
     f(e, args);
@@ -247,33 +281,15 @@ rule extendedDeadlineValueSetIfQuorumReached(method f) filtered {f -> !f.isView}
 }
 
 /*
-* R8: If the deadline for a proposal has not been reached, users can still vote.
-* --RULE PASSING
-* --ADVANCED SANITY PASSING
-*/
-rule canVote(method f) filtered {f -> !f.isView} {
-    env e; calldataarg args; uint256 pId;
-    address acc = e.msg.sender;
-    uint256 deadline = proposalDeadline(pId);
-    bool votedBefore = hasVoted(e, pId, acc);
-    
-    require(proposalCreated(pId));
-    require(deadline >= e.block.number);
-    // last error? 
-    helperFunctionsWithRevertOnlyCastVote(pId, f, e);
-    bool votedAfter = hasVoted(e, pId, acc);
-    
-    assert !votedBefore && votedAfter => deadline >= e.block.number;
-}
-
-/*
- * R9: Deadline can never be reduced.
+ * R8: Deadline can never be reduced.
  * RULE PASSING
  * ADVANCED SANITY PASSING
  */
 rule deadlineNeverReduced(method f) filtered {f -> !f.isView} {
     env e; calldataarg args; uint256 pId;
-    require(proposalCreated(pId));
+
+    requireInvariant quorumReachedEffect(e, pId);
+    requireInvariant proposalNotCreatedEffects(e, pId);
 
     uint256 deadlineBefore = proposalDeadline(pId);
     f(e, args);
diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec
new file mode 100644
index 000000000..b390da45d
--- /dev/null
+++ b/certora/specs/Initializable.spec
@@ -0,0 +1,3 @@
+methods {
+    
+}
\ No newline at end of file