diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index fb854dc22..db054b7b0 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -25,7 +25,7 @@ jobs:
               uses: actions/setup-java@v3
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
-            - name: Install certora cli-beta
+            - name: Install certora cli
               run: pip install -Iv certora-cli
 
             - name: Install solc
diff --git a/certora/scripts/verifySafe.sh b/certora/scripts/verifySafe.sh
index c909a4188..7315e1bb5 100755
--- a/certora/scripts/verifySafe.sh
+++ b/certora/scripts/verifySafe.sh
@@ -10,7 +10,7 @@ certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
     --solc solc7.6 \
     --optimistic_loop \
-    --prover_args "-optimisticFallback true" \
+    --prover_args '-optimisticFallback true' \
     --loop_iter 3 \
     --optimistic_hashing \
     --hashing_length_bound 352 \
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
index 8564aeb79..103367b7d 100644
--- a/certora/specs/Safe.spec
+++ b/certora/specs/Safe.spec
@@ -130,6 +130,28 @@ hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644
     fallbackHandlerAddress = newFallbackHandlerAddress;
 }
 
+invariant threholdShouldBeLessThanOwners() getOwnersCount() >= getThreshold()
+    filtered { f -> reachableOnly(f) }
+    { preserved {
+        // The prover found a counterexample if the owners count is max uint256,
+        // but this is not a realistic scenario.
+        require getOwnersCount() >= 1 && getOwnersCount() < MAX_UINT256();
+      }
+    }
+
+invariant safeOwnerCannotBeItself(env e) !isOwner(e, currentContract)
+    filtered { f -> reachableOnly(f) }
+
+rule safeOwnerCannotBeSentinelAddress(method f) filtered {
+    f -> reachableOnly(f)
+} {
+    calldataarg args; env e;
+    f(e, args);
+
+    assert isOwner(e, 1) == false;
+}
+
+
 rule fallbackHandlerAddressChange(method f) filtered {
     f -> f.selector != sig:simulateAndRevert(address,bytes).selector &&
          f.selector != sig:getStorageAt(uint256,uint256).selector