diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index 79bef19..e0da6c9 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -1,6 +1,7 @@
 using ERC20A as staked;
 methods {
   function staked.balanceOf(address) external returns (uint256) envfree;
+  function stakeSupply() external returns (uint256) envfree;
 }
 
 function isMigrationfunction(method f) returns bool {
@@ -15,6 +16,17 @@ function simplification() {
   require currentContract.migration == 0;
 }
 
+ghost mathint sumOfBalances /* sigma account[u].balance forall u */ {
+	init_state axiom sumOfBalances == 0;
+}
+
+hook Sstore accounts[KEY address addr].balance uint256 newValue (uint256 oldValue) STORAGE {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
+invariant sumOfBalancesIsStakeSupply()
+      sumOfBalances == to_mathint(stakeSupply());
+
 
 rule reachability(method f)
 {