diff --git a/.github/workflows/certora_4337.yml b/.github/workflows/certora_4337.yml
index 510c2c78e..3bcee4214 100644
--- a/.github/workflows/certora_4337.yml
+++ b/.github/workflows/certora_4337.yml
@@ -19,12 +19,12 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh', 'verifySignatureLengthCheck.sh']
+        rule: ['Safe4337Module', 'TransactionExecutionMethods', 'ValidationDataLastBitOne', 'SignatureLengthCheck']
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Install pnpm
-        uses: pnpm/action-setup@v3
+        uses: pnpm/action-setup@v4
         with:
           version: 9
 
@@ -33,7 +33,7 @@ jobs:
         with: { python-version: 3.11 }
 
       - name: Install certora cli
-        run: pip install -Iv certora-cli==7.3.0
+        run: pip install -r modules/4337/certora/requirements.txt
 
       - name: Install solc
         run: |
@@ -47,8 +47,7 @@ jobs:
       - name: Verify rule ${{ matrix.rule }}
         working-directory: ./modules/4337
         run: |
-          echo "key length" ${#CERTORAKEY}
-          chmod +x ./certora/scripts/${{ matrix.rule }}
-          ./certora/scripts/${{ matrix.rule }}
+          echo "Certora key length" ${#CERTORAKEY}
+          certoraRun certora/conf/${{ matrix.rule }}.conf --wait_for_results=all
         env:
           CERTORAKEY: ${{ secrets.CERTORA_KEY }}
diff --git a/README.md b/README.md
index 4888cc171..6ae37f079 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,7 @@ This repository contains a collection of modules for the [Safe Smart Account](ht
 - [4337 Module](./modules/4337)
 - [Allowance Module](./modules/allowances)
 - [Passkey](./modules/passkey)
+- [Recovery Module](./modules/recovery/)
 
 ## Examples
 
diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol
index 509564ccc..cdcaeef02 100644
--- a/modules/4337/certora/harnesses/Account.sol
+++ b/modules/4337/certora/harnesses/Account.sol
@@ -94,8 +94,10 @@ contract Account is Safe {
     }
 }
 
-// @notice This is a harness contract for the rule that verfies the validation data
-//         in case the checkSignature functions reverts.
+/*
+ * @notice This is a harness contract for the rule that verfies the validation data
+ *         in case the checkSignature functions reverts.
+ */
 contract AlwaysRevertingAccount {
     function checkSignatures(bytes32 dataHash, bytes memory data, bytes memory signatures) public view {
         revert();
diff --git a/modules/4337/certora/requirements.txt b/modules/4337/certora/requirements.txt
new file mode 100644
index 000000000..60f7546c3
--- /dev/null
+++ b/modules/4337/certora/requirements.txt
@@ -0,0 +1 @@
+certora-cli==7.3.0
diff --git a/modules/4337/certora/scripts/verify4337Module.sh b/modules/4337/certora/scripts/verify4337Module.sh
deleted file mode 100755
index 18a29bdae..000000000
--- a/modules/4337/certora/scripts/verify4337Module.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/bash
-
-params=()
-
-if [[ -n "$CI" ]]; then
-    params=("--wait_for_results")
-fi
-
-certoraRun certora/conf/Safe4337Module.conf \
-    "${params[@]}" \
-    "$@"
-
diff --git a/modules/4337/certora/scripts/verifySignatureLengthCheck.sh b/modules/4337/certora/scripts/verifySignatureLengthCheck.sh
deleted file mode 100755
index 702f55feb..000000000
--- a/modules/4337/certora/scripts/verifySignatureLengthCheck.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/bash
-
-params=()
-
-if [[ -n "$CI" ]]; then
-    params=("--wait_for_results")
-fi
-
-certoraRun certora/conf/SignatureLengthCheck.conf \
-    "${params[@]}" \
-    "$@"
-
diff --git a/modules/4337/certora/scripts/verifyTransactionExecutionMethods.sh b/modules/4337/certora/scripts/verifyTransactionExecutionMethods.sh
deleted file mode 100755
index 8056f5bd4..000000000
--- a/modules/4337/certora/scripts/verifyTransactionExecutionMethods.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/bin/bash
-
-params=()
-
-if [[ -n "$CI" ]]; then
-    params=("--wait_for_results")
-fi
-
-certoraRun certora/conf/TransactionExecutionMethods.conf \
-    "${params[@]}" \
-    "$@"
diff --git a/modules/4337/certora/scripts/verifyValidationData.sh b/modules/4337/certora/scripts/verifyValidationData.sh
deleted file mode 100755
index 44105a94e..000000000
--- a/modules/4337/certora/scripts/verifyValidationData.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/bin/bash
-
-params=()
-
-if [[ -n "$CI" ]]; then
-    params=("--wait_for_results")
-fi
-
-
-certoraRun certora/conf/ValidationDataLastBitOne.conf \
-    "${params[@]}" \
-    --msg "Safe4337Module $*" \
-    "$@"