Certora · aehyvari · Jun 4, 2025
diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml
@@ -1,122 +1,35 @@
 name: Certora
 
 on:
-  # Run when PRs from feat/* branches are merged into dev
   pull_request:
-    types: [closed]
     branches:
-      - main
-
-  # Run on any pushes to certora/* branches
-  push:
-    branches:
-      - 'certora/**'
-
-  # Biweekly schedule (1st and 15th of each month at midnight UTC)
-  schedule:
-    - cron: '0 0 1,15 * *'
-
-  # Manual trigger
+      - certora/distro
   workflow_dispatch:
 
 jobs:
-  # First job: Compile the contracts for Certora verification
-  compile:
-    name: Compile
-    # Run if it meets one of these conditions:
-    # 1. It's a merged PR from a feat/* branch to dev
-    # 2. It's a push to a certora/* branch
-    # 3. It's a scheduled run
-    # 4. It's a manually triggered run
-    if: >
-      (github.event_name == 'pull_request' && 
-       github.event.pull_request.merged == true && 
-       startsWith(github.head_ref, 'feat/')) || 
-      (github.event_name == 'push' && 
-       startsWith(github.ref, 'refs/heads/certora/')) ||
-      github.event_name == 'schedule' || 
-      github.event_name == 'workflow_dispatch'
-    runs-on: protocol-x64-16core
-    steps:
-      # Checkout the repository with submodules
-      - uses: actions/checkout@v4
-        with:
-          submodules: recursive
-          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
-          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
-
-      # Install the Foundry toolchain
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-        with:
-          version: stable
-
-      # Install dependencies using Forge
-      - name: Install forge dependencies
-        run: forge install
-
-      # Run Certora compilation step only
-      - uses: Certora/certora-run-action@v1
-        with:
-          # List of configuration files for different contracts to verify
-          configurations: |-
-            certora/confs/core/AllocationManager.conf
-            certora/confs/core/AllocationManagerSanity.conf
-            certora/confs/core/DelegationManager.conf
-            certora/confs/core/DelegationManagerValidState.conf
-            certora/confs/core/StrategyManager.conf
-            certora/confs/permissions/Pausable.conf
-            certora/confs/pods/EigenPodManagerRules.conf
-            certora/confs/strategies/StrategyBase.conf
-          use-beta: true
-          solc-versions: 0.8.27
-          solc-remove-version-prefix: "0."
-          job-name: "Eigenlayer Contracts"
-          certora-key: ${{ secrets.CERTORAKEY }}
-          # Only compile, don't run verification yet
-          compilation-steps-only: true
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-  # Second job: Run the actual verification after compilation succeeds
-  verify:
-    name: Verify
-    runs-on: protocol-x64-16core
-    # This job depends on the compile job
-    needs: compile
-    # Same conditions as the compile job
-    if: >
-      (github.event_name == 'pull_request' && 
-       github.event.pull_request.merged == true && 
-       startsWith(github.head_ref, 'feat/')) || 
-      (github.event_name == 'push' && 
-       startsWith(github.ref, 'refs/heads/certora/')) ||
-      github.event_name == 'schedule' || 
-      github.event_name == 'workflow_dispatch'
+  certora_run:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
     steps:
-      # Checkout the repository with submodules
-      - uses: actions/checkout@v4
+      - name: Checkout repository
+        uses: actions/checkout@v4
         with:
           submodules: recursive
-          # Use dev branch for scheduled runs, otherwise use the branch that triggered the workflow
-          ref: ${{ github.event_name == 'schedule' && 'dev' || github.ref }}
-
-      # Install the Foundry toolchain.
       - name: Install Foundry
         uses: foundry-rs/foundry-toolchain@v1
         with:
           version: stable
-
-      # Install dependencies using Forge
       - name: Install forge dependencies
         run: forge install
-
-      # Run Certora verification with the same configurations
-      - uses: Certora/certora-run-action@v1
+      - name: Run Certora pipeline
+        uses: Certora/certora-run-action@v1
         with:
-          # List of configuration files for different contracts to verify
           configurations: |-
             certora/confs/core/AllocationManager.conf
+            certora/confs/core/AllocationManagerValidState.conf
             certora/confs/core/AllocationManagerSanity.conf
             certora/confs/core/DelegationManager.conf
             certora/confs/core/DelegationManagerValidState.conf
@@ -126,7 +39,6 @@ jobs:
             certora/confs/strategies/StrategyBase.conf
           use-beta: true
           solc-versions: 0.8.27
-          solc-remove-version-prefix: "0."
           job-name: "Eigenlayer Contracts"
           certora-key: ${{ secrets.CERTORAKEY }}
         env:

diff --git a/certora/confs/core/AllocationManager.conf b/certora/confs/core/AllocationManager.conf
@@ -1,7 +1,7 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "src/contracts/core/AllocationManager.sol",
+        "certora/harnesses/AllocationManagerHarness.sol",
         "src/contracts/permissions/PauserRegistry.sol",
         "src/contracts/permissions/PermissionController.sol",
         "src/contracts/core/DelegationManager.sol",
