diff --git a/.github/workflows/certora-prover-conf.yml b/.github/workflows/certora-prover-conf.yml
index 9210685b46..62d825f5d2 100644
--- a/.github/workflows/certora-prover-conf.yml
+++ b/.github/workflows/certora-prover-conf.yml
@@ -7,6 +7,7 @@ on:
       - testnet-holesky
       - mainnet
       - rewards-spec
+      - formal-verification*
   pull_request: {}
   workflow_dispatch: {}
 
diff --git a/certora/conf/rewardsCoordinatorWithoutSanity.conf b/certora/conf/rewardsCoordinatorWithoutSanity.conf
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/certora/harnesses/RewardsCoordinatorHarness.sol b/certora/harnesses/RewardsCoordinatorHarness.sol
deleted file mode 100644
index 2af5d4687e..0000000000
--- a/certora/harnesses/RewardsCoordinatorHarness.sol
+++ /dev/null
@@ -1,24 +0,0 @@
-// SPDX-License-Identifier: BUSL-1.1
-pragma solidity ^0.8.12;
-
-import "../../src/contracts/core/RewardsCoordinator.sol";
-
-contract RewardsCoordinatorHarness is RewardsCoordinator {
-    constructor(
-        IDelegationManager _delegationManager,
-        IStrategyManager _strategyManager,
-        uint32 _CALCULATION_INTERVAL_SECONDS,
-        uint32 _MAX_PAYMENT_DURATION,
-        uint32 _MAX_RETROACTIVE_LENGTH,
-        uint32 _MAX_FUTURE_LENGTH,
-        uint32 _GENESIS_PAYMENT_TIMESTAMP
-    ) RewardsCoordinator(
-        _delegationManager,
-        _strategyManager,
-        _CALCULATION_INTERVAL_SECONDS,
-        _MAX_PAYMENT_DURATION,
-        _MAX_RETROACTIVE_LENGTH,
-        _MAX_FUTURE_LENGTH,
-        _GENESIS_PAYMENT_TIMESTAMP
-    ) {}
-}
\ No newline at end of file