diff --git a/certora/conf/v1.5/safe.conf b/certora/conf/v1.5/hash.conf
similarity index 89%
rename from certora/conf/v1.5/safe.conf
rename to certora/conf/v1.5/hash.conf
index 4e4565d17..9e82324e9 100644
--- a/certora/conf/v1.5/safe.conf
+++ b/certora/conf/v1.5/hash.conf
@@ -5,7 +5,7 @@
     "link": [
 
     ],
-    "verify": "SafeHarness:certora/specs/v1.5/Safe.spec",
+    "verify": "SafeHarness:certora/specs/v1.5/Hash.spec",
 
     "assert_autofinder_success": true,
     "optimistic_summary_recursion": true,
diff --git a/certora/specs/v1.5/Hash.spec b/certora/specs/v1.5/Hash.spec
new file mode 100644
index 000000000..67217d450
--- /dev/null
+++ b/certora/specs/v1.5/Hash.spec
@@ -0,0 +1,45 @@
+/* A specification for the Safe setup function */
+
+
+// ---- Methods block ----------------------------------------------------------
+methods {
+    function getThreshold() external returns (uint256) envfree;
+
+    function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ;
+}
+
+// ---- Functions and ghosts ---------------------------------------------------
+
+
+// ---- Invariants -------------------------------------------------------------
+
+
+// ---- Rules ------------------------------------------------------------------
+
+/// @dev setup can only be called if threshold = 0 and setup sets threshold > 0 
+/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f
+
+rule setupThresholdZeroAndSetsPositiveThreshold(
+        address[] _owners,
+        uint256 _threshold,
+        address to,
+        bytes data,
+        address fallbackHandler,
+        address paymentToken,
+        uint256 payment,
+        address paymentReceiver) {
+    env e;
+
+    uint256 old_threshold = getThreshold();
+
+    // a successful call to setup
+    setup(e,_owners,_threshold,to,data,fallbackHandler,
+        paymentToken,payment,paymentReceiver);
+
+    uint256 new_threshold = getThreshold();
+
+    assert (
+        new_threshold >  0 &&
+        old_threshold == 0
+    );
+}
diff --git a/certora/specs/v1.5/Safe.spec b/certora/specs/v1.5/Safe.spec
deleted file mode 100644
index 0e9b986dc..000000000
--- a/certora/specs/v1.5/Safe.spec
+++ /dev/null
@@ -1,47 +0,0 @@
-/* A specification for the Safe setup function */
-
-
-// ---- Methods block ----------------------------------------------------------
-methods {
-    function getThreshold() external returns (uint256) envfree;
-
-    function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ;
-}
-
-// ---- Functions and ghosts ---------------------------------------------------
-
-
-// ---- Invariants -------------------------------------------------------------
-
-
-// ---- Rules ------------------------------------------------------------------
-
-/// @dev approvedHashes[user][hash] can only be changed by msg.sender==user
-/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 
-
-rule approvedHashesUpdate(method f,bytes32 userHash,address user) filtered {
-    f -> f.selector != sig:simulateAndRevert(address,bytes).selector
-} {
-    env e;
-
-    uint256 hashBefore = approvedHashVal(e,user,userHash);
-
-    calldataarg args;
-    f(e,args);
-
-    uint256 hashAfter = approvedHashVal(e,user,userHash);
-
-    assert (hashBefore != hashAfter =>
-        (e.msg.sender == user)
-    );
-}
-
-
-/// @dev approvedHashes is set when calling approveHash
-/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6
-
-rule approvedHashesSet(bytes32 hashToApprove) {
-    env e;
-    approveHash(e,hashToApprove);
-    assert(approvedHashVal(e,e.msg.sender,hashToApprove) == 1);
-}
\ No newline at end of file