diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index eab36199..100601d2 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -100,6 +100,22 @@ invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId,
 invariant cantBeMissedIfInPeriod(MarketplaceHarness.SlotId slotId, Periods.Period period)
     lastBlockTimestampGhost <= publicPeriodEnd(period) => !_missingMirror[slotId][period];
 
+// STATUS - in progress (fails on constructor state due to a strange behaviour in the tool)
+// _marketplaceTotals.received - _marketplaceTotals.sent == tokenBalanceOfContract
+// https://prover.certora.com/output/3106/4e6cac8055ac45bb92840e14d9b095eb/?anonymousKey=655a42ca6306a023db78914d5a188d8ec2882771
+invariant totalSentIsLessThanOrEqualTotalReceived()
+    totalReceived - totalSent <= to_mathint(Token.balanceOf(currentContract))
+    {
+        preserved fillSlot(MarketplaceHarness.RequestId requestId, uint256 slotIndex, MarketplaceHarness.Groth16Proof proof) with (env e2) {
+            require e2.msg.sender != currentContract;
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+        preserved requestStorage(MarketplaceHarness.Request request) with (env e3) {
+            require e3.msg.sender != currentContract;
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+    }
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/