diff --git a/certora/specs/AccessControlDefaultAdminRules.spec b/certora/specs/AccessControlDefaultAdminRules.spec
index ab9074fcf..6b116b637 100644
--- a/certora/specs/AccessControlDefaultAdminRules.spec
+++ b/certora/specs/AccessControlDefaultAdminRules.spec
@@ -284,7 +284,7 @@ rule beginDefaultAdminTransfer(env e, address newAdmin) {
   // effect
   assert success => pendingDefaultAdmin_() == newAdmin,
     "pending default admin is set";
-  assert success => pendingDefaultAdminSchedule_() == assert_uint48(e.block.timestamp + defaultAdminDelay(e)),
+  assert success => to_mathint(pendingDefaultAdminSchedule_()) == e.block.timestamp + defaultAdminDelay(e),
     "pending default admin delay is set";
 }
 
@@ -309,7 +309,7 @@ rule pendingDefaultAdminDelayEnforced(env e1, env e2, method f, calldataarg args
   // change can only happen towards the newAdmin, with the delay
   assert adminAfter != adminBefore => (
     adminAfter == newAdmin &&
-    e2.block.timestamp >= assert_uint256(e1.block.timestamp + delayBefore)
+    to_mathint(e2.block.timestamp) >= e1.block.timestamp + assert_uint256(delayBefore)
   ),
     "The admin can only change after the enforced delay and to the previously scheduled new admin";
 }
@@ -395,7 +395,7 @@ rule changeDefaultAdminDelay(env e, uint48 newDelay) {
     "pending delay is set";
 
   assert success => (
-    pendingDelaySchedule_(e) > assert_uint48(e.block.timestamp) ||
+    assert_uint256(pendingDelaySchedule_(e)) > e.block.timestamp ||
     delayBefore == newDelay || // Interpreted as decreasing, x - x = 0
     defaultAdminDelayIncreaseWait() == 0
   ),
@@ -421,7 +421,7 @@ rule pendingDelayWaitEnforced(env e1, env e2, method f, calldataarg args, uint48
 
   assert delayAfter != delayBefore => (
     delayAfter == newDelay &&
-    e2.block.timestamp >= assert_uint256(delayWait)
+    to_mathint(e2.block.timestamp) >= delayWait
   ),
     "A delay can only change after the applied schedule";
 }
@@ -435,9 +435,9 @@ rule pendingDelayWait(env e, uint48 newDelay) {
   uint48 oldDelay = defaultAdminDelay(e);
   changeDefaultAdminDelay(e, newDelay);
 
-  assert newDelay > oldDelay => pendingDelaySchedule_(e) == assert_uint48(increasingDelaySchedule(e, newDelay)),
+  assert newDelay > oldDelay => to_mathint(pendingDelaySchedule_(e)) == increasingDelaySchedule(e, newDelay),
     "Delay wait is the minimum between the new delay and a threshold when the delay is increased";
-  assert newDelay <= oldDelay => pendingDelaySchedule_(e) == assert_uint48(decreasingDelaySchedule(e, newDelay)),
+  assert newDelay <= oldDelay => to_mathint(pendingDelaySchedule_(e)) == decreasingDelaySchedule(e, newDelay),
     "Delay wait is the difference between the current and the new delay when the delay is decreased";
 }
 
diff --git a/certora/specs/methods/IAccessControlDefaultAdminRules.spec b/certora/specs/methods/IAccessControlDefaultAdminRules.spec
index a9dd08b7f..d02db180d 100644
--- a/certora/specs/methods/IAccessControlDefaultAdminRules.spec
+++ b/certora/specs/methods/IAccessControlDefaultAdminRules.spec
@@ -1,36 +1,36 @@
-import "./IERC5313.spec"
+import "./IERC5313.spec";
 
 methods {
     // === View ==
     
     // Default Admin
-    defaultAdmin() returns(address) envfree
-    pendingDefaultAdmin() returns(address, uint48) envfree
+    function defaultAdmin() external returns(address) envfree;
+    function pendingDefaultAdmin() external returns(address, uint48) envfree;
     
     // Default Admin Delay
-    defaultAdminDelay() returns(uint48)
-    pendingDefaultAdminDelay() returns(uint48, uint48)
-    defaultAdminDelayIncreaseWait() returns(uint48) envfree
+    function defaultAdminDelay() external returns(uint48);
+    function pendingDefaultAdminDelay() external returns(uint48, uint48);
+    function defaultAdminDelayIncreaseWait() external returns(uint48) envfree;
     
     // === Mutations ==
 
     // Default Admin
-    beginDefaultAdminTransfer(address)
-    cancelDefaultAdminTransfer()
-    acceptDefaultAdminTransfer()
+    function beginDefaultAdminTransfer(address) external;
+    function cancelDefaultAdminTransfer() external;
+    function acceptDefaultAdminTransfer() external;
 
     // Default Admin Delay
-    changeDefaultAdminDelay(uint48)
-    rollbackDefaultAdminDelay()
+    function changeDefaultAdminDelay(uint48) external;
+    function rollbackDefaultAdminDelay() external;
 
     // == FV ==
     
     // Default Admin
-    pendingDefaultAdmin_() returns (address) envfree
-    pendingDefaultAdminSchedule_() returns (uint48) envfree
+    function pendingDefaultAdmin_() external returns (address) envfree;
+    function pendingDefaultAdminSchedule_() external returns (uint48) envfree;
     
     // Default Admin Delay
-    pendingDelay_() returns (uint48)
-    pendingDelaySchedule_() returns (uint48)
-    delayChangeWait_(uint48) returns (uint48)
+    function pendingDelay_() external returns (uint48);
+    function pendingDelaySchedule_() external returns (uint48);
+    function delayChangeWait_(uint48) external returns (uint48);
 }