diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml
new file mode 100644
index 00000000..f3d07a0d
--- /dev/null
+++ b/.github/workflows/certora-prover.yml
@@ -0,0 +1,63 @@
+name: Certora Prover
+
+on:
+  push:
+    branches:
+      - master
+      - release-v*
+      - formal-verification
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  list-scripts:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - uses: actions/checkout@v2
+      - id: set-matrix
+        run: echo ::set-output name=matrix::$(ls certora/scripts/*.sh | grep -v '\WnoCI\W' | jq -Rsc 'split("\n")[:-1]')
+  verify:
+    runs-on: ubuntu-latest
+    needs: list-scripts
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+      - name: Install forge dependencies
+        run: forge install
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+          cache: 'pip'
+      - name: Install java
+        uses: actions/setup-java@v2
+        with:
+          distribution: temurin
+          java-version: '17'
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify rule ${{ matrix.params }}
+        run: |
+          touch certora/applyHarness.patch
+          make -C certora munged
+          bash ${{ matrix.params }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params: ${{ fromJson(needs.list-scripts.outputs.matrix) }}
diff --git a/.gitignore b/.gitignore
index db471e42..bac8fb01 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,9 @@ node_modules/
 
 # Dotenv file
 .env
+
+# Certora Outputs
+.certora_internal/
+.certora_recent_jobs.json
+
+*.DS_Store
diff --git a/.gitmodules b/.gitmodules
index 635af195..6c719165 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,3 @@
-[submodule "lib/forge-std"]
-	path = lib/forge-std
-	url = https://github.com/foundry-rs/forge-std
 [submodule "lib/eigenlayer-contracts"]
 	path = lib/eigenlayer-contracts
-	url = https://github.com/Layr-labs/eigenlayer-contracts
-[submodule "lib/ds-test"]
-	path = lib/ds-test
-	url = https://github.com/dapphub/ds-test
+	url = https://github.com/Layr-Labs/eigenlayer-contracts
diff --git a/certora/.gitignore b/certora/.gitignore
new file mode 100644
index 00000000..28437922
--- /dev/null
+++ b/certora/.gitignore
@@ -0,0 +1 @@
+munged
\ No newline at end of file
diff --git a/certora/Makefile b/certora/Makefile
new file mode 100644
index 00000000..77c6375b
--- /dev/null
+++ b/certora/Makefile
@@ -0,0 +1,25 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../src
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+refresh: munged record
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
new file mode 100644
index 00000000..e69de29b
diff --git a/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol b/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol
new file mode 100644
index 00000000..54330ea1
--- /dev/null
+++ b/certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol
@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: BUSL-1.1
+pragma solidity =0.8.12;
+
+import "../munged/BLSRegistryCoordinatorWithIndices.sol";
+
+contract BLSRegistryCoordinatorWithIndicesHarness is BLSRegistryCoordinatorWithIndices {
+    constructor(
+        ISlasher _slasher,
+        IServiceManager _serviceManager,
+        IStakeRegistry _stakeRegistry,
+        IBLSPubkeyRegistry _blsPubkeyRegistry,
+        IIndexRegistry _indexRegistry
+    )
+        BLSRegistryCoordinatorWithIndices(_slasher, _serviceManager, _stakeRegistry, _blsPubkeyRegistry, _indexRegistry)
+    {}
+
+    // @notice function based upon `BitmapUtils.bytesArrayToBitmap`, used to determine if an array contains any duplicates
+    function bytesArrayContainsDuplicates(bytes memory bytesArray) public pure returns (bool) {
+        // sanity-check on input. a too-long input would fail later on due to having duplicate entry(s)
+        if (bytesArray.length > 256) {
+            return false;
+        }
+
+        // initialize the empty bitmap, to be built inside the loop
+        uint256 bitmap;
+        // initialize an empty uint256 to be used as a bitmask inside the loop
+        uint256 bitMask;
+
+        // loop through each byte in the array to construct the bitmap
+        for (uint256 i = 0; i < bytesArray.length; ++i) {
+            // construct a single-bit mask from the numerical value of the next byte out of the array
+            bitMask = uint256(1 << uint8(bytesArray[i]));
+            // check that the entry is not a repeat
+            if (bitmap & bitMask != 0) {
+                return false;
+            }
+            // add the entry to the bitmap
+            bitmap = (bitmap | bitMask);
+        }
+
+        // if the loop is completed without returning early, then the array contains no duplicates
+        return true;
+    }
+
+    // @notice verifies that a bytes array is a (non-strict) subset of a bitmap
+    function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes memory arrayWhichShouldBeASubsetOfTheReference) public pure returns (bool) {
+        uint256 arrayWhichShouldBeASubsetOfTheReferenceBitmap = BitmapUtils.bytesArrayToBitmap(arrayWhichShouldBeASubsetOfTheReference);
+        if (referenceBitmap | arrayWhichShouldBeASubsetOfTheReferenceBitmap == referenceBitmap) {
+            return true;
+        } else {
+            return false;
+        }
+    }
+}
\ No newline at end of file
diff --git a/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh
new file mode 100644
index 00000000..a6e7e171
--- /dev/null
+++ b/certora/scripts/verifyBLSRegistryCoordinatorWithIndices.sh
@@ -0,0 +1,21 @@
+if [[ "$2" ]]
+then
+    RULE="--rule $2"
+fi
+
+solc-select use 0.8.12
+
+certoraRun certora/harnesses/BLSRegistryCoordinatorWithIndicesHarness.sol \
+    lib/eigenlayer-contracts/lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \
+    certora/munged/StakeRegistry.sol certora/munged/BLSPubkeyRegistry.sol certora/munged/IndexRegistry.sol \
+    lib/eigenlayer-contracts/src/contracts/core/Slasher.sol \
+    --verify BLSRegistryCoordinatorWithIndicesHarness:certora/specs/BLSRegistryCoordinatorWithIndices.spec \
+    --optimistic_loop \
+    --optimistic_hashing \
+    --prover_args '-optimisticFallback true -recursionEntryLimit 2 ' \
+    $RULE \
+    --loop_iter 2 \
+    --packages @openzeppelin=lib/eigenlayer-contracts/lib/openzeppelin-contracts @openzeppelin-upgrades=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable eigenlayer-contracts=lib/eigenlayer-contracts \
+    --msg "BLSRegistryCoordinatorWithIndices $1 $2" \
+
+# TODO: import a ServiceManager contract
\ No newline at end of file
diff --git a/certora/specs/BLSRegistryCoordinatorWithIndices.spec b/certora/specs/BLSRegistryCoordinatorWithIndices.spec
new file mode 100644
index 00000000..a4eaeb01
--- /dev/null
+++ b/certora/specs/BLSRegistryCoordinatorWithIndices.spec
@@ -0,0 +1,173 @@
+
+methods {
+    //// External Calls
+	// external calls to StakeRegistry
+    function _.quorumCount() external => DISPATCHER(true);
+    function _.getCurrentTotalStakeForQuorum(uint8 quorumNumber) external => DISPATCHER(true);
+    function _.getCurrentOperatorStakeForQuorum(bytes32 operatorId, uint8 quorumNumber) external => DISPATCHER(true);
+    // function _.registerOperator(address, bytes32, bytes) external => DISPATCHER(true);
+    function _.registerOperator(address, bytes32, bytes) external => NONDET;
+    function _.deregisterOperator(bytes32, bytes) external => DISPATCHER(true);
+
+	// external calls to Slasher
+    function _.contractCanSlashOperatorUntilBlock(address, address) external => DISPATCHER(true);
+
+    // external calls to BLSPubkeyRegistry
+    // function _.registerOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true);
+    function _.registerOperator(address, bytes, BN254.G1Point) external => NONDET;
+    function _.deregisterOperator(address, bytes, BN254.G1Point) external => DISPATCHER(true);
+
+	// external calls to ServiceManager
+    function _.latestServeUntilBlock() external => DISPATCHER(true);
+    function _.recordLastStakeUpdateAndRevokeSlashingAbility(address, uint256) external => DISPATCHER(true);
+
+	// external calls to IndexRegistry
+    // function _.registerOperator(bytes32, bytes) external => DISPATCHER(true);
+    function _.registerOperator(bytes32, bytes) external => NONDET;
+    function _.deregisterOperator(bytes32, bytes, bytes32[]) external => DISPATCHER(true);
+
+    // external calls to ERC1271 (can import OpenZeppelin mock implementation)
+    // isValidSignature(bytes32 hash, bytes memory signature) returns (bytes4 magicValue) => DISPATCHER(true)
+    // function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true);
+    function _.isValidSignature(bytes32, bytes) external => NONDET;
+
+	// external calls to BLSPubkeyCompendium
+    function _.pubkeyHashToOperator(bytes32) external => DISPATCHER(true);
+
+    //envfree functions
+    function OPERATOR_CHURN_APPROVAL_TYPEHASH() external returns (bytes32) envfree;
+    function slasher() external returns (address) envfree;
+    function serviceManager() external returns (address) envfree;
+    function blsPubkeyRegistry() external returns (address) envfree;
+    function stakeRegistry() external returns (address) envfree;
+    function indexRegistry() external returns (address) envfree;
+    function registries(uint256) external returns (address) envfree;
+    function churnApprover() external returns (address) envfree;
+    function isChurnApproverSaltUsed(bytes32) external returns (bool) envfree;
+    function getOperatorSetParams(uint8 quorumNumber) external returns (IBLSRegistryCoordinatorWithIndices.OperatorSetParam) envfree;
+    function getOperator(address operator) external returns (IRegistryCoordinator.Operator) envfree;
+    function getOperatorId(address operator) external returns (bytes32) envfree;
+    function getOperatorStatus(address operator) external returns (IRegistryCoordinator.OperatorStatus) envfree;
+    function getQuorumBitmapIndicesByOperatorIdsAtBlockNumber(uint32 blockNumber, bytes32[] operatorIds)
+        external returns (uint32[]) envfree;
+    function getQuorumBitmapByOperatorIdAtBlockNumberByIndex(bytes32 operatorId, uint32 blockNumber, uint256 index) external returns (uint192) envfree;
+    function getQuorumBitmapUpdateByOperatorIdByIndex(bytes32 operatorId, uint256 index)
+        external returns (IRegistryCoordinator.QuorumBitmapUpdate) envfree;
+    function getCurrentQuorumBitmapByOperatorId(bytes32 operatorId) external returns (uint192) envfree;
+    function getQuorumBitmapUpdateByOperatorIdLength(bytes32 operatorId) external returns (uint256) envfree;
+    function numRegistries() external returns (uint256) envfree;
+    function calculateOperatorChurnApprovalDigestHash(
+        bytes32 registeringOperatorId,
+        IBLSRegistryCoordinatorWithIndices.OperatorKickParam[] operatorKickParams,
+        bytes32 salt,
+        uint256 expiry
+    ) external returns (bytes32) envfree;
+
+    // harnessed functions
+    function bytesArrayContainsDuplicates(bytes bytesArray) external returns (bool) envfree;
+    function bytesArrayIsSubsetOfBitmap(uint256 referenceBitmap, bytes arrayWhichShouldBeASubsetOfTheReference) external returns (bool) envfree;
+}
+
+// If my Operator status is REGISTERED ⇔ my quorum bitmap MUST BE nonzero
+invariant registeredOperatorsHaveNonzeroBitmaps(address operator)
+    getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED <=>
+        getCurrentQuorumBitmapByOperatorId(getOperatorId(operator)) != 0;
+
+// if two operators have different addresses, then they have different IDs
+// excludes the case in which the operator is not registered, since then they can both have ID zero (the default)
+invariant operatorIdIsUnique(address operator1, address operator2)
+    operator1 != operator2 =>
+        (getOperatorStatus(operator1) == IRegistryCoordinator.OperatorStatus.REGISTERED => getOperatorId(operator1) != getOperatorId(operator2));
+
+definition methodCanModifyBitmap(method f) returns bool =
+    f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector
+    || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector
+    || f.selector == sig:registerOperatorWithCoordinator(
+        bytes,
+        BN254.G1Point,
+        string,
+        IBLSRegistryCoordinatorWithIndices.OperatorKickParam[],
+        ISignatureUtils.SignatureWithSaltAndExpiry
+    ).selector
+    || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector
+    || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector;
+
+definition methodCanAddToBitmap(method f) returns bool =
+    f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector
+    || f.selector == sig:registerOperatorWithCoordinator(bytes, BN254.G1Point, string).selector
+    || f.selector == sig:registerOperatorWithCoordinator(
+        bytes,
+        BN254.G1Point,
+        string,
+        IBLSRegistryCoordinatorWithIndices.OperatorKickParam[],
+        ISignatureUtils.SignatureWithSaltAndExpiry
+    ).selector;
+
+// `registerOperatorWithCoordinator` with kick params also meets this definition due to the 'churn' mechanism
+definition methodCanRemoveFromBitmap(method f) returns bool =
+    f.selector == sig:registerOperatorWithCoordinator(
+        bytes,
+        BN254.G1Point,
+        string,
+        IBLSRegistryCoordinatorWithIndices.OperatorKickParam[],
+        ISignatureUtils.SignatureWithSaltAndExpiry
+    ).selector
+    || f.selector == sig:deregisterOperatorWithCoordinator(bytes, bytes).selector
+    || f.selector == sig:deregisterOperatorWithCoordinator(bytes, BN254.G1Point, bytes32[]).selector;
+
+// verify that quorumNumbers provided as an input to deregister operator MUST BE a subset of the operator’s current quorums
+rule canOnlyDeregisterFromExistingQuorums(address operator) {
+    requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator);
+
+    // TODO: store this status, verify that all calls to `deregisterOperatorWithCoordinator` *fail* if the operator is not registered first!
+    require(getOperatorStatus(operator) == IRegistryCoordinator.OperatorStatus.REGISTERED);
+
+    uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator));
+
+    bytes quorumNumbers;
+    BN254.G1Point pubkey;
+    bytes32[] operatorIdsToSwap;
+    env e;
+
+    deregisterOperatorWithCoordinator(e, quorumNumbers, pubkey, operatorIdsToSwap);
+
+    // if deregistration is successful, verify that `quorumNumbers` input was proper
+    if (getOperatorStatus(operator) != IRegistryCoordinator.OperatorStatus.REGISTERED) {
+        assert(bytesArrayIsSubsetOfBitmap(bitmapBefore, quorumNumbers));
+    } else {
+        assert(true);
+    }
+}
+
+/* TODO: this is a Work In Progress
+rule canOnlyModifyBitmapWithSpecificFunctions(address operator) {
+    requireInvariant registeredOperatorsHaveNonzeroBitmaps(operator);
+    uint256 bitmapBefore = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator));
+    // prepare to perform arbitrary function call
+    method f;
+    env e;
+    // TODO: need to ensure that if the function can modify the bitmap, then we are using the operator as an input
+    if (!methodCanModifyBitmap(f)) {
+        // perform arbitrary function call
+        calldataarg arg;
+        f(e, arg);
+        uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator));
+        assert(bitmapAfter == bitmapBefore);
+    } else if (
+        f.selector == sig:registerOperatorWithCoordinator(bytes, bytes).selector
+    ) {
+        if (e.msg.sender != operator) {
+            uint256 bitmapAfter = getCurrentQuorumBitmapByOperatorId(getOperatorId(operator));
+            assert(bitmapAfter == bitmapBefore);
+        }
+    }
+
+        // if method did not remove from bitmap, it must have added
+        if (bitmapAfter & bitmapBefore == bitmapBefore) {
+            assert(methodCanAddToBitmap(f));
+        } else {
+            assert(methodCanRemoveFromBitmap(f));
+        }
+    }
+}
+*/
\ No newline at end of file
diff --git a/lib/ds-test b/lib/ds-test
deleted file mode 160000
index e282159d..00000000
--- a/lib/ds-test
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit e282159d5170298eb2455a6c05280ab5a73a4ef0
diff --git a/lib/forge-std b/lib/forge-std
deleted file mode 160000
index f73c73d2..00000000
--- a/lib/forge-std
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f73c73d2018eb6a111f35e4dae7b4f27401e9421
diff --git a/remappings.txt b/remappings.txt
index 26950b6a..25d27daf 100644
--- a/remappings.txt
+++ b/remappings.txt
@@ -1,7 +1,7 @@
 @openzeppelin-upgrades/=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable/
 @openzeppelin/=lib/eigenlayer-contracts/lib/openzeppelin-contracts/
-ds-test/=lib/ds-test/src/
+ds-test/=lib/eigenlayer-contracts/lib/ds-test/src/
 eigenlayer-contracts/=lib/eigenlayer-contracts/
-forge-std/=lib/forge-std/src/
+forge-std/=lib/eigenlayer-contracts/lib/forge-std/src/
 openzeppelin-contracts-upgradeable/=lib/eigenlayer-contracts/lib/openzeppelin-contracts-upgradeable/
 openzeppelin-contracts/=lib/eigenlayer-contracts/lib/openzeppelin-contracts/