diff --git a/certora/harnesses/AccessManagedHarness.sol b/certora/harnesses/AccessManagedHarness.sol
index 50be23ad5..1e73d445d 100644
--- a/certora/harnesses/AccessManagedHarness.sol
+++ b/certora/harnesses/AccessManagedHarness.sol
@@ -10,27 +10,30 @@ contract AccessManagedHarness is AccessManaged {
 
     constructor(address initialAuthority) AccessManaged(initialAuthority) {}
 
-    function someFunction() public restricted() {
+    function someFunction() public restricted {
         // Sanity for FV: the msg.data when calling this function should be the same as the data used when checking
         // the schedule. This is a reformulation of `msg.data == SOME_FUNCTION_CALLDATA` that focuses on the operation
         // hash for this call.
         require(
-            IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data)
-            ==
-            IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA)
+            IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data) ==
+                IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA)
         );
     }
 
     function authority_canCall_immediate(address caller) public view returns (bool result) {
-        (result,) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+        (result, ) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
     }
 
     function authority_canCall_delay(address caller) public view returns (uint32 result) {
-        (,result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
+        (, result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector);
     }
 
     function authority_getSchedule(address caller) public view returns (uint48) {
         IAccessManager manager = IAccessManager(authority());
         return manager.getSchedule(manager.hashOperation(caller, address(this), SOME_FUNCTION_CALLDATA));
     }
+
+    function _hasCode(address account) public view returns (bool) {
+        return account.code.length > 0;
+    }
 }
diff --git a/certora/specs/AccessManaged.spec b/certora/specs/AccessManaged.spec
index 7e4619d96..2b232a4bf 100644
--- a/certora/specs/AccessManaged.spec
+++ b/certora/specs/AccessManaged.spec
@@ -7,9 +7,10 @@ methods {
     function authority_canCall_immediate(address) external returns (bool);
     function authority_canCall_delay(address)     external returns (uint32);
     function authority_getSchedule(address)       external returns (uint48);
+    function _hasCode(address)                    external returns (bool) envfree;
 
     // Summaries
-    function _.setAuthority(address)               external => DISPATCHER(true);
+    function _.setAuthority(address)              external => DISPATCHER(true);
 }
 
 invariant isConsumingScheduledOpClean()
@@ -35,3 +36,24 @@ rule callRestrictedFunction(env e) {
         )
     );
 }
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Only valid authorities can be set by the current authority                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule setAuthority(env e) {
+    require nonpayable(e);
+
+    address newAuthority;
+
+    address previousAuthority = authority();
+
+    setAuthority@withrevert(e, newAuthority);
+    bool success = !lastReverted;
+
+    assert (success && authority() == newAuthority) <=> (
+        previousAuthority == e.msg.sender &&
+        _hasCode(newAuthority)
+    );
+}