diff --git a/certora/confs/StakeVault.conf b/certora/confs/StakeVault.conf
new file mode 100644
index 0000000..579be3c
--- /dev/null
+++ b/certora/confs/StakeVault.conf
@@ -0,0 +1,22 @@
+{
+  "files": [
+    "src/RewardsStreamerMP.sol",
+    "src/StakeVault.sol",
+    "certora/helpers/ERC20A.sol"
+  ],
+  "link" : [
+    "StakeVault:STAKING_TOKEN=ERC20A",
+    "RewardsStreamerMP:STAKING_TOKEN=ERC20A",
+    "RewardsStreamerMP:REWARD_TOKEN=ERC20A",
+    "StakeVault:stakeManager=RewardsStreamerMP"
+  ],
+  "msg": "Verifying StakeVault.sol",
+  "rule_sanity": "basic",
+  "verify": "StakeVault:certora/specs/StakeVault.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "packages": [
+    "forge-std=lib/forge-std/src",
+    "@openzeppelin=lib/openzeppelin-contracts"
+  ]
+}
diff --git a/certora/specs/RewardsStreamerMP.spec b/certora/specs/RewardsStreamerMP.spec
index db7e557..c5ef8cf 100644
--- a/certora/specs/RewardsStreamerMP.spec
+++ b/certora/specs/RewardsStreamerMP.spec
@@ -1,7 +1,11 @@
-using RewardsStreamerMP as streamer;
+import "./shared.spec";
+
 using ERC20A as staked;
 
 methods {
+    function ERC20A.balanceOf(address) external returns (uint256) envfree;
+    function ERC20A.allowance(address, address) external returns(uint256) envfree;
+    function ERC20A.totalSupply() external returns(uint256) envfree;
     function totalStaked() external returns (uint256) envfree;
     function accounts(address) external returns (uint256, uint256, uint256, uint256, uint256, uint256) envfree;
     function lastMPUpdatedTime() external returns (uint256) envfree;
@@ -29,12 +33,6 @@ function getAccountMP(address account) returns uint256 {
     return accountMP;
 }
 
-function getAccountStakedBalance(address account) returns uint256 {
-    uint256 stakedBalance;
-    stakedBalance, _, _, _, _, _ = streamer.accounts(account);
-    return stakedBalance;
-}
-
 function getAccountLockUntil(address account) returns uint256 {
     uint256 lockUntil;
     _, _, _, _, _, lockUntil = streamer.accounts(account);
diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec
new file mode 100644
index 0000000..37d6690
--- /dev/null
+++ b/certora/specs/StakeVault.spec
@@ -0,0 +1,76 @@
+import "./shared.spec";
+
+using ERC20A as staked;
+using RewardsStreamerMP as stakeManager;
+
+methods {
+  function ERC20A.balanceOf(address) external returns (uint256) envfree;
+  function ERC20A.allowance(address, address) external returns(uint256) envfree;
+  function ERC20A.totalSupply() external returns(uint256) envfree;
+  function RewardsStreamerMP.accounts(address) external returns(uint256, uint256, uint256, uint256, uint256, uint256) envfree;
+  function _.owner() external => DISPATCHER(true);
+  function _.transfer(address, uint256) external => DISPATCHER(true);
+}
+
+// check that the ERC20.balanceOf(vault) is >= to StakeManager.accounts[a].balance
+invariant accountBalanceVsERC20Balance()
+  staked.balanceOf(currentContract) >= getAccountStakedBalance(currentContract)
+  { preserved with (env e) {
+      // the sender can't be the vault otherwise it can transfer tokens
+      require e.msg.sender != currentContract;
+      // nobody has allowance to spend the tokens of the vault
+      require staked.allowance(currentContract, e.msg.sender) == 0;
+      // if it's a generic transfer to the vault, it can't overflow
+      require staked.balanceOf(currentContract) + staked.balanceOf(e.msg.sender) <= to_mathint(staked.totalSupply());
+      // if it's a transfer from the StakeManager to the vault as reward address, it can't overflow
+      require staked.balanceOf(currentContract) + staked.balanceOf(stakeManager) <= to_mathint(staked.totalSupply());
+    }
+
+    // the next blocked is run instead of the general one if the current function is staked.transferFrom.
+    // if it's a transferFrom, we don't have the from in the first preserved block to check for an overflow
+    preserved staked.transferFrom(address from, address to, uint256 amount) with (env e) {
+      // if the msg.sender is the vault than it would be able to move tokens.
+      // it would be possible only if the Vault contract called the ERC20.transferFrom.
+      require e.msg.sender != currentContract;
+      // no one has allowance to move tokens owned by the vault
+      require staked.allowance(currentContract, e.msg.sender) == 0;
+      require staked.balanceOf(from) + staked.balanceOf(to) <= to_mathint(staked.totalSupply());
+    }
+
+    preserved stake(uint256 amount, uint256 duration) with (env e) {
+
+      require e.msg.sender != currentContract;
+
+      require staked.balanceOf(currentContract) + staked.balanceOf(e.msg.sender) + staked.balanceOf(stakeManager) <= to_mathint(staked.totalSupply());
+    }
+
+    preserved stake(uint256 amount, uint256 duration, address from) with (env e) {
+      require e.msg.sender != currentContract;
+      require from != currentContract;
+      require staked.balanceOf(currentContract) + staked.balanceOf(from) + staked.balanceOf(stakeManager) <= to_mathint(staked.totalSupply());
+    }
+  }
+
+
+rule reachability(method f) {
+  calldataarg args;
+  env e;
+  f(e,args);
+  satisfy true;
+}
+
+/*
+  The rule below is commented out as it's merely used to easily have the
+  prover find all functions that change balances.
+
+rule whoChangeERC20Balance(method f)
+{
+  simplification();
+  address user;
+  uint256 before = staked.balanceOf(user);
+  calldataarg args;
+  env e;
+  f(e,args);
+  assert before == staked.balanceOf(user);
+}
+*/
diff --git a/certora/specs/shared.spec b/certora/specs/shared.spec
new file mode 100644
index 0000000..45e1e52
--- /dev/null
+++ b/certora/specs/shared.spec
@@ -0,0 +1,8 @@
+using RewardsStreamerMP as streamer;
+
+function getAccountStakedBalance(address account) returns uint256 {
+    uint256 stakedBalance;
+    stakedBalance, _, _, _, _, _ = streamer.accounts(account);
+    return stakedBalance;
+}
+