diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 432c119..66af58c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -139,7 +139,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install Certora CLI
-        run: pip3 install certora-cli==5.0.5
+        run: pip3 install certora-cli==7.17.2
 
       - name: Install Solidity
         run: |
diff --git a/certora/confs/RewardsStreamerMP.conf b/certora/confs/RewardsStreamerMP.conf
index 4123e8d..15a06b5 100644
--- a/certora/confs/RewardsStreamerMP.conf
+++ b/certora/confs/RewardsStreamerMP.conf
@@ -1,9 +1,15 @@
 {
-  "files": ["src/RewardsStreamerMP.sol"],
+  "files": [
+    "src/RewardsStreamerMP.sol",
+    "certora/helpers/ERC20A.sol"
+  ],
+  "link" : [
+    "RewardsStreamerMP:STAKING_TOKEN=ERC20A",
+    "RewardsStreamerMP:REWARD_TOKEN=ERC20A"
+  ],
   "msg": "Verifying RewardsStreamerMP.sol",
   "rule_sanity": "basic",
   "verify": "RewardsStreamerMP:certora/specs/RewardsStreamerMP.spec",
-  "wait_for_results": "all",
   "optimistic_loop": true,
   "loop_iter": "3",
   "packages": [
diff --git a/certora/helpers/ERC20A.sol b/certora/helpers/ERC20A.sol
new file mode 100644
index 0000000..d28333f
--- /dev/null
+++ b/certora/helpers/ERC20A.sol
@@ -0,0 +1,10 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.26;
+
+import { ERC20 } from "@openzeppelin/contracts/token/ERC20/ERC20.sol";
+
+contract ERC20A is ERC20 {
+   constructor(string memory name_, string memory symbol_) ERC20(name_, symbol_) {}
+}
+
diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec
index 4be8f4d..0de959e 100644
--- a/certora/specs/RewardsStreamerMP.spec
+++ b/certora/specs/RewardsStreamerMP.spec
@@ -1,3 +1,16 @@
-rule test {
-    assert true;
+using ERC20A as staked;
+
+methods {
+    function totalStaked() external returns (uint256) envfree;
 }
+
+ghost mathint sumOfBalances {
+	init_state axiom sumOfBalances == 0;
+}
+
+hook Sstore users[KEY address account].stakedBalance uint256 newValue (uint256 oldValue) {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+invariant sumOfBalancesIsTotalStaked()
+  sumOfBalances == to_mathint(totalStaked());