diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index e849a64..a420003 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -3,8 +3,6 @@ import "./shared.spec";
 using ERC20A as Token;
 
 methods {
-    function Token.balanceOf(address) external returns (uint256) envfree;
-    function Token.totalSupply() external returns (uint256) envfree;
     function publicPeriodEnd(Periods.Period) external returns (Marketplace.Timestamp) envfree;
     function generateSlotId(Marketplace.RequestId, uint64) external returns (Marketplace.SlotId) envfree;
 }
@@ -13,18 +11,6 @@ methods {
 |              Ghosts and hooks              |
 --------------------------------------------*/
 
-ghost mathint sumOfBalances {
-    init_state axiom sumOfBalances == 0;
-}
-
-hook Sload uint256 balance Token._balances[KEY address addr] {
-    require sumOfBalances >= to_mathint(balance);
-}
-
-hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
-    sumOfBalances = sumOfBalances - oldValue + newValue;
-}
-
 ghost Marketplace.Timestamp lastBlockTimestampGhost;
 
 hook TIMESTAMP uint v {
@@ -147,9 +133,6 @@ function slotAttributesAreConsistent(env e, Marketplace.SlotId slotId) {
 |                 Invariants                 |
 --------------------------------------------*/
 
-invariant totalSupplyIsSumOfBalances()
-    to_mathint(Token.totalSupply()) == sumOfBalances;
-
 invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
     currentContract.requestState(e, requestId) == Marketplace.RequestState.Started => to_mathint(currentContract.getRequest(e, requestId).ask.slots) - slotsFilledGhost[requestId] <= to_mathint(currentContract.getRequest(e, requestId).ask.maxSlotLoss);