diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec
index 21a033585..6b9b55de5 100644
--- a/certora/specs/ERC20.spec
+++ b/certora/specs/ERC20.spec
@@ -23,11 +23,11 @@ ghost mathint sumOfBalances {
 // overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an 
 // already used address (or upgraded from corrupted state).
 // We restrict such behavior by making sure no balance is greater than the sum of balances.
-hook Sload uint256 balance _balances[KEY address addr] STORAGE {
+hook Sload uint256 balance _balances[KEY address addr] {
     require sumOfBalances >= to_mathint(balance);
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     sumOfBalances = sumOfBalances - oldValue + newValue;
 }
 
diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec
index bad4c4737..e5d5546f2 100644
--- a/certora/specs/ERC721.spec
+++ b/certora/specs/ERC721.spec
@@ -113,7 +113,7 @@ ghost mapping(address => mathint) _ownedByUser {
     init_state axiom forall address a. _ownedByUser[a] == 0;
 }
 
-hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE {
+hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
     _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
     _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
     _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
@@ -132,13 +132,13 @@ ghost mapping(address => mathint) _balances {
     init_state axiom forall address a. _balances[a] == 0;
 }
 
-hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE {
+hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
     _supply = _supply - oldValue + newValue;
 }
 
 // TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add
 // many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved.
-hook Sload uint256 value _balances[KEY address user] STORAGE {
+hook Sload uint256 value _balances[KEY address user] {
     require _balances[user] == to_mathint(value);
 }
 
diff --git a/requirements.txt b/requirements.txt
index bdea09aa8..60f7546c3 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1 +1 @@
-certora-cli==4.13.1
+certora-cli==7.3.0