diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol
new file mode 100644
index 00000000000..19437e0fc7e
--- /dev/null
+++ b/certora/harnesses/InitializableHarness.sol
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../patched/proxy/utils/Initializable.sol";
+
+contract InitializableHarness is Initializable {
+    function initialize()          public initializer      {}
+    function reinitialize(uint8 n) public reinitializer(n) {}
+    function disable()             public { _disableInitializers(); }
+
+    function nested_init_init()                     public initializer      { initialize();    }
+    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
+    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
+    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
+
+    function version() public view returns (uint8) {
+        return _getInitializedVersion();
+    }
+
+    function initializing() public view returns (bool) {
+        return _isInitializing();
+    }
+}
diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol
new file mode 100644
index 00000000000..4d30e504189
--- /dev/null
+++ b/certora/harnesses/Ownable2StepHarness.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable2Step.sol";
+
+contract Ownable2StepHarness is Ownable2Step {
+  function restricted() external onlyOwner {}
+}
diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol
new file mode 100644
index 00000000000..93cbb4770c2
--- /dev/null
+++ b/certora/harnesses/OwnableHarness.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable.sol";
+
+contract OwnableHarness is Ownable {
+  function restricted() external onlyOwner {}
+}
diff --git a/certora/run.js b/certora/run.js
index 074a6ccde4c..2fb942c7622 100644
--- a/certora/run.js
+++ b/certora/run.js
@@ -8,7 +8,7 @@
 
 const MAX_PARALLEL = 4;
 
-const specs = require(__dirname + '/specs.json');
+let specs = require(__dirname + '/specs.json');
 
 const proc = require('child_process');
 const { PassThrough } = require('stream');
@@ -20,14 +20,20 @@ if (request.startsWith('-')) {
   extraOptions.unshift(request);
   request = '';
 }
-const [reqSpec, reqContract] = request.split(':').reverse();
 
-for (const { spec, contract, files, options = [] } of Object.values(specs)) {
-  if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) {
-    limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
+if (request) {
+  const [reqSpec, reqContract] = request.split(':').reverse();
+  specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract));
+  if (specs.length === 0) {
+    console.error(`Error: Requested spec '${request}' not found in specs.json`);
+    process.exit(1);
   }
 }
 
+for (const { spec, contract, files, options = [] } of Object.values(specs)) {
+  limit(runCertora, spec, contract, files, [...options.split(' '), ...extraOptions]);
+}
+
 // Run certora, aggregate the output and print it at the end
 async function runCertora(spec, contract, files, options = []) {
   const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];
diff --git a/certora/specs.json b/certora/specs.json
index 25b9d1fb25a..228e85fe4f3 100644
--- a/certora/specs.json
+++ b/certora/specs.json
@@ -4,6 +4,16 @@
     "contract": "AccessControlHarness",
     "files": ["certora/harnesses/AccessControlHarness.sol"]
   },
+  {
+    "spec": "Ownable",
+    "contract": "OwnableHarness",
+    "files": ["certora/harnesses/OwnableHarness.sol"]
+  },
+  {
+    "spec": "Ownable2Step",
+    "contract": "Ownable2StepHarness",
+    "files": ["certora/harnesses/Ownable2StepHarness.sol"]
+  },
   {
     "spec": "ERC20",
     "contract": "ERC20PermitHarness",
@@ -30,5 +40,10 @@
       "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
       "--optimistic_loop"
     ]
+  },
+  {
+    "spec": "Initializable",
+    "contract": "InitializableHarness",
+    "files": ["certora/harnesses/InitializableHarness.sol"]
   }
 ]
diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec
index 170d56fd403..8e8f6ac9d86 100644
--- a/certora/specs/AccessControl.spec
+++ b/certora/specs/AccessControl.spec
@@ -44,22 +44,27 @@ rule onlyGrantCanGrant(env e, bytes32 role, address account) {
 rule grantRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    grantRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    grantRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == true && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -70,22 +75,27 @@ rule grantRoleEffect(env e) {
 rule revokeRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    revokeRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -96,19 +106,24 @@ rule revokeRoleEffect(env e) {
 rule renounceRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    renounceRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> account2 == e.msg.sender;
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> account == e.msg.sender;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec
new file mode 100644
index 00000000000..1ba8d54e81f
--- /dev/null
+++ b/certora/specs/Initializable.spec
@@ -0,0 +1,165 @@
+import "helpers.spec"
+
+methods {
+    // initialize, reinitialize, disable
+    initialize()        envfree
+    reinitialize(uint8) envfree
+    disable()           envfree
+
+    nested_init_init()            envfree
+    nested_init_reinit(uint8)       envfree
+    nested_reinit_init(uint8)       envfree
+    nested_reinit_reinit(uint8,uint8) envfree
+
+    // view
+    version()      returns uint8 envfree
+    initializing() returns bool  envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition isUninitialized() returns bool = version() == 0;
+definition isInitialized()   returns bool = version() > 0;
+definition isDisabled()      returns bool = version() == 255;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution.    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant notInitializing()
+    !initializing()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: The version cannot decrease & disable state is irrevocable.                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increasingVersion(env e) {
+    uint8 versionBefore = version();
+    bool disabledBefore = isDisabled();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert versionBefore <= version(), "_initialized must only increase";
+    assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize a contract that is already initialized.                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeTwice() {
+    require isInitialized();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract must only be initialized once";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize once disabled.                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeOnceDisabled() {
+    require isDisabled();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot reinitialize once disabled.                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotReinitializeOnceDisabled() {
+    require isDisabled();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot nest initializers (after construction).                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotNestInitializers_init_init() {
+    nested_init_init@withrevert();
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_init_reinit(uint8 m) {
+    nested_init_reinit@withrevert(m);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_init(uint8 n) {
+    nested_reinit_init@withrevert(n);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
+    nested_reinit_reinit@withrevert(n, m);
+    assert lastReverted, "nested initializers";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Initialize correctly sets the version.                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule initializeEffects() {
+    requireInvariant notInitializing();
+
+    bool isUninitializedBefore = isUninitialized();
+
+    initialize@withrevert();
+    bool success = !lastReverted;
+
+    assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
+    assert success => version() == 1,         "initialize must set version() to 1";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Reinitialize correctly sets the version.                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule reinitializeEffects() {
+    requireInvariant notInitializing();
+
+    uint8 versionBefore = version();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+    bool success = !lastReverted;
+
+    assert success <=> versionBefore < n, "can only reinitialize to a latter versions";
+    assert success => version() == n,     "reinitialize must set version() to n";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Can disable.                                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule disableEffect() {
+    requireInvariant notInitializing();
+
+    disable@withrevert();
+    bool success = !lastReverted;
+
+    assert success,      "call to _disableInitializers failed";
+    assert isDisabled(), "disable state not set";
+}
diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec
new file mode 100644
index 00000000000..48bd84d13fc
--- /dev/null
+++ b/certora/specs/Ownable.spec
@@ -0,0 +1,78 @@
+import "helpers.spec"
+import "methods/IOwnable.spec"
+
+methods {
+    restricted()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership changes ownership                                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
+    assert success => owner() == newOwner, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner                                                           │
+
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership can only change in specific ways                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e, method f) {
+    address oldCurrent = owner();
+
+    calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+
+    // If owner changes, must be either transferOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector)
+    );
+}
diff --git a/certora/specs/Ownable2Step.spec b/certora/specs/Ownable2Step.spec
new file mode 100644
index 00000000000..70c520a03f5
--- /dev/null
+++ b/certora/specs/Ownable2Step.spec
@@ -0,0 +1,108 @@
+import "helpers.spec"
+import "methods/IOwnable2Step.spec"
+
+methods {
+    restricted()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: transferOwnership sets the pending owner                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule transferOwnership(env e) {
+    require nonpayable(e);
+
+    address newOwner;
+    address current = owner();
+
+    transferOwnership@withrevert(e, newOwner);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == newOwner, "pending owner not set";
+    assert success => owner() == current, "current owner changed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceOwnership removes the owner and the pendingOwner                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceOwnership(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    renounceOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == current, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == 0, "owner not cleared";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: acceptOwnership changes owner and reset pending owner                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule acceptOwnership(env e) {
+
+    require nonpayable(e);
+
+    address current = owner();
+    address pending = pendingOwner();
+
+    acceptOwnership@withrevert(e);
+    bool success = !lastReverted;
+
+    assert success <=> e.msg.sender == pending, "unauthorized caller";
+    assert success => pendingOwner() == 0, "pending owner not cleared";
+    assert success => owner() == pending, "owner not transferred";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Access control: only current owner can call restricted functions                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
+    require nonpayable(e);
+
+    address current = owner();
+
+    calldataarg args;
+    restricted@withrevert(e, args);
+
+    assert !lastReverted <=> e.msg.sender == current, "access control failed";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: ownership and pending ownership can only change in specific ways                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule ownerOrPendingOwnerChange(env e, method f) {
+    address oldCurrent = owner();
+    address oldPending = pendingOwner();
+
+    calldataarg args;
+    f(e, args);
+
+    address newCurrent = owner();
+    address newPending = pendingOwner();
+
+    // If owner changes, must be either acceptOwnership or renounceOwnership
+    assert oldCurrent != newCurrent => (
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
+    );
+
+    // If pending changes, must be either acceptance or reset
+    assert oldPending != newPending => (
+        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == transferOwnership(address).selector) ||
+        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
+        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
+    );
+}
diff --git a/certora/specs/methods/IOwnable.spec b/certora/specs/methods/IOwnable.spec
new file mode 100644
index 00000000000..cfa15f95ff1
--- /dev/null
+++ b/certora/specs/methods/IOwnable.spec
@@ -0,0 +1,5 @@
+methods {
+    owner() returns (address) envfree
+    transferOwnership(address)
+    renounceOwnership()
+}
diff --git a/certora/specs/methods/IOwnable2Step.spec b/certora/specs/methods/IOwnable2Step.spec
new file mode 100644
index 00000000000..c8e671d272c
--- /dev/null
+++ b/certora/specs/methods/IOwnable2Step.spec
@@ -0,0 +1,7 @@
+methods {
+    owner() returns (address) envfree
+    pendingOwner() returns (address) envfree
+    transferOwnership(address)
+    acceptOwnership()
+    renounceOwnership()
+}