@@ -10,19 +10,19 @@
         "src/contracts/strategies/StrategyBase.sol",
         "certora/mocks/CertoraAVSRegistrar.sol",
         "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
-        "src/contracts/libraries/OperatorSetLib.sol"
-    ],
-    "java_args": [
+        "src/contracts/libraries/OperatorSetLib.sol",
+        "certora/harnesses/ShortStringsUpgradeableHarness.sol",
     ],
+    "java_args": [],
     "link": [
-        "AllocationManager:pauserRegistry=PauserRegistry",
+        "AllocationManagerHarness:pauserRegistry=PauserRegistry",
         "DelegationManager:permissionController=PermissionController",
-        "DelegationManager:allocationManager=AllocationManager",
-        "AllocationManager:permissionController=PermissionController",
+        "DelegationManager:allocationManager=AllocationManagerHarness",
+        "AllocationManagerHarness:permissionController=PermissionController",
         "DelegationManager:strategyManager=StrategyManager",
-        "AllocationManager:delegation=DelegationManager",
+        "AllocationManagerHarness:delegation=DelegationManager",
         "EigenPodManager:delegationManager=DelegationManager",
-        "DelegationManager:eigenPodManager=EigenPodManager"
+        "DelegationManager:eigenPodManager=EigenPodManager",
     ],
     "loop_iter": "1",
     "optimistic_fallback": true,
@@ -32,14 +32,18 @@
         "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
     ],
     "parametric_contracts": [
-        "AllocationManager"
+        "AllocationManagerHarness"
     ],
+    "msg": "AllocationManager Rules",
     "process": "emv",
     "prover_args": [
-        " -recursionErrorAsAssert false -recursionEntryLimit 3"
+        "-recursionErrorAsAssert false -recursionEntryLimit 3",
+        "-splitParallel true",
+        "-dontStopAtFirstSplitTimeout true",
     ],
-    "solc": "solc8.27",
     "solc_optimize": "1",
-    "verify": "AllocationManager:certora/specs/core/AllocationManagerRules.spec",
+    "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerRules.spec",
     "server": "production",
+    "rule_sanity": "basic",
+    "build_cache": true
 }
diff --git a/certora/confs/core/AllocationManagerSanity.conf b/certora/confs/core/AllocationManagerSanity.conf
@@ -1,7 +1,7 @@
 {
     "assert_autofinder_success": true,
     "files": [
-        "src/contracts/core/AllocationManager.sol",
+        "certora/harnesses/AllocationManagerHarness.sol",
         "src/contracts/permissions/PauserRegistry.sol",
         "src/contracts/permissions/PermissionController.sol",
         "src/contracts/core/DelegationManager.sol",
@@ -12,17 +12,16 @@
         "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
         "src/contracts/libraries/OperatorSetLib.sol"
     ],
-    "java_args": [
-    ],
+    "java_args": [],
     "link": [
-        "AllocationManager:pauserRegistry=PauserRegistry",
+        "AllocationManagerHarness:pauserRegistry=PauserRegistry",
         "DelegationManager:permissionController=PermissionController",
-        "DelegationManager:allocationManager=AllocationManager",
-        "AllocationManager:permissionController=PermissionController",
+        "DelegationManager:allocationManager=AllocationManagerHarness",
+        "AllocationManagerHarness:permissionController=PermissionController",
         "DelegationManager:strategyManager=StrategyManager",
-        "AllocationManager:delegation=DelegationManager",
+        "AllocationManagerHarness:delegation=DelegationManager",
         "EigenPodManager:delegationManager=DelegationManager",
-        "DelegationManager:eigenPodManager=EigenPodManager"
+        "DelegationManager:eigenPodManager=EigenPodManager",
     ],
     "loop_iter": "2",
     "optimistic_fallback": true,
@@ -32,14 +31,14 @@
         "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
     ],
     "parametric_contracts": [
-        "AllocationManager"
+        "AllocationManagerHarness"
     ],
     "process": "emv",
     "prover_args": [
         " -recursionErrorAsAssert false -recursionEntryLimit 3"
     ],
-    "solc": "solc8.27",
     "solc_optimize": "1",
     "solc_via_ir": true,
-    "verify": "AllocationManager:certora/specs/core/AllocationManagerSanity.spec"
+    "server": "production",
+    "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerSanity.spec"
 }
