diff --git a/certora/scripts/verifyAccessControl.sh b/certora/scripts/verifyAccessControl.sh
index 6b1a7ba05..eb706d063 100644
--- a/certora/scripts/verifyAccessControl.sh
+++ b/certora/scripts/verifyAccessControl.sh
@@ -3,7 +3,6 @@ certoraRun \
     --verify AccessControlHarness:certora/specs/AccessControl.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "modifier check"
+    --cloud \
+    --msg "AccessControl verification"
     
\ No newline at end of file
diff --git a/certora/scripts/verifyAllSasha.sh b/certora/scripts/verifyAllSasha.sh
new file mode 100644
index 000000000..e87893bf9
--- /dev/null
+++ b/certora/scripts/verifyAllSasha.sh
@@ -0,0 +1,5 @@
+sh certora/scripts/verifyTimelock.sh
+sh certora/scripts/verifyERC1155.sh
+sh certora/scripts/verifyERC20FlashMint.sh
+sh certora/scripts/verifyERC20Wrapper.sh
+sh certora/scripts/verifyAccessControl.sh
diff --git a/certora/scripts/verifyERC1155.sh b/certora/scripts/verifyERC1155.sh
index 169df616d..84c59fc47 100644
--- a/certora/scripts/verifyERC1155.sh
+++ b/certora/scripts/verifyERC1155.sh
@@ -4,8 +4,6 @@ certoraRun \
     --solc solc8.2 \
     --optimistic_loop \
     --loop_iter 3 \
-    --staging \
-    --rule_sanity \
-    --rule "$1" \
-    --msg "$1 check"
+    --cloud \
+    --msg "ERC1155 verification"
     
\ No newline at end of file
diff --git a/certora/scripts/verifyERC20FlashMint.sh b/certora/scripts/verifyERC20FlashMint.sh
index cd29f5b1a..0af81e006 100644
--- a/certora/scripts/verifyERC20FlashMint.sh
+++ b/certora/scripts/verifyERC20FlashMint.sh
@@ -4,7 +4,6 @@ certoraRun \
     --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "flashMint"
+    --cloud \
+    --msg "ERC20FlashMint verification"
     
\ No newline at end of file
diff --git a/certora/scripts/verifyERC20Wrapper.sh b/certora/scripts/verifyERC20Wrapper.sh
index 15654d84e..e1ef85ef0 100644
--- a/certora/scripts/verifyERC20Wrapper.sh
+++ b/certora/scripts/verifyERC20Wrapper.sh
@@ -4,7 +4,6 @@ certoraRun \
     --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
     --solc solc8.2 \
     --optimistic_loop \
-    --staging \
-    --rule_sanity \
-    --msg "ERC20wrapper spec"
+    --cloud \
+    --msg "ERC20Wrapper verification"
     
\ No newline at end of file
diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh
index 2876d5f92..5afc11911 100644
--- a/certora/scripts/verifyTimelock.sh
+++ b/certora/scripts/verifyTimelock.sh
@@ -5,8 +5,6 @@ certoraRun \
     --optimistic_loop \
     --loop_iter 3 \
     --staging alex/new-dt-hashing-alpha \
-    --rule_sanity \
     --settings -byteMapHashingPrecision=32 \
-    --rule "$1" \
-    --msg "$1"
+    --msg "TimelockController verification"
       
\ No newline at end of file
diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec
index 01c1b4295..bc95288e9 100644
--- a/certora/specs/ERC20Wrapper.spec
+++ b/certora/specs/ERC20Wrapper.spec
@@ -195,6 +195,7 @@ rule recoverSpec(env e){
     uint256 wrapperTotalBefore = totalSupply(e);
     uint256 wrapperUserBalanceBefore = balanceOf(e, account);
     uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender);
+    uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract);
 
     mathint value = underlyingThisBalanceBefore - wrapperTotalBefore;
 
diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec
index cbad3336e..d0e2a6b74 100644
--- a/certora/specs/RulesInProgress.spec
+++ b/certora/specs/RulesInProgress.spec
@@ -136,4 +136,28 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) {
     uint256 ps = proposalSnapshot(pId);
 
     assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla";
-}
\ No newline at end of file
+}
+
+
+
+/////////////////// 2nd iteration with OZ ////////////////////////// 
+
+// STATUS - in progress
+// execute() is the only way to set timestamp to 1
+rule getTimestampOnlyChange(method f, env e){
+    bytes32 id;
+    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay;
+    address[] targets; uint256[] values; bytes[] datas;
+
+    require (targets[0] == target && values[0] == value && datas[0] == data)
+                || (targets[1] == target && values[1] == value && datas[1] == data)
+                || (targets[2] == target && values[2] == value && datas[2] == data);
+
+    hashIdCorrelation(id, target, value, data, predecessor, salt);
+
+    executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas);
+
+    assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector  
+                                        || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
+}
+
diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec
index fbce17bfd..29aeaee69 100644
--- a/certora/specs/TimelockController.spec
+++ b/certora/specs/TimelockController.spec
@@ -335,27 +335,3 @@ rule cancelChange(env e){
 
     assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
 }
-
-
-
-
-
-
-// STATUS - in progress
-// execute() is the only way to set timestamp to 1
-rule getTimestampOnlyChange(method f, env e){
-    bytes32 id;
-    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; uint256 delay;
-    address[] targets; uint256[] values; bytes[] datas;
-
-    require (targets[0] == target && values[0] == value && datas[0] == data)
-                || (targets[1] == target && values[1] == value && datas[1] == data)
-                || (targets[2] == target && values[2] == value && datas[2] == data);
-
-    hashIdCorrelation(id, target, value, data, predecessor, salt);
-
-    executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas);
-
-    assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector  
-                                        || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector, "Did you find a way to break the system?";
-}