diff --git a/modules/4337/certora/specs/Safe4337Module.spec b/modules/4337/certora/specs/Safe4337Module.spec
index 112d21637..ade56b0e4 100644
--- a/modules/4337/certora/specs/Safe4337Module.spec
+++ b/modules/4337/certora/specs/Safe4337Module.spec
@@ -25,6 +25,8 @@ methods {
     function getOperationHash(
         Safe4337Module.PackedUserOperation userOp
     ) external returns(bytes32) envfree => PER_CALLEE_CONSTANT;
+    function _checkSignatureLength(bytes calldata, uint256) internal returns(bool) => ALWAYS(true);
+
 }
 persistent ghost ERC2771MessageSender() returns address;
 
diff --git a/modules/4337/certora/specs/ValidationDataLastBitOne.spec b/modules/4337/certora/specs/ValidationDataLastBitOne.spec
index 9f48e24bb..c2b1a8970 100644
--- a/modules/4337/certora/specs/ValidationDataLastBitOne.spec
+++ b/modules/4337/certora/specs/ValidationDataLastBitOne.spec
@@ -12,7 +12,7 @@ methods {
         Safe4337Module.PackedUserOperation userOp
     ) external returns(bytes32) envfree => PER_CALLEE_CONSTANT;
 
-    function _._checkSignatureLength(bytes calldata, uint256) internal => ALWAYS(true);
+    function _checkSignatureLength(bytes calldata, uint256) internal returns(bool)=> ALWAYS(true);
 }
 
 rule validationDataLastBitOneIfCheckSignaturesFails(address sender,