diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 0c1d939..49e2499 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -191,6 +191,22 @@ invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotI
     currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
         currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
 
+// 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                 |
 --------------------------------------------*/