diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml
new file mode 100644
index 00000000..6f621104
--- /dev/null
+++ b/.github/workflows/certora-prover.yml
@@ -0,0 +1,35 @@
+on:
+  pull_request:
+    branches:
+      - dev
+  workflow_dispatch:
+
+jobs:
+  certora_run_submission:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+      id-token: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - name: Submit verification jobs to Certora Prover
+        uses: Certora/certora-run-action@v2
+        with:
+          # Add your configurations as lines, each line is separated.
+          # Specify additional options for each configuration by adding them after the configuration.
+          configurations: |-
+            certora/confs/ECDSATableCalculator.conf
+            certora/confs/AVSRegistrarWithAllowlist.conf
+            certora/confs/BN254TableCalculator.conf
+            certora/confs/AVSRegistrarWithSocket.conf
+            certora/confs/AVSRegistrar.conf
+          solc-versions: 0.8.27
+          job-name: "Verified Rules"
+          certora-key: ${{ secrets.CERTORAKEY }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/certora/confs/AVSRegistrar.conf b/certora/confs/AVSRegistrar.conf
new file mode 100644
index 00000000..5cb3c2f6
--- /dev/null
+++ b/certora/confs/AVSRegistrar.conf
@@ -0,0 +1,23 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarAsIdentifier.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarAsIdentifier:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarAsIdentifier:allocationManager=AllocationManager"
+  ],
+  "msg": "AVSRegistrarAsIdentifier rules",
+  "server": "production",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarAsIdentifier.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarAsIdentifier:certora/specs/AVSRegistrar.spec"
+}
diff --git a/certora/confs/AVSRegistrarWithAllowlist.conf b/certora/confs/AVSRegistrarWithAllowlist.conf
new file mode 100644
index 00000000..5b54835f
--- /dev/null
+++ b/certora/confs/AVSRegistrarWithAllowlist.conf
@@ -0,0 +1,34 @@
+{
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarWithAllowlist.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarWithAllowlist:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarWithAllowlist:allocationManager=AllocationManager"
+  ],
+  "packages": [
+    "husky=node_modules/husky",
+    "@commitlint/cli=node_modules/@commitlint/cli",
+    "@commitlint/config-conventional=node_modules/@commitlint/config-conventional",
+    "forge-std=lib/forge-std/src",
+    "ds-test=lib/ds-test/src",
+    "@openzeppelin=lib/openzeppelin-contracts",
+    "openzeppelin-contracts-upgradeable=lib/openzeppelin-contracts-upgradeable",
+    "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable",
+    "eigenlayer-contracts=lib/eigenlayer-contracts"
+  ],
+
+  "msg": "AVSRegistrarWithAllowlist rules",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarWithAllowlist.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarWithAllowlist:certora/specs/AVSRegistrarWithAllowlist.spec",
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf"
+}
diff --git a/certora/confs/AVSRegistrarWithSocket.conf b/certora/confs/AVSRegistrarWithSocket.conf
new file mode 100644
index 00000000..92c0d10a
--- /dev/null
+++ b/certora/confs/AVSRegistrarWithSocket.conf
@@ -0,0 +1,22 @@
+{
+  "files": [
+    "src/middlewareV2/registrar/presets/AVSRegistrarWithSocket.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol"
+  ],
+  "link": [
+    "AVSRegistrarWithSocket:keyRegistrar=KeyRegistrar",
+    "AVSRegistrarWithSocket:allocationManager=AllocationManager"
+  ],
+  "msg": "AVSRegistrarWithSocket rules",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "src/middlewareV2/registrar/presets/AVSRegistrarWithSocket.sol",
+        "num_mutants": 5
+      }
+    ]
+  },
+  "verify": "AVSRegistrarWithSocket:certora/specs/AVSRegistrarWithSocket.spec",
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf"
+}
diff --git a/certora/confs/BN254TableCalculator.conf b/certora/confs/BN254TableCalculator.conf
new file mode 100644
index 00000000..2af1d0f5
--- /dev/null
+++ b/certora/confs/BN254TableCalculator.conf
@@ -0,0 +1,17 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/tableCalculator/BN254TableCalculator.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/DelegationManager.sol"
+  ],
+  "link": [
+    "BN254TableCalculator:keyRegistrar=KeyRegistrar",
+    "BN254TableCalculator:allocationManager=AllocationManager",
+    "AllocationManager:delegation=DelegationManager"
+  ],
+  "optimistic_hashing": true,
+  "msg": "sanity_BN254TableCalculator",
+  "verify": "BN254TableCalculator:certora/specs/BN254TableCalculator.spec"
+}
diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf
new file mode 100644
index 00000000..aecb1040
--- /dev/null
+++ b/certora/confs/BaseConfForInheritance.conf
@@ -0,0 +1,31 @@
+{
+  "assert_autofinder_success": true,
+  "global_timeout": "7200",
+  "loop_iter": "2",
+  "optimistic_loop": true,
+  "solc": "solc",
+  "solc_optimize": "200",
+  "solc_via_ir": false,
+  "server": "production",
+  "packages": [
+    "husky=node_modules/husky",
+    "@commitlint/cli=node_modules/@commitlint/cli",
+    "@commitlint/config-conventional=node_modules/@commitlint/config-conventional",
+    "forge-std=lib/forge-std/src",
+    "ds-test=lib/ds-test/src",
+    "@openzeppelin=lib/openzeppelin-contracts",
+    "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable",
+    "openzeppelin-contracts-upgradeable=lib/openzeppelin-contracts-upgradeable",
+    "eigenlayer-contracts=lib/eigenlayer-contracts"
+  ],
+  "prover_args": [
+    "-verifyCache",
+    "-verifyTACDumps",
+    "-testMode",
+    "-checkRuleDigest",
+    "-callTraceHardFail on",
+    "-allowArrayLengthUpdates true",
+    "-linearInvariantBound 4"
+  ],
+  "prover_version": "master"
+}
diff --git a/certora/confs/ECDSATableCalculator.conf b/certora/confs/ECDSATableCalculator.conf
new file mode 100644
index 00000000..36c7f763
--- /dev/null
+++ b/certora/confs/ECDSATableCalculator.conf
@@ -0,0 +1,16 @@
+{
+  "override_base_config": "certora/confs/BaseConfForInheritance.conf",
+  "files": [
+    "src/middlewareV2/tableCalculator/ECDSATableCalculator.sol",
+    "lib/eigenlayer-contracts/src/contracts/permissions/KeyRegistrar.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/AllocationManager.sol",
+    "lib/eigenlayer-contracts/src/contracts/core/DelegationManager.sol"
+  ],
+  "link": [
+    "ECDSATableCalculator:keyRegistrar=KeyRegistrar",
+    "ECDSATableCalculator:allocationManager=AllocationManager",
+    "AllocationManager:delegation=DelegationManager"
+  ],
+  "msg": "sanity_ECDSATableCalculator",
+  "verify": "ECDSATableCalculator:certora/specs/ECDSATableCalculator.spec"
+}
diff --git a/certora/specs/AVSRegistrar.spec b/certora/specs/AVSRegistrar.spec
new file mode 100644
index 00000000..8c7fa8e5
--- /dev/null
+++ b/certora/specs/AVSRegistrar.spec
@@ -0,0 +1,72 @@
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+
+methods{
+    // function _.getBN254Key(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    // function _.merkleizeKeccak(bytes32[] memory) internal => NONDET;
+    // function _getOperatorWeights(BN254TableCalculator.OperatorSet calldata) internal returns (address[] memory, uint256[][] memory) => returnEmptyWeights();
+
+}
+
+/*
+ * msg.sender != address(allocationManager) => revert
+ *
+ * What it means: 
+ * The registerOperator function can only be called by the AllocationManager contract address, and any call from a different address must revert.
+ * 
+ * Why it should hold: The function has the onlyAllocationManager modifier which enforces this access control. This is a critical security boundary that ensures only the authorized AllocationManager can register operators for the AVS. 
+ *
+ * Possible consequences: Unauthorized operator registration, bypassing of allocation management logic, potential manipulation of operator sets, and violation of the intended protocol governance structure. 
+ */
+rule registerOperatorOnlyAllocationManager(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+    bytes data;
+
+    // call function under test
+    registerOperator@withrevert(e, operator, _, operatorSetIds, data);
+    bool registerOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert ((e.msg.sender != currentContract.allocationManager) => registerOperator_reverted), "msg.sender != address(allocationManager) => revert";
+}
+
+rule registerOperatorOnlyValidKeys(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+    bytes data;
+
+    KeyRegistrar.OperatorSet operatorSet;
+    require operatorSetIds.length > 0, "assume non empty operator set list, an empty list does not cause a revert";
+    require operatorSet.avs == currentContract.avs;
+    require operatorSet.id == operatorSetIds[0];
+
+    bool keyRegistered = currentContract.keyRegistrar.isRegistered(e, operatorSet, operator);
+
+    // call function under test
+    registerOperator@withrevert(e, operator, _, operatorSetIds, data);
+    bool registerOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert (!keyRegistered => registerOperator_reverted), "operator key not valid";
+}
+
+/*
+ * msg.sender != address(allocationManager) => revert
+ *
+ * What it means: Only the allocation manager contract can call the deregisterOperator function, any other caller should cause a revert
+ *
+ * Why it should hold: The function has the onlyAllocationManager modifier which enforces access control. This is a critical security boundary that ensures only the authorized allocation manager can deregister operators. The zero address is not a valid operator address and deregistering it would be a meaningless operation. This prevents invalid input and follows standard Ethereum patterns of rejecting zero addresses
+ *
+ * Possible consequences: Unauthorized deregistration of operators, disruption of AVS operations, potential griefing attacks where malicious actors can remove legitimate operators. Invalid state transitions, confusion in operator tracking, potential issues with downstream systems that assume valid operator addresses
+ */
+rule deregisterOperatorOnlyAllocationManager(env e) {
+    address operator;
+    uint32[] operatorSetIds;
+
+    // call function under test
+    deregisterOperator@withrevert(e, operator, _, operatorSetIds);
+    bool deregisterOperator_reverted = lastReverted;
+
+    // verify integrity
+    assert ((e.msg.sender != currentContract.allocationManager) => deregisterOperator_reverted), "msg.sender != address(allocationManager) => revert";
+}
diff --git a/certora/specs/AVSRegistrarWithAllowlist.spec b/certora/specs/AVSRegistrarWithAllowlist.spec
new file mode 100644
index 00000000..cfe356fe
--- /dev/null
+++ b/certora/specs/AVSRegistrarWithAllowlist.spec
@@ -0,0 +1,105 @@
+import "AVSRegistrar.spec";
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+use rule registerOperatorOnlyAllocationManager; 
+use rule registerOperatorOnlyValidKeys;
+use rule deregisterOperatorOnlyAllocationManager;
+
+
+/*
+ * _initialized > 0 => revert
+ *
+ * What it means: The initialize function must revert if the contract has already been initialized (_initialized > 0)
+ *
+ * Why it should hold: The initializer modifier should prevent re-initialization to maintain contract integrity and prevent ownership takeover after deployment
+ *
+ * Possible consequences: Ownership takeover, allowlist manipulation, complete compromise of access control system
+ */
+rule initialize_already_initialized_reverts(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    uint8 _initialized_before = currentContract._initialized;
+
+    // call function under test
+    initialize@withrevert(e, avs, admin);
+    bool initialize_reverted = lastReverted;
+
+    // verify integrity
+    assert ((_initialized_before > 0) => initialize_reverted), "_initialized > 0 => revert";
+}
+
+/*
+ * _initialized@after > _initialized@before
+ *
+ * What it means: After successful initialization, the _initialized state variable must increase from its previous value
+ *
+ * Why it should hold: The initializer modifier must properly mark the contract as initialized to prevent future re-initialization attempts
+ *
+ * Possible consequences: Re-initialization vulnerability, ownership takeover, state corruption
+ */
+rule initialize_sets_initialized_state(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    uint8 _initialized_before = currentContract._initialized;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    uint8 _initialized_after = currentContract._initialized;
+
+    // verify integrity
+    assert (_initialized_after > _initialized_before), "_initialized@after > _initialized@before";
+}
+
+/*
+ * _owner@after == admin
+ *
+ * What it means: When initialize is called with a  admin address, that address must become the contract owner
+ *
+ * Why it should hold: The purpose of initialization is to establish proper ownership, and the admin parameter should be set as the owner to enable access control
+ *
+ * Possible consequences: Broken access control, inability to manage allowlists, contract becomes non-functional
+ */
+rule initialize_admin_becomes_owner(env e) {
+    address admin;
+    address avs;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    address _owner_after = currentContract._owner;
+
+    // verify integrity
+    assert (_owner_after == admin), "_owner@after == admin";
+}
+
+/*
+ * _initializing@before == false && _initializing@after == false
+ *
+ * What it means: The _initializing flag should be false both before and after the initialize function execution
+ *
+ * Why it should hold: The initializer modifier should properly manage the _initializing flag to prevent reentrancy during initialization and ensure clean state transitions
+ *
+ * Possible consequences: Reentrancy attacks during initialization, inconsistent initialization state, potential for multiple simultaneous initializations
+ */
+rule initialize_initializing_flag_during_execution(env e) {
+    address admin;
+    address avs;
+
+    // assign all the 'before' variables
+    bool _initializing_before = currentContract._initializing;
+
+    // call function under test
+    initialize(e, avs, admin);
+
+    // assign all the 'after' variables
+    bool _initializing_after = currentContract._initializing;
+
+    // verify integrity
+    assert ((_initializing_before == false) && (_initializing_after == false)), "_initializing@before == false && _initializing@after == false";
+}
\ No newline at end of file
diff --git a/certora/specs/AVSRegistrarWithSocket.spec b/certora/specs/AVSRegistrarWithSocket.spec
new file mode 100644
index 00000000..cf8c88b9
--- /dev/null
+++ b/certora/specs/AVSRegistrarWithSocket.spec
@@ -0,0 +1,5 @@
+import "AVSRegistrar.spec";
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+use rule registerOperatorOnlyAllocationManager; 
+use rule registerOperatorOnlyValidKeys;
+use rule deregisterOperatorOnlyAllocationManager;
\ No newline at end of file
diff --git a/certora/specs/BN254TableCalculator.spec b/certora/specs/BN254TableCalculator.spec
new file mode 100644
index 00000000..e84fefa2
--- /dev/null
+++ b/certora/specs/BN254TableCalculator.spec
@@ -0,0 +1,24 @@
+import "Summaries/BN254-nondet.spec";
+import "Summaries/Math.spec";
+
+methods{
+    function _.isRegistered(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    function _.getBN254Key(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    function _.merkleizeKeccak(bytes32[] memory) internal => NONDET;
+    // function _getOperatorWeights(BN254TableCalculator.OperatorSet calldata) internal returns (address[] memory, uint256[][] memory) => returnEmptyWeights();
+
+    unresolved external in _._ => DISPATCH
+    [ 
+        KeyRegistrar.isRegistered(BN254TableCalculator.OperatorSet, address),
+        KeyRegistrar.getBN254Key(BN254TableCalculator.OperatorSet, address),
+    ] default NONDET;
+}
+
+use builtin rule sanity filtered { f -> f.contract == currentContract }
+
+function returnEmptyWeights() returns (address[], uint256[][]) {
+    address[] addresses;
+    uint256[][] weights;
+
+    return (addresses, weights);
+}  
\ No newline at end of file
diff --git a/certora/specs/ECDSATableCalculator.spec b/certora/specs/ECDSATableCalculator.spec
new file mode 100644
index 00000000..cbbe4d45
--- /dev/null
+++ b/certora/specs/ECDSATableCalculator.spec
@@ -0,0 +1,11 @@
+methods {
+    function _.isRegistered(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+    function _.getECDSAAddress(KeyRegistrar.OperatorSet, address) external => DISPATCHER(true);
+
+    unresolved external in _._ => DISPATCH[
+        KeyRegistrar.getECDSAAddress(KeyRegistrar.OperatorSet, address),
+        KeyRegistrar.isRegistered(KeyRegistrar.OperatorSet, address),
+    ] default NONDET;
+}
+
+use builtin rule sanity filtered { f -> f.contract == currentContract }
\ No newline at end of file
diff --git a/certora/specs/Summaries/BN254-nondet.spec b/certora/specs/Summaries/BN254-nondet.spec
new file mode 100644
index 00000000..679f690e
--- /dev/null
+++ b/certora/specs/Summaries/BN254-nondet.spec
@@ -0,0 +1,24 @@
+methods {
+    // BN254 implements elliptic curve operations, let's NONDET all of them
+    function BN254._ external => NONDET;
+    function BN254.plus(BN254.G1Point memory a, BN254.G1Point memory b) internal returns (BN254.G1Point memory) => CVL_randomPoint();
+    function BN254.pairing(BN254.G1Point memory a1, BN254.G2Point memory a2, BN254.G1Point memory b1, BN254.G2Point memory b2) internal returns (bool) => NONDET;
+    function BN254.safePairing(BN254.G1Point memory a, BN254.G2Point memory b, BN254.G1Point memory c, BN254.G2Point memory d, uint256) internal returns (bool,bool) => NONDET;
+    function BN254.scalar_mul(BN254.G1Point memory p, uint256 s) internal returns (BN254.G1Point memory) => CVL_randomPoint();
+
+    function BN254.expMod(uint256 b, uint256 e, uint256 m) internal returns (uint256) => CVL_expMod(b,e,m);
+}
+
+function CVL_plus(BN254.G1Point a, BN254.G1Point b) returns BN254.G1Point {
+    BN254.G1Point res;
+    return res;
+}
+
+function CVL_randomPoint() returns BN254.G1Point {
+    BN254.G1Point res;
+    return res;
+}
+
+function CVL_expMod(uint256 b, uint256 e, uint256 m) returns uint256 {
+    return require_uint256((b^e) % m);
+}
\ No newline at end of file
diff --git a/certora/specs/Summaries/Math.spec b/certora/specs/Summaries/Math.spec
new file mode 100644
index 00000000..111e11d6
--- /dev/null
+++ b/certora/specs/Summaries/Math.spec
@@ -0,0 +1,8 @@
+methods{
+    function Math.mulDiv(uint256 x, uint256 y, uint256 d) internal returns (uint256) => mulDivDownCVL(x,y,d);
+}
+
+function mulDivDownCVL(uint256 x, uint256 y, uint256 z) returns uint256 {
+    assert z !=0, "mulDivDown error: cannot divide by zero";
+    return require_uint256(x * y / z);
+}
\ No newline at end of file