diff --git a/certora/certora.conf b/certora/confs/StakeManager.conf
similarity index 50%
rename from certora/certora.conf
rename to certora/confs/StakeManager.conf
index fcb2aeb..3291acf 100644
--- a/certora/certora.conf
+++ b/certora/confs/StakeManager.conf
@@ -1,9 +1,16 @@
 {
-  "files": ["contracts/StakeManager.sol"],
+  "files": 
+    ["contracts/StakeManager.sol",
+      "certora/helpers/ERC20A.sol"
+    ],
+  "link" : [
+    "StakeManager:stakedToken=ERC20A"
+  ],
   "msg": "Verifying StakeManager.sol",
   "rule_sanity": "basic",
   "verify": "StakeManager:certora/specs/StakeManager.spec",
-  "wait_for_results": "all",
+  "optimistic_loop": true,
+  "loop_iter": "3",
   "packages": [
     "@openzeppelin=lib/openzeppelin-contracts"
   ]
diff --git a/certora/confs/StakeVault.conf b/certora/confs/StakeVault.conf
new file mode 100644
index 0000000..c70040e
--- /dev/null
+++ b/certora/confs/StakeVault.conf
@@ -0,0 +1,22 @@
+{
+  "files": [
+    "contracts/StakeManager.sol",
+    "contracts/StakeVault.sol",
+    "certora/helpers/ERC20A.sol"
+  ],
+  "link" : [
+    "StakeVault:STAKED_TOKEN=ERC20A",
+    "StakeManager:stakedToken=ERC20A",
+    "StakeVault:stakeManager=StakeManager"
+  ],
+  "msg": "Verifying StakeVault.sol",
+  "rule_sanity": "basic",
+  "verify": "StakeVault:certora/specs/StakeVault.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "packages": [
+    "@openzeppelin=lib/openzeppelin-contracts"
+  ]
+}
+
+
diff --git a/certora/helpers/ERC20A.sol b/certora/helpers/ERC20A.sol
new file mode 100644
index 0000000..cabfa08
--- /dev/null
+++ b/certora/helpers/ERC20A.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.19;
+
+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/StakeManager.spec b/certora/specs/StakeManager.spec
index c1f7813..79bef19 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -1,4 +1,50 @@
-
-rule shouldPass {
-  assert true;
+using ERC20A as staked;
+methods {
+  function staked.balanceOf(address) external returns (uint256) envfree;
+}
+
+function isMigrationfunction(method f) returns bool {
+  return  f.selector == sig:leave().selector ||
+          f.selector == sig:migrate(address,StakeManager.Account).selector ||
+          f.selector == sig:migrate().selector;
+}
+
+/*  assume that migration is zero, causing the verification to take into account only
+ cases where it is zero. specifically no externall call to the migration contract */
+function simplification() {
+  require currentContract.migration == 0;
+}
+
+
+rule reachability(method f)
+{
+  calldataarg args;
+  env e;
+  f(e,args);
+  satisfy true;
+}
+
+/**
+@title when there is no migration - some functions must revert.
+Other function should have non reverting cases
+**/
+rule revertsWhenNoMigration(method f) {
+  calldataarg args;
+  env e;
+  require currentContract.migration == 0;
+  f@withrevert(e,args);
+  bool reverted = lastReverted;
+  if (!isMigrationfunction(f))
+    satisfy !reverted;
+  assert isMigrationfunction(f) => reverted;
+}
+
+rule whoChangeERC20Balance(  method f ) filtered { f -> f.contract != staked }
+{
+  address user;
+  uint256 before = staked.balanceOf(user);
+  calldataarg args;
+  env e;
+  f(e,args);
+  assert before == staked.balanceOf(user);
 }
diff --git a/certora/specs/StakeVault.spec b/certora/specs/StakeVault.spec
new file mode 100644
index 0000000..5532ebd
--- /dev/null
+++ b/certora/specs/StakeVault.spec
@@ -0,0 +1,28 @@
+using ERC20A as staked;
+using StakeManager as stakeManager;
+methods {
+  function ERC20A.balanceOf(address) external returns (uint256) envfree;
+}
+
+/*  assume that migration is zero, causing to ignore cases where it is not zero */
+function simplification() {
+  require stakeManager.migration == 0;
+}
+
+rule reachability(method f){
+  calldataarg args;
+  env e;
+  f(e,args);
+  satisfy true;
+}
+
+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/contracts/StakeVault.sol b/contracts/StakeVault.sol
index 0b5ddbd..63c0b0b 100644
--- a/contracts/StakeVault.sol
+++ b/contracts/StakeVault.sol
@@ -20,7 +20,7 @@ contract StakeVault is Ownable {
 
     StakeManager private stakeManager;
 
-    ERC20 private immutable STAKED_TOKEN;
+    ERC20 public immutable STAKED_TOKEN;
 
     event Staked(address from, address to, uint256 _amount, uint256 time);
 
diff --git a/package.json b/package.json
index 30fe663..fe9df59 100644
--- a/package.json
+++ b/package.json
@@ -20,9 +20,11 @@
   "scripts": {
     "clean": "rm -rf cache out",
     "lint": "pnpm lint:sol && pnpm prettier:check",
-    "verify": "certoraRun certora/certora.conf",
+    "verify": "pnpm verify:stake_vault && pnpm verify:stake_manager",
     "lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol",
     "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
-    "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"
+    "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore",
+    "verify:stake_vault": "certoraRun certora/confs/StakeVault.conf",
+    "verify:stake_manager": "certoraRun certora/confs/StakeManager.conf"
   }
 }