diff --git a/certora/confs/WebAuthnBitVectorTheory.conf b/certora/confs/WebAuthnBitVectorTheory.conf
index 285439bef..7b928b6fa 100644
--- a/certora/confs/WebAuthnBitVectorTheory.conf
+++ b/certora/confs/WebAuthnBitVectorTheory.conf
@@ -13,6 +13,7 @@
         "@account-abstraction=node_modules/@account-abstraction"
     ],
     "prover_args": ["-useBitVectorTheory"],
+    "rule": ["encodeClientDataJsonIntegrity", "uniqueMessagePerChallenge"],
     "solc": "solc8.23",
     "solc_via_ir": false,
     "optimistic_loop": true,
diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
index 8c9fd02f2..0321274e4 100644
--- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
+++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
@@ -29,4 +29,21 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory {
         require(success);
         magicValue = abi.decode(result, (bytes4));
     }
+
+    function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) {
+        bytes32 codeHash = keccak256(
+            abi.encodePacked(
+                type(SafeWebAuthnSignerProxy).creationCode,
+                "01234567891011121314152546",
+                uint256(uint160(address(SINGLETON))),
+                x,
+                y,
+                uint256(P256.Verifiers.unwrap(verifiers))
+            )
+        );
+        value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash)));
+    }
+    function castToAddress(uint256 value) public pure returns (address addr){
+        addr = address(uint160(value));
+    }
 }
diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
index 731f268c4..c0e6c7e72 100644
--- a/certora/specs/SafeWebAuthnSignerFactory.spec
+++ b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -2,7 +2,8 @@ using SafeWebAuthnSignerProxy as proxy;
 using SafeWebAuthnSignerSingleton as singleton;
 
 methods{
-    function getSigner(uint256, uint256, P256.Verifiers) external returns (address);
+    // function getSigner(uint256, uint256, P256.Verifiers) external returns (address);
+    // function getSigner(uint256 x, uint256 y, P256.Verifiers v) internal returns (address) => getSignerGhost(x, y, v);
     function createSigner(uint256, uint256, P256.Verifiers) external returns (address);
     function hasNoCode(address) external returns (bool) envfree;
 }
@@ -30,10 +31,51 @@ rule singletonNeverChanges()
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ getSigner is unique for every x,y and verifier combination    (Violated but low prob)                               │
+ getSigner is unique for every x,y and verifier combination, proved with assumptions: 
+    1.)      value before cast to address <= max_uint160.
+    2.)      munging required to complete signer data to be constructed from full 32bytes size arrays 
+        function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) {
+        bytes32 codeHash = keccak256(
+            abi.encodePacked(
+                type(SafeWebAuthnSignerProxy).creationCode,
+                "01234567891011121314152546", <--------------- HERE!
+                uint256(uint160(address(SINGLETON))),
+                x,
+                y,
+                uint256(P256.Verifiers.unwrap(verifiers))
+            )
+        );
+        value = uint256(keccak256(abi.encodePacked(hex"ff", address(this), bytes32(0), codeHash)));
+    }                  
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
-// consider adding the following munging after the creationcode to get a more clear dump 01234567891011121314152546
+
+// helper rule to justify the use of the munged implementation (proved)
+rule mungedEquivalence()
+{
+    env e1;
+    env e2;
+
+    require e1.msg.value == 0 && e2.msg.value == 0;
+    uint256 x;
+    uint256 y;
+    P256.Verifiers verifier;
+
+    storage s = lastStorage;
+
+    uint256 harnessedSignerValue = getSignerHarnessed@withrevert(e1, x, y, verifier);
+    bool harnessedSignerRevert1 = lastReverted;
+
+    address harnessedSigner = castToAddress@withrevert(e1, harnessedSignerValue);
+    bool harnessedSignerRevert2 = harnessedSignerRevert1 && lastReverted;
+
+    address signer = getSigner@withrevert(e2, x, y, verifier) at s;
+    bool signerRevert = lastReverted;
+
+    assert (harnessedSignerRevert2 == signerRevert);
+    assert (!harnessedSignerRevert2 && !signerRevert) => (harnessedSigner == signer);
+}
+
 
 rule uniqueSigner(){
     env e;
@@ -42,23 +84,37 @@ rule uniqueSigner(){
     uint256 firstY;
     P256.Verifiers firstVerifier;
 
-    address firstSigner = getSigner(e, firstX, firstY, firstVerifier);
+    uint256 firstSignerValue = getSignerHarnessed(e, firstX, firstY, firstVerifier);
+    require firstSignerValue <= max_uint160;
+
+    address firstSigner = castToAddress(e, firstSignerValue);
 
     uint256 secondX;
     uint256 secondY;
     P256.Verifiers secondVerifier;
 
-    address secondSigner = getSigner(e, secondX, secondY, secondVerifier);
+    uint256 secondSignerValue = getSignerHarnessed(e, secondX, secondY, secondVerifier);
+    require secondSignerValue <= max_uint160;
+
+    address secondSigner = castToAddress(e, secondSignerValue);
+
 
     assert firstSigner == secondSigner <=> (firstX == secondX && firstY == secondY && firstVerifier == secondVerifier);
 }
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ createSigner and getSigner always returns the same address   (Violated but low prob)                                │
+│ createSigner and getSigner always returns the same address   (Proved under assumption)                              │
 └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 */
 
+// Summary is correct only if the unique signer rule is proved !!! 
+ghost getSignerGhost(uint256, uint256, P256.Verifiers) returns address {
+    axiom forall uint256 x1. forall uint256 y1. forall P256.Verifiers v1.
+    forall uint256 x2. forall uint256 y2. forall P256.Verifiers v2.
+    (getSignerGhost(x1, y1, v1) == getSignerGhost(x2, y2, v2)) <=> (x1 == x2 && y1 == y2 && v1 == v2); 
+}
+
 rule createAndGetSignerEquivalence(){
     env e;
 
diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
index f3abcbc47..efc64ed45 100644
--- a/certora/specs/WebAuthn.spec
+++ b/certora/specs/WebAuthn.spec
@@ -86,10 +86,11 @@ rule verifySignatureEq(){
     bool result1 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers);
     bool firstCallRevert = lastReverted;
 
-    bool result2 = verifySignature@withrevert(e, challenge, bytesSignature, authenticatorFlags, x, y, verifiers) at firstStorage;
+    bool result2 = verifySignature@withrevert(e, challenge, structSignature, authenticatorFlags, x, y, verifiers) at firstStorage;
     bool secondCallRevert = lastReverted;
 
-    assert (firstCallRevert == secondCallRevert) || (result1 == result2);
+    assert firstCallRevert == secondCallRevert;
+    assert (!firstCallRevert && !secondCallRevert) => result1 == result2;
 }
 
 /*
diff --git a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol
index 26d9f54c0..629fc574a 100644
--- a/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol
+++ b/modules/passkey/contracts/SafeWebAuthnSignerFactory.sol
@@ -36,6 +36,7 @@ contract SafeWebAuthnSignerFactory is ISafeSignerFactory {
         bytes32 codeHash = keccak256(
             abi.encodePacked(
                 type(SafeWebAuthnSignerProxy).creationCode,
+                "01234567891011121314152546", // munged for word alignment workaround (32 bytes)
                 uint256(uint160(address(SINGLETON))),
                 x,
                 y,