diff --git a/certora/confs/core/AllocationManagerValidState.conf b/certora/confs/core/AllocationManagerValidState.conf
@@ -0,0 +1,45 @@
+{
+    "assert_autofinder_success": true,
+    "files": [
+        "certora/harnesses/AllocationManagerHarness.sol",
+        "src/contracts/permissions/PauserRegistry.sol",
+        "src/contracts/permissions/PermissionController.sol",
+        "src/contracts/core/DelegationManager.sol",
+        "src/contracts/pods/EigenPodManager.sol",
+        "src/contracts/core/StrategyManager.sol",
+        "src/contracts/strategies/StrategyBase.sol",
+        "certora/mocks/CertoraAVSRegistrar.sol",
+        "lib/openzeppelin-contracts-v4.9.0/contracts/token/ERC20/ERC20.sol",
+        "src/contracts/libraries/OperatorSetLib.sol"
+    ],
+    "java_args": [],
+    "link": [
+        "AllocationManagerHarness:pauserRegistry=PauserRegistry",
+        "DelegationManager:permissionController=PermissionController",
+        "DelegationManager:allocationManager=AllocationManagerHarness",
+        "AllocationManagerHarness:permissionController=PermissionController",
+        "DelegationManager:strategyManager=StrategyManager",
+        "AllocationManagerHarness:delegation=DelegationManager",
+        "EigenPodManager:delegationManager=DelegationManager",
+        "DelegationManager:eigenPodManager=EigenPodManager",
+    ],
+    "loop_iter": "1",
+    "optimistic_fallback": true,
+    "optimistic_loop": true,
+    "packages": [
+        "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
+        "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
+    ],
+    "parametric_contracts": [
+        "AllocationManagerHarness"
+    ],
+    "process": "emv",
+    "msg": "AllocationManager Valid State Invariants",
+    "prover_args": [
+        " -recursionErrorAsAssert false -recursionEntryLimit 3"
+    ],
+    "solc_optimize": "1",
+    "verify": "AllocationManagerHarness:certora/specs/core/AllocationManagerValidState.spec",
+    "rule_sanity": "basic",
+    "server": "production",
+}
diff --git a/certora/confs/core/DelegationManager.conf b/certora/confs/core/DelegationManager.conf
@@ -9,7 +9,6 @@
         "src/contracts/strategies/StrategyBase.sol",
         "src/contracts/core/StrategyManager.sol",
         "src/contracts/permissions/PauserRegistry.sol",
-        "src/contracts/core/DelegationManager.sol",
         "src/contracts/permissions/PermissionController.sol",
         "src/contracts/core/AllocationManager.sol"
     ],
@@ -20,7 +19,7 @@
         "AllocationManager:permissionController=PermissionController",
         "DelegationManagerHarness:strategyManager=StrategyManager",
         "EigenPodManager:delegationManager=DelegationManagerHarness",
-        "DelegationManagerHarness:eigenPodManager=EigenPodManager"
+        "DelegationManagerHarness:eigenPodManager=EigenPodManager",
     ],
     "loop_iter": "2",
     "optimistic_fallback": true,
@@ -34,6 +33,7 @@
         "-tinyTimeout 20",
         "-depth 20"
     ],
+    "msg": "DelegationManager Rules",
     "packages": [
         "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
         "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
@@ -43,8 +43,9 @@
     ],
     "rule_sanity": "basic",
     "process": "emv",
-    "solc": "solc8.27",
     "solc_optimize": "1",
     "solc_via_ir": true,
+    "build_cache": true, 
+    "server": "production",
     "verify": "DelegationManagerHarness:certora/specs/core/DelegationManager.spec"
 }
diff --git a/certora/confs/core/DelegationManagerValidState.conf b/certora/confs/core/DelegationManagerValidState.conf
@@ -9,9 +9,9 @@
         "src/contracts/strategies/StrategyBase.sol",
         "src/contracts/core/StrategyManager.sol",
         "src/contracts/permissions/PauserRegistry.sol",
-        "src/contracts/core/DelegationManager.sol",
         "src/contracts/permissions/PermissionController.sol",
-        "src/contracts/core/AllocationManager.sol"
+        "src/contracts/core/AllocationManager.sol",
+        "certora/mocks/CertoraAVSRegistrar.sol",
     ],
     "link": [
         "AllocationManager:delegation=DelegationManagerHarness",
@@ -20,7 +20,7 @@
         "AllocationManager:permissionController=PermissionController",
         "DelegationManagerHarness:strategyManager=StrategyManager",
         "EigenPodManager:delegationManager=DelegationManagerHarness",
-        "DelegationManagerHarness:eigenPodManager=EigenPodManager"
+        "DelegationManagerHarness:eigenPodManager=EigenPodManager",
     ],
     "loop_iter": "1",
     "optimistic_fallback": true,
@@ -31,13 +31,15 @@
         "@openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable-v4.9.0",
         "@openzeppelin=lib/openzeppelin-contracts-v4.9.0"
     ],
+    "msg": "DelegationManager Valid State Invariants",
     "parametric_contracts": [
-        "DelegationManagerHarness"
+        "DelegationManagerHarness", 
     ],
-   "rule_sanity": "basic",
+    "rule_sanity": "basic",
     "process": "emv",
-    "solc": "solc8.27",
     "solc_optimize": "1",
     "solc_via_ir": true,
+    "build_cache": true,
+    "server": "production",
     "verify": "DelegationManagerHarness:certora/specs/core/DelegationManagerValidState.spec"
 }