diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf
index 5caa384..658f55c 100644
--- a/certora/confs/Marketplace.conf
+++ b/certora/confs/Marketplace.conf
@@ -1,5 +1,6 @@
 {
     "files": [
+        "certora/harness/MarketplaceHarness.sol",
         "contracts/Marketplace.sol",
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
@@ -11,7 +12,7 @@
     ],
     "msg": "Verifying Marketplace",
     "rule_sanity": "basic",
-    "verify": "Marketplace:certora/specs/Marketplace.spec",
+    "verify": "MarketplaceHarness:certora/specs/Marketplace.spec",
     "optimistic_loop": true,
     "loop_iter": "3",
     "optimistic_hashing": true,
diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
new file mode 100644
index 0000000..272fe9c
--- /dev/null
+++ b/certora/harness/MarketplaceHarness.sol
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.23;
+
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IGroth16Verifier} from "../../contracts/Groth16.sol";
+import {MarketplaceConfig} from "../../contracts/Configuration.sol";
+import {Marketplace} from "../../contracts/Marketplace.sol";
+import {RequestId} from "../../contracts/Requests.sol";
+
+contract MarketplaceHarness is Marketplace {
+    constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
+
+    function requestContext(RequestId requestId) public returns (Marketplace.RequestContext memory) {
+        return _requestContexts[requestId];
+    }
+}
+
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index af013bc..75dc1eb 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -1,5 +1,9 @@
 using ERC20A as Token;
 
+methods {
+    function Token.balanceOf(address) external returns (uint256) envfree;
+}
+
 /*--------------------------------------------
 |              Ghosts and hooks              |
 --------------------------------------------*/
@@ -24,6 +28,26 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25
     totalSent = totalSent + defaultValue - defaultValue_old;
 }
 
+function canCancelRequest(method f) returns bool {
+    return f.selector == sig:withdrawFunds(Marketplace.RequestId).selector;
+}
+
+function canStartRequest(method f) returns bool {
+    return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
+}
+
+function canFinishRequest(method f) returns bool {
+    return f.selector == sig:freeSlot(Marketplace.SlotId).selector;
+}
+
+function canFailRequest(method f) returns bool {
+    return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector || 
+        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
+}
+
+invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
+    to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/
@@ -56,3 +80,51 @@ rule totalSentCannotDecrease(env e, method f) {
 
     assert total_after >= total_before;
 }
+
+rule allowedRequestStateChanges(env e, method f) {
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New;
+}
+
+rule functionsCausingRequestStateChanges(env e, method f) {
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    // RequestState.New -> RequestState.Started
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
+
+    // RequestState.Started -> RequestState.Finished
+    assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Finished => canFinishRequest(f);
+
+    // RequestState.Started -> RequestState.Failed
+    assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Failed => canFailRequest(f);
+
+    // RequestState.New -> RequestState.Cancelled
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
+}
+
+rule finishedRequestCannotBeStartedAgain(env e, method f) {
+
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    require requestStateBefore == Marketplace.RequestState.Finished;
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    assert requestStateBefore == requestStateAfter;
+}
diff --git a/contracts/Marketplace.sol b/contracts/Marketplace.sol
index 4ea1b6f..e6763ce 100644
--- a/contracts/Marketplace.sol
+++ b/contracts/Marketplace.sol
@@ -19,7 +19,7 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
   MarketplaceConfig private _config;
 
   mapping(RequestId => Request) private _requests;
-  mapping(RequestId => RequestContext) private _requestContexts;
+  mapping(RequestId => RequestContext) internal _requestContexts;
   mapping(SlotId => Slot) internal _slots;
 
   MarketplaceTotals internal _marketplaceTotals;