diff --git a/certora/confs/ProxySimulator.conf b/certora/confs/ProxySimulator.conf
deleted file mode 100644
index 1dddbee43..000000000
--- a/certora/confs/ProxySimulator.conf
+++ /dev/null
@@ -1,29 +0,0 @@
-{
-    "assert_autofinder_success": true,
-    "files": [
-        "certora/helpers/ProxySimulator.sol",
-        "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
-        "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        "modules/passkey/contracts/libraries/P256.sol",
-        "modules/passkey/contracts/libraries/WebAuthn.sol",
-        "certora/harnesses/WebAuthnHarness.sol",
-
-    ],
-    "link": [
-        "ProxySimulator:_proxy=SafeWebAuthnSignerProxy",
-        "SafeWebAuthnSignerProxy:_VERIFIERS=P256",
-        "SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
-    ],
-    "packages":[
-        "@safe-global=node_modules/@safe-global",
-        "@account-abstraction=node_modules/@account-abstraction"
-    ],
-    "solc": "solc8.23",
-    "solc_via_ir": false,
-    "optimistic_loop": true,
-    "loop_iter": "6",
-    "optimistic_hashing": true,
-    "hashing_length_bound": "2048",
-    "rule_sanity": "basic",
-    "verify": "ProxySimulator:certora/specs/ProxySimulator.spec"
-}
\ No newline at end of file
diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
index 872879470..26ae793d7 100644
--- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
+++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
@@ -29,11 +29,4 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory {
         require(success);
         magicValue = abi.decode(result, (bytes4));
     }
-
-    // /**
-    //     munge to pass the SignerCreationCantOverride rule.
-    //  */
-    // function _hasNoCode(address account) internal view override returns (bool result) {
-    //     return account.code.length > 0;
-    // }
 }
diff --git a/certora/helpers/ProxySimulator.sol b/certora/helpers/ProxySimulator.sol
deleted file mode 100644
index d9decc29f..000000000
--- a/certora/helpers/ProxySimulator.sol
+++ /dev/null
@@ -1,24 +0,0 @@
-// SPDX-License-Identifier: LGPL-3.0-only
-/* solhint-disable no-complex-fallback */
-pragma solidity >=0.8.0;
-
-import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol";
-
-contract ProxySimulator {
-
-    address internal _proxy;
-
-    constructor(address proxy) {
-        _proxy = proxy;
-    }
-
-    function authenticate(bytes32 message, bytes calldata signature) external returns (bytes4) {
-        bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature);
-
-        (bool success, bytes memory result) = _proxy.call(data);
-
-        require(success);
-
-        return abi.decode(result, (bytes4));
-    }
-}
\ No newline at end of file
diff --git a/certora/specs/ProxySimulator.spec b/certora/specs/ProxySimulator.spec
deleted file mode 100644
index 43cf3a30d..000000000
--- a/certora/specs/ProxySimulator.spec
+++ /dev/null
@@ -1,56 +0,0 @@
-using SafeWebAuthnSignerProxy as SafeWebAuthnSignerProxy;
-using WebAuthnHarness as WebAuthnHarness;
-
-methods {
-    function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) => 
-        verifySignatureAllowMalleabilityGhost(a, b, c, d, e, f);
-
-    function WebAuthn.encodeSigningMessage(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) internal returns (bytes memory) =>
-        GETencodeSigningMessageCVL(challenge, authenticatorData, clientDataFields);
-
-    function WebAuthnHarness.checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal returns (bool) =>
-        checkInjectiveSummary(challenge, authenticatorData, clientDataFields, result);
-}
-
-function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes
-{
-    env e;
-    return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields);
-}
-
-ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool {
-    axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 z1. forall bytes32 x2. forall bytes32 y2. forall bytes32 z2. forall bytes32 result.
-    checkInjectiveSummary(x1, y1, z1, result) && checkInjectiveSummary(x2, y2, z2, result) => x1 == x2;
-}
-
-ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool {
-    axiom forall P256.Verifiers a. forall bytes32 message1. forall bytes32 message2. forall uint256 c. forall uint256 d. forall uint256 e. forall uint256 f.
-        verifySignatureAllowMalleabilityGhost(a, message1, c, d, e, f) && 
-        verifySignatureAllowMalleabilityGhost(a, message2, c, d, e, f) => message1 == message2;
-}
-
-// This is the same MAGIC_VALUE constant used in ERC1271.
-definition MAGIC_VALUE() returns bytes4 = to_bytes4(0x1626ba7e);
-
-methods {
-    function authenticate(bytes32, bytes) external returns (bytes4) envfree;
-    function _._ external => DISPATCH [
-        SafeWebAuthnSignerProxy._,
-        SafeWebAuthnSignerSingleton._
-    ] default NONDET;
-}
-
-/*
-Property 14. Proxy - verify return data from the fallback is only one of the magicNumbers
-Uses another contract that simulates interaction with the proxy. The reason is that the prover doesn't check all
-possible calldata values so this simulation will make the prover choose different values that will be passed on the calldata.
-Rule stuck.
-*/
-rule proxyReturnValue {
-    bytes32 message;
-    bytes signature;
-
-    bytes4 ret = authenticate(message, signature);
-
-    satisfy ret == MAGIC_VALUE() || ret == to_bytes4(0);
-}
diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec
index 07b61934f..45bef619b 100644
--- a/certora/specs/SafeWebAuthnSignerSingleton.spec
+++ b/certora/specs/SafeWebAuthnSignerSingleton.spec
@@ -84,44 +84,6 @@ rule verifyIsValidSignatureAreEqual(env e){
                                          (magicValue_hashed == to_bytes4(0) && magicValue_message == to_bytes4(0));
 }
 
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Once signer passed isValidSignature it will never fail on it after any call                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-
-rule verifyIsValidSignatureWillContinueToSucceed(){
-    env e;
-    env e1;
-    env e2;
-    env e3;
-    require e1.msg.value == 0 && e2.msg.value == 0 && e3.msg.value == 0;
-
-    method f;
-    calldataarg args;
-
-    bytes32 message;
-    WebAuthn.Signature sigStruct;
-    bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct);
-
-    bytes32 message3;
-    WebAuthn.Signature sigStruct3;
-    bytes signature3 = WebAuthnHarness.encodeSignature(e, sigStruct3);
-
-    bytes4 firstVerified = isValidSignature@withrevert(e1, message, signature);
-    bool firstReverted = lastReverted;
-
-    f(e, args);
-    // isValidSignature(e3, message3, signature3);
-
-    bytes4 secondVerify = isValidSignature@withrevert(e2, message, signature);
-    bool secondRevert = lastReverted;
-
-    assert firstReverted == secondRevert;
-    assert (!firstReverted && !secondRevert) => (firstVerified == secondVerify);
-    satisfy true;
-}
-
 rule isValidSignatureRevertingConditions {
     env e;
     bytes32 message;