diff --git a/.github/workflows/certora.yaml b/.github/workflows/certora.yaml
index 2a2230f5e..42187a8fa 100644
--- a/.github/workflows/certora.yaml
+++ b/.github/workflows/certora.yaml
@@ -1,9 +1,19 @@
 name: Certora
 
-# Formal verification lane. Runs on demand, on a weekly schedule, and on PRs that touch
-# contracts or the Certora workspace. NOT a required PR gate yet (no branch protection):
-# it stays informational until prover runtimes and false-positive rates are understood
-# across the full matrix (see docs/testing/certora-followup.md "CI maturation").
+# Formal verification lane. Three jobs with different gating intent:
+#
+#   certora-check   — compile + CVL type-check every conf. No CERTORAKEY, no cloud,
+#                     deterministic and fast. This is the lane's REQUIRED-gate candidate:
+#                     it catches spec/contract signature drift (the failure that left
+#                     ClusterPayoutOracle.spec stale behind three contract commits).
+#   spec-freshness  — on PRs, fail if a contract with Certora coverage changed without
+#                     its spec being reviewed (bypass with [spec-ok] in the PR title/body).
+#   certora         — the full cloud prover matrix. Needs the CERTORAKEY secret and runs
+#                     for minutes-to-hours, so it stays NON-gating (informational) until
+#                     runtimes/false-positive rates are understood; promote the fast confs
+#                     (math, cluster-payout-oracle, loop-reputation, protocol-config,
+#                     mul-div-lemma) to required cloud runs once stable. See
+#                     docs/testing/certora-round3-plan.md (Track G).
 
 on:
   workflow_dispatch:
@@ -25,6 +35,85 @@ env:
   SOLC_VERSION: "0.8.35"
 
 jobs:
+  # ---------------------------------------------------------------------------
+  # Required-gate candidate: compile + CVL type-check, no secret, no cloud run.
+  # ---------------------------------------------------------------------------
+  certora-check:
+    runs-on: ubuntu-latest
+    name: certora-check (compile + typecheck)
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          submodules: true
+
+      - uses: ./.github/actions/setup-foundry
+
+      - name: Use preinstalled Java 21
+        # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs
+        # Java >= 19; the runner's default java is older. Point at the GitHub-hosted
+        # runner's preinstalled JDK 21 rather than apt-installing one that is not the
+        # default on PATH.
+        run: |
+          echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV"
+          echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH"
+      - name: Verify Java
+        run: java --version
+
+      - name: Install Certora CLI and solc
+        run: |
+          python3 -m pip install --upgrade pip
+          python3 -m pip install "certora-cli${CERTORA_CLI_VERSION}" solc-select
+          solc-select install "$SOLC_VERSION"
+          solc-select use "$SOLC_VERSION"
+          certoraRun --version
+          solc --version
+
+      - name: Compile + type-check every conf
+        working-directory: packages/foundry
+        run: |
+          set -uo pipefail
+          failed=()
+          for conf in certora/confs/*.conf; do
+            [ "$(basename "$conf")" = "base.conf" ] && continue
+            echo "::group::$conf"
+            if certoraRun "$conf" --compilation_steps_only; then
+              echo "OK: $conf"
+            else
+              echo "::error::compile/type-check failed: $conf"
+              failed+=("$conf")
+            fi
+            echo "::endgroup::"
+          done
+          if [ "${#failed[@]}" -ne 0 ]; then
+            echo "Type-check failed for: ${failed[*]}"
+            exit 1
+          fi
+          echo "All confs compiled and type-checked."
+
+  # ---------------------------------------------------------------------------
+  # PR guard: a covered contract may not change without its spec being reviewed.
+  # ---------------------------------------------------------------------------
+  spec-freshness:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'pull_request'
+    name: spec-freshness
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          fetch-depth: 0
+
+      - name: Check spec freshness vs. contract changes
+        env:
+          BASE_REF: ${{ github.base_ref }}
+          SPEC_FRESHNESS_OVERRIDE: "${{ github.event.pull_request.title }} ${{ github.event.pull_request.body }}"
+        run: |
+          git fetch --no-tags --depth=1 origin "$BASE_REF"
+          git diff --name-only "origin/${BASE_REF}...HEAD" \
+            | python3 packages/foundry/certora/scripts/check_spec_freshness.py --changed-stdin
+
+  # ---------------------------------------------------------------------------
+  # Full cloud prover matrix (non-gating; needs the CERTORAKEY secret).
+  # ---------------------------------------------------------------------------
   certora:
     runs-on: ubuntu-latest
     strategy:
@@ -32,9 +121,11 @@ jobs:
       matrix:
         conf:
           - certora/confs/math.conf
+          - certora/confs/mul-div-lemma.conf
           - certora/confs/cluster-payout-oracle.conf
           - certora/confs/round-voting-engine.conf
           - certora/confs/round-reward-distributor.conf
+          - certora/confs/round-reward-distributor-conservation.conf
           - certora/confs/no-double-claim.conf
           - certora/confs/round-voting-engine-lifecycle.conf
           - certora/confs/launch-distribution-pool.conf
@@ -45,8 +136,10 @@ jobs:
           - certora/confs/launch-distribution-pool-cap.conf
           - certora/confs/launch-distribution-pool-conservation.conf
           # NOTE: question-reward-escrow.conf and question-reward-escrow-claim.conf are
-          # intentionally excluded — both exceed certora-cli's 15-minute output window on
-          # this 1,490-line + 11-library contract. Run them manually with a larger budget.
+          # intentionally excluded from the proof matrix — both exceed certora-cli's
+          # 15-minute output window on this 1,490-line + 11-library contract. Run them
+          # manually with a larger budget. (They are still compile/type-checked by the
+          # certora-check job above.)
     name: ${{ matrix.conf }}
     steps:
       - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
@@ -55,11 +148,16 @@ jobs:
 
       - uses: ./.github/actions/setup-foundry
 
-      - name: Install Java 21
+      - name: Use preinstalled Java 21
+        # certora-cli's local CVL type-checker (used by --compilation_steps_only) needs
+        # Java >= 19; the runner's default java is older. Point at the GitHub-hosted
+        # runner's preinstalled JDK 21 rather than apt-installing one that is not the
+        # default on PATH.
         run: |
-          sudo apt-get update
-          sudo apt-get install -y --no-install-recommends openjdk-21-jre-headless
-          java --version
+          echo "JAVA_HOME=$JAVA_HOME_21_X64" >> "$GITHUB_ENV"
+          echo "$JAVA_HOME_21_X64/bin" >> "$GITHUB_PATH"
+      - name: Verify Java
+        run: java --version
 
       - name: Install Certora CLI and solc
         run: |
diff --git a/docs/testing/certora-escalation-internal-summary-via-ir.md b/docs/testing/certora-escalation-internal-summary-via-ir.md
new file mode 100644
index 000000000..21b299642
--- /dev/null
+++ b/docs/testing/certora-escalation-internal-summary-via-ir.md
@@ -0,0 +1,80 @@
+# Certora escalation — internal-function summaries under solc_optimize + solc_via_ir
+
+This is a ready-to-file support/forum write-up for the one genuinely tooling-blocked item
+in the RateLoop Certora lane (Track A). It is parked here, not chased, because — as
+verified below — there is no working path in certora-cli 8.13.1, which is the latest
+release. File it upstream and re-test on each certora-cli bump.
+
+## Summary
+
+Several high-value properties (single-use refund on `RoundVotingEngine`, per-commit
+no-double-claim on `QuestionRewardPoolEscrow`) require summarizing an **internal**
+commit-resolution function deterministically. certora-cli 8.13.1 cannot apply
+internal-function summaries when the contract is compiled with `solc_optimize` +
+`solc_via_ir`, emitting:
+
+```
+Cannot apply summaries for internal functions ... when compiling using solc_optimize and solc_via_ir
+```
+
+and (relatedly, for the auto-finder):
+
+```
+Failed to generate auto finder for <fn> ...
+WARNING: Cannot apply summaries for internal functions with unnamed argument when compiling using solc_optimize and solc_via_ir
+```
+
+These contracts genuinely require `via_ir`: building them on the legacy pipeline fails with
+`Stack too deep. Try compiling with --via-ir`. So `via_ir` cannot be dropped, and the
+internal summary cannot be applied — there is no intersection.
+
+## Environment
+
+- certora-cli: 8.13.1 (latest as of 2026-05-19; confirmed on PyPI / Prover changelog)
+- solc: 0.8.35 + `via_ir`, optimizer runs = 100, evm = cancun
+- `yul_optimizer_steps` set to solc 0.8.34's step string (certora-cli does not natively map
+  0.8.35's via_ir Yul steps — a separate, minor gap)
+
+## Real-world repro cases in this repo
+
+Both are committed and reproduce the warning under `make certora-check`
+(`certoraRun <conf> --compilation_steps_only`):
+
+- `packages/foundry/certora/confs/round-voting-engine-lifecycle.conf` — the single-use
+  refund property routes through the engine's internal `_resolveClaimCommit`.
+- `packages/foundry/certora/confs/question-reward-escrow-claim.conf` — the per-commit
+  no-double-claim routes through `QuestionRewardPoolEscrow._resolveQuestionRewardClaim`
+  (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733), which is
+  internal — not an external call summarizable the way `NoDoubleClaim.spec` summarizes the
+  distributor→engine external `resolveClaimCommit`.
+
+## What was already tried (and did not work)
+
+Recorded from the round-2 empirical validation (docs/testing/certora-next-steps.md):
+
+| Attempt | Result |
+|---|---|
+| `function_finder_mode: relaxed` (valid key in 8.13.1) | internal summary still not applied |
+| `use_memory_safe_autofinders` conf key | rejected — not a valid key in 8.13.1 |
+| Drop via_ir (`solc_via_ir: false`) so internal summaries work | compile error: `Stack too deep. Try compiling with --via-ir` |
+| Re-expose the internal fn as external on a harness | does not intercept — the call inside the contract is to the internal function directly |
+
+## The ask
+
+Add support for applying CVL internal-function summaries (or a sound equivalent) when a
+contract is compiled with `solc_optimize` + `solc_via_ir`. Failing that, guidance on a
+supported pattern for deterministically modeling an internal resolver in a via_ir-required
+contract.
+
+## What we did instead (so the properties are not silently uncovered)
+
+- Proved the **resolution-independent state gates** the single-use properties build on:
+  refunds revert unless the round is terminal-but-not-settled; refunded pools reject
+  claims (`RoundVotingEngineLifecycle.spec`, `QuestionRewardPoolEscrow.spec`).
+- Proved the **cross-contract** no-double-claim where the resolver IS external
+  (`NoDoubleClaim.spec`).
+- The remaining single-use refund / per-commit no-double-claim are defense-in-depth on
+  flag-guarded paths already exercised by the Foundry test suite.
+
+Treat this as a tooling escalation, not an engineering task, until a certora-cli release
+maps internal summaries under via_ir.
diff --git a/docs/testing/certora-round3-plan.md b/docs/testing/certora-round3-plan.md
new file mode 100644
index 000000000..716346ded
--- /dev/null
+++ b/docs/testing/certora-round3-plan.md
@@ -0,0 +1,190 @@
+# Certora — round-3 plan (research-backed)
+
+This is the third follow-up. Rounds 1–2 ([`certora-followup.md`](./certora-followup.md),
+[`certora-next-steps.md`](./certora-next-steps.md)) landed Phases 1–10 / Tracks B–G as
+verified slices, with the blocked remainder recorded in
+[`certora-security-findings.md`](./certora-security-findings.md). This round re-asks the
+question **"is it worth continuing, and if so on what?"** after a fresh research pass, and
+narrows the work to what is actually unblocked and high-value today.
+
+> **Implementation status (2026-06-09).** All seven items below were implemented on branch
+> `certora-followup-research-3`, each as its own commit. Every spec/conf compiles and CVL
+> type-checks under certora-cli 8.13.1 (`make certora-check`); full proofs run on the cloud
+> prover via CI (no `CERTORAKEY` locally). Summary:
+>
+> | Item | Outcome |
+> |---|---|
+> | 1. Oracle spec refresh | ✅ added `cannotReproposeRejectedCorrelationEpochRoot` (covers the L-Oracle-4 replay branch), fixed the stale line ref, documented the still-deferred new surface |
+> | 2. Track C aggregate conservation | ◑ landed the tooling-independent pieces: `MulDivLemma.spec` (the reusable `(a*b)/c<=a` bound) + distributor accumulator monotonicity. The full inductive `claimed<=pool` upper bound stays deferred (needs the score-weight summation / engine model) — documented precisely |
+> | 3. Track G CI | ✅ secret-free `certora-check` type-check gate + `spec-freshness` PR guard (+ script, tested) + new confs wired into the cloud matrix |
+> | 4. Gambit | ✅ three mutation confs (FrontendRegistry, FeedbackBonusEscrow, RewardMath) + `make certora-mutate` + how-to README |
+> | 5. Track B cap | ◑ `assignedCapWithinFullCap` machine-checks the cap-assignment clamp under `-smt_useNIA` (was by-inspection only); end-to-end global invariant stays the documented residual |
+> | 6. Track D QRPE | ◑ `nondet_difficult_funcs` load-cut applied; **corrected the premise** — QRPE's resolver is internal, so per-commit no-double-claim is blocked by the same wall as Track A, not unblockable by send-only |
+> | 7. Track A | ✅ escalation write-up filed in-repo (`certora-escalation-internal-summary-via-ir.md`); no engineering, revisit on cli bump |
+>
+> ◑ = partial by design (the tooling-independent slice landed; the residual is a documented
+> solver/tooling limit, not a contract defect).
+
+## Should we continue? — yes, with a narrowed scope
+
+The effort is mature and the docs are excellent. Two research findings reshape the plan:
+
+1. **certora-cli 8.13.1 is already the latest release** (May 19, 2026 — confirmed on PyPI
+   and the Prover changelog). There is no 8.14+/9.x. So the items parked as
+   "tooling-blocked, revisit on a cli bump" — chiefly **Track A** (engine internal-resolution
+   under `via_ir`), native solc-0.8.35 `via_ir` mapping, and the large-contract timeout — have
+   **no upgrade path right now**. The existing "escalate, don't chase" call on Track A is
+   correct and should be treated as final for this round. We are at the tooling ceiling; do
+   not spend engineering time fighting it.
+
+2. **The contracts have outrun the specs.** `ClusterPayoutOracle.sol` changed three times on
+   2026-06-08 (`10ded66c` block replay of rejected correlation roots, `808570b3` reject
+   same-frontend challenges, `969536f0` split oracle metadata vs root rejections) — all
+   *after* `ClusterPayoutOracle.spec` was frozen on 2026-06-07. The spec still compiles (no
+   signature/struct drift), so existing proofs are not invalidated, but the new
+   security-relevant branches (correlation-epoch root/metadata rejection split, same-frontend
+   challenge guard) are **uncovered**, and one inline line reference is now stale (385 → 429).
+   This is verification debt accruing in real time, and it is the freshest, most concrete
+   reason to keep the lane alive.
+
+Net: continue, but spend the budget on **tooling-independent, fund-protecting work** —
+refreshing drifted specs, the one headline solvency property that research showed is now
+cheap, CI maturation, and a spec-strength check — not on the confirmed tooling dead-ends.
+
+## What is genuinely left
+
+| Item | Status after research | Verdict |
+|---|---|---|
+| Oracle spec drift (new uncovered branches) | NEW finding — contract changed after spec frozen | **Do first** — fresh debt |
+| Track C: aggregate `claimed ≤ pool` (RoundRewardDistributor) | Feasible & cheaper than thought — the sum is already a scalar slot | **High value** |
+| Track G: promote fast confs to required PR gate + freshness guard | CI still non-gating (`workflow_dispatch` + cron) | **High value, low effort** |
+| Track B: machine-check `paid ≤ cap` end-to-end | Documented solver-completeness gap; correct by inspection | Low priority |
+| Track D: QRPE no-double-claim without timeout | NONDET-lib fix not yet attempted; may be blocked by same via_ir/internal-summary limit | Attempt, time-boxed |
+| Gambit mutation testing | `certoraMutate` actively maintained; runs against existing specs | Worthwhile assurance check |
+| Track A: engine internal-resolution under via_ir | Confirmed hard limit in 8.13.1 (latest); no fix exists | **Escalate only** — file issue, stop |
+
+## The plan (priority order)
+
+### 1. Refresh the ClusterPayoutOracle spec to the current contract  ← do first
+
+The contract grew new branches the spec doesn't see. Close the gap:
+
+- Fix the stale line reference in `ClusterPayoutOracle.spec` (rejected-root guard moved from
+  `:385` to `:429`).
+- Add rules for the **new** rejection surface from `969536f0` / `10ded66c`:
+  - correlation-epoch root rejection is permanent and blocks replay
+    (`rejectedCorrelationEpochRoots`, new `rejectedCorrelationEpochSnapshotDigests`);
+  - the metadata-vs-root split (`rejectCorrelationEpoch` / `rejectCorrelationEpochRoot` /
+    `rejectFinalizedCorrelationEpoch` / `rejectFinalizedCorrelationEpochRoot`) — each path's
+    guard fires and is single-use.
+- Add a rule for the same-frontend challenge guard (`808570b3`): a challenge from the
+  proposing frontend reverts.
+
+**Effort:** low–medium. Reuses the existing full-contract oracle conf; these are
+state-gate / single-use rules in the shape the spec already proves.
+
+### 2. Track C — aggregate `claimed ≤ pool` (headline solvency)
+
+The single most valuable unproven property: a round's total reward payouts never exceed its
+voter pool. Research showed this is **easier than the original ghost+hook plan** because the
+aggregate already lives in a scalar:
+
+- `RoundRewardDistributor.roundVoterRewardClaimedAmount[contentId][roundId]` (`:78`) is the
+  running sum, written at `:265` and `:597`; the analogous frontend sum is
+  `roundFrontendClaimedAmount` (`:98`). No `hook Sstore` over a mapping range needed.
+- The bound `voterPool` comes from the engine (`votingEngine.rbtsRoundState(...)`, `:248`),
+  which the distributor specs currently summarize `NONDET`. **Missing piece:** expose
+  `voterPool` deterministically — add a distributor-side harness getter (the
+  `RoundVotingEngineHarness` does not expose it today) — then prove the scalar invariant
+  `roundVoterRewardClaimedAmount[c][r] <= voterPool(c,r)`.
+- Mirror the `LaunchDistributionPoolConservation.spec` idiom (counter already *is* the sum)
+  rather than the hook-heavy `sumOfBalances` pattern.
+
+**Effort:** medium. Main cost is the harness getter + getting the invariant inductive
+(likely needs the `claimedAmount > voterPool` revert at `:256` as an auxiliary fact).
+
+### 3. Track G — CI maturation: required gate + spec-freshness guard
+
+`certora.yaml` is still `workflow_dispatch` + weekly cron, non-gating; the run step warns
+(not fails) when `CERTORAKEY` is unset. Two steps:
+
+- Promote the fast, stable confs (`math`, `cluster-payout-oracle`, `loop-reputation`,
+  `protocol-config`) to a **required, path-filtered PR check**. Keep heavy confs (engine,
+  escrow, the two excluded QRPE confs) on the weekly schedule + send-only so a slow solver
+  never blocks a PR. Keep `fail-fast: false`.
+- Add a lightweight **spec-freshness guard**: a CI check (or `make` target) that fails when a
+  contract with a matching spec is changed in a PR without the spec being touched — this is
+  exactly the drift that produced item 1, and a guard makes it visible instead of silent.
+
+**Effort:** low. Mostly workflow YAML + a small diff-checking script.
+
+### 4. Gambit mutation testing (spec-strength check)
+
+Run `certoraMutate` against the verified confs to measure whether the specs actually catch
+injected bugs (a passing spec over a weak property is false assurance). Start with the
+cleanest harness-based confs (`frontend-registry`, `feedback-bonus-escrow`,
+`loop-reputation`, `math`). Run manually first, record surviving-mutant counts, and only
+wire into CI if runtimes are acceptable. Note: the same via_ir/internal-summary constraints
+apply to the Prover runs Gambit triggers, so prefer the harness-based (non-via_ir) confs.
+
+**Effort:** medium. New tooling surface; value is diagnostic, not a new proof.
+
+### 5. Track B — machine-check `paid ≤ cap` end-to-end (low priority)
+
+`raterLaunchPaid[r] <= raterLaunchCap[r]` is correct by inspection and covered by two proved
+lemmas; only the end-to-end machine proof is missing (nonlinear mul-div the SMT backend won't
+discharge). If wanted: add a small pure CVL lemma proving `a*b/c <= a` for `b <= c` once and
+apply it to the assignment + the `finalizeEarnedRaterRewardCredit` / `unlockFullEarnedRaterCap`
+catch-up paths. Low priority — assurance is already adequate.
+
+### 6. Track D — QRPE no-double-claim without timeout (attempt, time-boxed)
+
+The suggested NONDET-summary of the heavy libraries
+(`QuestionRewardPoolEscrowQualificationLib/ClaimLib/VoterLib/TransferLib`) is **not yet
+applied** — the current specs only NONDET external contract calls. Try it with send-only mode
+(`wait_for_results: NONE`, `global_timeout: 7200`). **Risk:** the escrow needs `via_ir`, under
+which 8.13.1 cannot instrument internal-function summaries — the same wall as Track A may
+apply to internal libraries. Time-box it; if the via_ir/internal-summary error appears, fold
+it into the Track A escalation rather than chasing.
+
+### 7. Track A — escalate, then stop
+
+Confirmed dead-end in 8.13.1 (the latest). File a Certora forum/support issue with the
+already-reduced `_ProbeInternalSummary` repro asking for internal-summary support under
+`solc_optimize + via_ir`, link it from `certora-security-findings.md`, and re-test only when
+8.14+ ships. No further engineering this round.
+
+## Suggested sequencing
+
+```
+1. Oracle spec refresh         ← fresh verification debt, do first
+2. Track C (aggregate ≤ pool)  ← headline solvency, now cheap
+3. Track G (CI gate + freshness guard)  ← lock in the gains, prevent future drift
+   ── then, as budget allows ──
+4. Gambit (spec-strength check)
+5. Track B (paid ≤ cap lemma)  ← low priority
+6. Track D (QRPE, time-boxed)  ← may hit the via_ir wall
+7. Track A (file issue, stop)  ← no engineering
+```
+
+Items 1–3 are the core of this round: they are all tooling-independent, fund- or
+correctness-protecting, and prevent the spec base from rotting against an active contract
+codebase. Items 4–7 are opportunistic.
+
+## Non-goals (unchanged)
+
+Still no whole-protocol proof, no off-chain scorer correctness, no economic-game properties,
+and no fighting the via_ir/internal-summary tooling limit until a new certora-cli ships. This
+round only widens on-chain accounting coverage and keeps the existing proofs honest against a
+moving contract base.
+
+## Sources
+
+- certora-cli releases (8.13.1 is latest, May 19 2026): https://pypi.org/project/certora-cli/ ,
+  https://docs.certora.com/en/latest/docs/prover/changelog/prover_changelog.html
+- CLI options (`function_finder_mode`, `wait_for_results`, `global_timeout`, `nondet_difficult_funcs`):
+  https://docs.certora.com/en/latest/docs/prover/cli/options.html
+- Timeouts guide: https://docs.certora.com/en/latest/docs/user-guide/out-of-resources/timeout.html
+- Ghosts/hooks + native ghost-map summation: https://docs.certora.com/en/latest/docs/cvl/ghosts.html
+- Require-invariants (inductive strengthening): https://docs.certora.com/en/latest/docs/user-guide/patterns/require-invariants.html
+- Gambit / certoraMutate: https://docs.certora.com/en/latest/docs/gambit/index.html , https://github.com/Certora/gambit
diff --git a/docs/testing/certora-security-findings.md b/docs/testing/certora-security-findings.md
index d927ce479..9ff6264b8 100644
--- a/docs/testing/certora-security-findings.md
+++ b/docs/testing/certora-security-findings.md
@@ -10,6 +10,27 @@ vulnerability. Every property that was scoped to a clean, provable slice was pro
 items that could not be proved are **modeling/tooling limitations**, not known bugs —
 they are listed below in full so the gap is explicit rather than hidden.
 
+## Round 3 (`certora-round3-plan.md`)
+
+A third pass (branch `certora-followup-research-3`) refreshed drifted specs and added the
+tooling-independent conservation pieces. **No exploitable vulnerability was found.** New
+machine-checked (cloud-prover) properties: the correlation-epoch rejected-root replay block
+(`cannotReproposeRejectedCorrelationEpochRoot`), the reusable mul-div bound `(a*b)/c <= a`
+(`MulDivLemma.spec`), the launch cap-assignment clamp under `-smt_useNIA`
+(`assignedCapWithinFullCap`), and RoundRewardDistributor accumulator monotonicity. Three
+findings refine the earlier deferral framing:
+
+1. **Oracle spec had drifted** behind three contract commits (new correlation-epoch
+   rejection branches). Not a bug — the existing proofs stayed sound (no signature drift) —
+   but coverage lagged. Closed for the replay branch; a CI `spec-freshness` guard now makes
+   future drift fail the PR instead of going silent.
+2. **QRPE no-double-claim is NOT unblockable by send-only** as the round-2 plan hoped:
+   `_resolveQuestionRewardClaim` is *internal*, so it hits the same via_ir/internal-summary
+   wall as the engine (now escalated — see
+   [`certora-escalation-internal-summary-via-ir.md`](./certora-escalation-internal-summary-via-ir.md)).
+3. **certora-cli 8.13.1 is the latest release**, so the via_ir blockers have no upgrade
+   path today; the escalation is filed and revisited on each cli bump.
+
 ## Round 2 (Tracks B–G of `certora-next-steps.md`)
 
 A second implementation pass added LoopReputation, ProtocolConfig, the
diff --git a/packages/foundry/Makefile b/packages/foundry/Makefile
index 7e28ea8ee..6253ead6b 100644
--- a/packages/foundry/Makefile
+++ b/packages/foundry/Makefile
@@ -1,4 +1,4 @@
-.PHONY: build deploy deploy-and-generate-abis generate-abis get-address account chain compile compile-all flatten fork format lint test verify verify-blockscout slither aderyn certora certora-check coverage check-contract-sizes check-storage-layouts snapshot-storage-layouts
+.PHONY: build deploy deploy-and-generate-abis generate-abis get-address account chain compile compile-all flatten fork format lint test verify verify-blockscout slither aderyn certora certora-check certora-mutate coverage check-contract-sizes check-storage-layouts snapshot-storage-layouts
 
 TEST_ARGS ?=
 COVERAGE_ARGS ?=
@@ -126,6 +126,8 @@ aderyn:
 # "override_base_config" key; certoraRun takes a single conf file.
 CERTORA_CONF ?= certora/confs/math.conf
 CERTORA_ARGS ?=
+# Gambit mutation-testing target (spec strength). See certora/mutation/README.md.
+MUTATION_CONF ?= certora/mutation/frontend-registry.mutation.conf
 
 certora:
 	certoraRun $(CERTORA_CONF) $(CERTORA_ARGS)
@@ -133,6 +135,11 @@ certora:
 certora-check:
 	certoraRun $(CERTORA_CONF) --compilation_steps_only $(CERTORA_ARGS)
 
+# Mutation testing: inject contract mutants and re-verify each against the spec.
+# Needs CERTORAKEY (one prover job per mutant); run manually, not in CI.
+certora-mutate:
+	certoraMutate $(MUTATION_CONF) $(CERTORA_ARGS)
+
 coverage:
 	forge coverage --offline --ir-minimum $(COVERAGE_ARGS)
 
diff --git a/packages/foundry/certora/README.md b/packages/foundry/certora/README.md
index 529c94994..9c15f38af 100644
--- a/packages/foundry/certora/README.md
+++ b/packages/foundry/certora/README.md
@@ -16,6 +16,8 @@ certora/
   confs/
     base.conf                   shared compiler + prover settings (no file targets)
     math.conf                   Phase 1: math-library harness + spec
+    mul-div-lemma.conf          Track B/C: reusable (a*b)/c <= a bound (NIA)
+    round-reward-distributor-conservation.conf  Track C: claimed-amount monotonicity
     cluster-payout-oracle.conf  Phase 2: ClusterPayoutOracle
     round-voting-engine.conf    Phase 3: RoundVotingEngine
     round-reward-distributor.conf  Phase 3: RoundRewardDistributor
@@ -167,6 +169,12 @@ yarn foundry:certora:check
   - Phase 4a (`question-reward-escrow-claim.conf`) — **authored, proof deferred**: the
     claim-flag-never-cleared rule type-checks but the solver exceeds the 15-min window on
     this large contract; not in CI. Run manually with a larger budget.
+  - Track B/C (`mul-div-lemma.conf`) — the reusable nonlinear bound `(a*b)/c <= a` for
+    `b <= c` (enables `-smt_useNIA`). Underpins the per-claimant reward bound and the launch
+    cap clamp.
+  - Track C (`round-reward-distributor-conservation.conf`) — the per-round claimed-amount
+    accumulators are monotone (no clawback/underflow). Full `claimed <= pool` upper bound
+    deferred (needs the engine score-weight model). See `certora-round3-plan.md`.
   - Verified under certora-cli 8.13.1 / solc 0.8.35 ("No errors found by Prover!").
   - See [`docs/testing/certora-followup.md`](../../../docs/testing/certora-followup.md)
     for the phase plan and [`certora-security-findings.md`](../../../docs/testing/certora-security-findings.md)
diff --git a/packages/foundry/certora/confs/launch-distribution-pool-cap.conf b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf
index 39f154a12..b739e0c19 100644
--- a/packages/foundry/certora/confs/launch-distribution-pool-cap.conf
+++ b/packages/foundry/certora/confs/launch-distribution-pool-cap.conf
@@ -5,5 +5,9 @@
   "override_base_config": "certora/confs/base.conf",
   "files": ["certora/harnesses/LaunchDistributionPoolHarness.sol"],
   "verify": "LaunchDistributionPoolHarness:certora/specs/LaunchDistributionPoolCap.spec",
+  // Enable the nonlinear-arithmetic SMT backend so the cap-assignment clamp
+  // (fullCap * bps) / 10000 <= fullCap (rule assignedCapWithinFullCap) is dischargeable;
+  // the default linear backend cannot (see certora-security-findings.md).
+  "prover_args": ["-smt_useNIA true"],
   "msg": "RateLoop Phase 5b LaunchDistributionPool cap invariant"
 }
diff --git a/packages/foundry/certora/confs/mul-div-lemma.conf b/packages/foundry/certora/confs/mul-div-lemma.conf
new file mode 100644
index 000000000..b941850b4
--- /dev/null
+++ b/packages/foundry/certora/confs/mul-div-lemma.conf
@@ -0,0 +1,13 @@
+{
+  // Track B/C primitive: the nonlinear (a*b)/c <= a bound. Inherits compiler/prover
+  // settings from base.conf; overrides via_ir off (pure-arithmetic, no IR codegen
+  // needed, mirrors math.conf) and enables the nonlinear-arithmetic SMT backend so
+  // the multiply-then-divide inequality is dischargeable (see MulDivLemma.spec and
+  // docs/testing/certora-security-findings.md).
+  "override_base_config": "certora/confs/base.conf",
+  "solc_via_ir": false,
+  "files": ["certora/harnesses/MathHarness.sol"],
+  "verify": "MathHarness:certora/specs/MulDivLemma.spec",
+  "prover_args": ["-smt_useNIA true"],
+  "msg": "RateLoop mul-div conservation lemma (Track B/C primitive)"
+}
diff --git a/packages/foundry/certora/confs/question-reward-escrow-claim.conf b/packages/foundry/certora/confs/question-reward-escrow-claim.conf
index 5d5e2918c..14cee2ba0 100644
--- a/packages/foundry/certora/confs/question-reward-escrow-claim.conf
+++ b/packages/foundry/certora/confs/question-reward-escrow-claim.conf
@@ -9,5 +9,12 @@
   "rule_sanity": "none",
   "global_timeout": 7200,
   "prover_args": ["-mediumTimeout 30 -depth 5"],
+  // Track D load-cut (compiler-level auto-summary, not blocked by via_ir): drop the heavy
+  // difficult view/pure internal functions so the claim-flag rule has a chance to complete.
+  // NOTE: the per-commit no-double-claim property itself stays blocked — _resolveQuestionRewardClaim
+  // (QuestionRewardPoolEscrow.sol:1460, called from the claim path at :733) is INTERNAL, not the
+  // external resolver the earlier plan assumed, so it faces the same internal-summary-under-via_ir
+  // wall as the engine (Track A). See docs/testing/certora-round3-plan.md.
+  "nondet_difficult_funcs": true,
   "msg": "RateLoop Phase 4a QuestionRewardPoolEscrow claim flag never cleared"
 }
diff --git a/packages/foundry/certora/confs/question-reward-escrow.conf b/packages/foundry/certora/confs/question-reward-escrow.conf
index f609ff596..52a4c35d6 100644
--- a/packages/foundry/certora/confs/question-reward-escrow.conf
+++ b/packages/foundry/certora/confs/question-reward-escrow.conf
@@ -8,5 +8,10 @@
   // This contract is large (1,490 lines + 11 libraries); the single revert-gate rule does
   // not need the sanity meta-checks, and disabling them keeps the SMT load down.
   "rule_sanity": "none",
+  // Track D load-cut: auto-summarize heuristically-difficult view/pure internal functions
+  // so the solver need not model the whole claim-weight/Merkle callgraph before reaching the
+  // early require(!refunded). This is a compiler-level auto-summary, NOT a CVL internal-
+  // function summary, so it is not blocked by the via_ir limitation (round3-plan Track D).
+  "nondet_difficult_funcs": true,
   "msg": "RateLoop Phase 4 QuestionRewardPoolEscrow refunded-pool claim gate"
 }
diff --git a/packages/foundry/certora/confs/round-reward-distributor-conservation.conf b/packages/foundry/certora/confs/round-reward-distributor-conservation.conf
new file mode 100644
index 000000000..770f04a5b
--- /dev/null
+++ b/packages/foundry/certora/confs/round-reward-distributor-conservation.conf
@@ -0,0 +1,9 @@
+{
+  // Track C (aggregate solvency, slice 1): RoundRewardDistributor per-round claimed-amount
+  // monotonicity (no clawback / no underflow). Inherits compiler/prover settings from
+  // base.conf. Run with: certoraRun certora/confs/round-reward-distributor-conservation.conf
+  "override_base_config": "certora/confs/base.conf",
+  "files": ["contracts/RoundRewardDistributor.sol"],
+  "verify": "RoundRewardDistributor:certora/specs/RoundRewardDistributorConservation.spec",
+  "msg": "RateLoop Track C RoundRewardDistributor conservation (monotonicity slice)"
+}
diff --git a/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol
index 0604bc325..ee0b55ad8 100644
--- a/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol
+++ b/packages/foundry/certora/harnesses/LaunchDistributionPoolHarness.sol
@@ -16,4 +16,13 @@ contract LaunchDistributionPoolHarness is LaunchDistributionPool {
     function unverifiedCapBps_() external view returns (uint256) {
         return uint256(launchRewardPolicy.unverifiedEarnedRaterCapBps);
     }
+
+    /// @notice Exposes the internal cap-assignment so the spec can machine-check the
+    ///         clamp `activeCap <= fullCap` directly at the point it is computed
+    ///         (`activeCap = (fullCap * bps) / BPS_DENOMINATOR`, or `fullCap` when the
+    ///         full cap is unlocked). Uses the live policy, so `unverifiedCapBps_()`
+    ///         is the bps the spec constrains <= 10000. See LaunchDistributionPoolCap.spec.
+    function assignLaunchCap_(address rater, uint256 fullCap) external returns (uint256 activeCap) {
+        (activeCap,) = _assignLaunchCap(rater, fullCap, launchRewardPolicy);
+    }
 }
diff --git a/packages/foundry/certora/mutation/README.md b/packages/foundry/certora/mutation/README.md
new file mode 100644
index 000000000..67c2b4647
--- /dev/null
+++ b/packages/foundry/certora/mutation/README.md
@@ -0,0 +1,55 @@
+# Gambit mutation testing
+
+Mutation testing measures **spec strength**: a passing Certora spec only means "no
+counterexample to the rules as written." It does *not* tell you whether the rules are
+strong enough to catch a real bug. [Gambit](https://docs.certora.com/en/latest/docs/gambit/index.html)
+(bundled with `certora-cli`) answers that — it injects small mutations into a contract
+and `certoraMutate` re-runs the Prover against each mutant:
+
+- a **killed** mutant = a rule failed on the broken code = the spec caught it (good);
+- a **surviving** mutant = every rule still passed on broken code = the spec
+  under-constrains that line (a weak-spec signal to investigate — *not* a contract bug).
+
+## Running
+
+Each mutant is a full Prover job, so this needs `CERTORAKEY` and is run **manually**, not
+in CI. From `packages/foundry`:
+
+```sh
+export CERTORAKEY=<personal_access_key>
+
+make certora-mutate                                            # default: FrontendRegistry
+make certora-mutate MUTATION_CONF=certora/mutation/feedback-bonus-escrow.mutation.conf
+make certora-mutate MUTATION_CONF=certora/mutation/reward-math.mutation.conf
+
+# or directly:
+certoraMutate certora/mutation/frontend-registry.mutation.conf
+```
+
+`certoraMutate` prints a dashboard link; the report lists each mutant and whether it was
+killed or survived.
+
+## Targets chosen first
+
+The confs here are the cleanest starting points — all **harness-based and `via_ir`-free**,
+so they dodge the internal-summary tooling limits that block the heavier contracts, and
+their proofs are fast enough for a full mutant sweep:
+
+| Mutation conf | Contract mutated | Spec under test |
+|---|---|---|
+| `frontend-registry.mutation.conf` | `FrontendRegistry.sol` | stake/slash conservation |
+| `feedback-bonus-escrow.mutation.conf` | `FeedbackBonusEscrow.sol` | bonus conservation + single-award |
+| `reward-math.mutation.conf` | `libraries/RewardMath.sol` | Math.spec conservation/bounds/monotonicity |
+
+## Interpreting results
+
+Record surviving-mutant counts per run. A survivor usually means one of:
+
+1. the mutated line is not covered by any rule → add a rule, or
+2. a rule is too weak (e.g. asserts `>= 0` where `<= cap` was intended) → tighten it, or
+3. the mutation is equivalent (semantically identical code) → no action, note it.
+
+Only wire a target into CI once its runtime is known and its survivor set is triaged to
+"covered or equivalent". Heavy / `via_ir` contracts (engine, escrow) are intentionally not
+listed yet — the same internal-summary constraints from the proof lane apply to the
+Prover runs Gambit triggers.
diff --git a/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf b/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf
new file mode 100644
index 000000000..4c6f4362d
--- /dev/null
+++ b/packages/foundry/certora/mutation/feedback-bonus-escrow.mutation.conf
@@ -0,0 +1,17 @@
+{
+  // Gambit mutation run for the FeedbackBonusEscrow conservation proofs.
+  // See certora/mutation/README.md and frontend-registry.mutation.conf for how
+  // surviving mutants are interpreted (weak-spec signal).
+  //
+  // Run from packages/foundry (needs CERTORAKEY):
+  //   certoraMutate certora/mutation/feedback-bonus-escrow.mutation.conf
+  "prover_conf": "certora/confs/feedback-bonus-escrow.conf",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "contracts/FeedbackBonusEscrow.sol"
+      }
+    ]
+  },
+  "msg": "FeedbackBonusEscrow spec-strength mutation run"
+}
diff --git a/packages/foundry/certora/mutation/frontend-registry.mutation.conf b/packages/foundry/certora/mutation/frontend-registry.mutation.conf
new file mode 100644
index 000000000..168a0a253
--- /dev/null
+++ b/packages/foundry/certora/mutation/frontend-registry.mutation.conf
@@ -0,0 +1,22 @@
+{
+  // Gambit mutation run for the FrontendRegistry stake/slash proofs.
+  // Measures whether FrontendRegistry.spec actually CATCHES injected bugs: Gambit
+  // generates mutants of the contract, and certoraMutate verifies each against the
+  // spec via the Prover. A SURVIVING mutant (all rules still pass on broken code)
+  // means the spec under-constrains that line — a weak-spec signal, not a contract bug.
+  //
+  // Run from packages/foundry (needs CERTORAKEY — each mutant is a full prover job):
+  //   certoraMutate certora/mutation/frontend-registry.mutation.conf
+  //
+  // Chosen as a first target because it is harness-based and via_ir-free (no internal-
+  // summary tooling limits) and the proofs are fast, so a full mutant sweep is cheap.
+  "prover_conf": "certora/confs/frontend-registry.conf",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "contracts/FrontendRegistry.sol"
+      }
+    ]
+  },
+  "msg": "FrontendRegistry spec-strength mutation run"
+}
diff --git a/packages/foundry/certora/mutation/reward-math.mutation.conf b/packages/foundry/certora/mutation/reward-math.mutation.conf
new file mode 100644
index 000000000..2cc94c11f
--- /dev/null
+++ b/packages/foundry/certora/mutation/reward-math.mutation.conf
@@ -0,0 +1,17 @@
+{
+  // Gambit mutation run for the pure math libraries (Math.spec). Mutating RewardMath
+  // exercises the conservation/bounds/monotonicity rules and the calculateVoterReward
+  // path that the mul-div lemma underpins. via_ir-free and fast.
+  //
+  // Run from packages/foundry (needs CERTORAKEY):
+  //   certoraMutate certora/mutation/reward-math.mutation.conf
+  "prover_conf": "certora/confs/math.conf",
+  "mutations": {
+    "gambit": [
+      {
+        "filename": "contracts/libraries/RewardMath.sol"
+      }
+    ]
+  },
+  "msg": "RewardMath spec-strength mutation run"
+}
diff --git a/packages/foundry/certora/scripts/check_spec_freshness.py b/packages/foundry/certora/scripts/check_spec_freshness.py
new file mode 100755
index 000000000..5f445e118
--- /dev/null
+++ b/packages/foundry/certora/scripts/check_spec_freshness.py
@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""Spec-freshness guard for the Certora lane.
+
+Fails when a contract that has Certora coverage is changed in a PR without its
+spec being touched — the exact drift that left ClusterPayoutOracle.spec stale
+behind three contract commits (see docs/testing/certora-round3-plan.md, Track G).
+
+The contract -> spec(s) map is derived from the conf files themselves (no second
+source of truth to keep in sync):
+  - each conf's `verify` key names the spec;
+  - each conf's `files` list names the verification targets. A target under
+    contracts/ is a direct dependency; a target under certora/harnesses/ is
+    resolved to the contracts/ files it imports, so harness-based confs
+    (FrontendRegistry, FeedbackBonusEscrow, ...) are covered too.
+
+Usage:
+    check_spec_freshness.py --changed-from <git-ref>      # diff <ref>...HEAD
+    check_spec_freshness.py --changed-file <path>         # newline-listed paths
+    git diff --name-only BASE...HEAD | check_spec_freshness.py --changed-stdin
+
+Escape hatch (for intentional contract-only changes that don't affect proven
+properties): include the literal token [spec-ok] anywhere in the environment
+variable SPEC_FRESHNESS_OVERRIDE (the workflow wires this to the PR title/body).
+"""
+
+from __future__ import annotations
+
+import argparse
+import json
+import os
+import posixpath
+import re
+import subprocess
+import sys
+from pathlib import Path
+
+# Repo-root-relative location of the foundry package and the certora workspace.
+FOUNDRY = "packages/foundry"
+CONFS_DIR = Path(FOUNDRY) / "certora" / "confs"
+
+
+def strip_jsonc(text: str) -> str:
+    """Remove // line comments so the commented conf files parse as JSON."""
+    out = []
+    for line in text.splitlines():
+        # Only strip // that is not inside a string. The confs only ever use //
+        # at the start of a (possibly indented) line or after a value, never
+        # inside string literals, so a simple heuristic is safe here.
+        in_str = False
+        result = []
+        i = 0
+        while i < len(line):
+            ch = line[i]
+            if ch == '"':
+                in_str = not in_str
+            if not in_str and ch == "/" and i + 1 < len(line) and line[i + 1] == "/":
+                break
+            result.append(ch)
+            i += 1
+        out.append("".join(result))
+    return "\n".join(out)
+
+
+def _is_library(rel: str) -> bool:
+    return rel.startswith("contracts/libraries/")
+
+
+def _resolve_imports(file_rel: str) -> list[str]:
+    """FOUNDRY-relative contracts/ files imported by file_rel (relative imports only).
+
+    Remapped imports (@openzeppelin/..., etc.) resolve outside contracts/ and are dropped.
+    """
+    path = Path(FOUNDRY) / file_rel
+    if not path.exists():
+        return []
+    base = posixpath.dirname(file_rel)
+    out: list[str] = []
+    # Matches `import "X";`, `import {a,b} from "X";`, `import * as N from "X";`.
+    for m in re.finditer(r'import\s+(?:[^"\';]*?\sfrom\s+)?"([^"]+)"', path.read_text()):
+        resolved = posixpath.normpath(posixpath.join(base, m.group(1)))
+        if resolved.startswith("contracts/") and (Path(FOUNDRY) / resolved).exists():
+            out.append(resolved)
+    return out
+
+
+def contract_deps(target_rel: str) -> set[str]:
+    """The contracts/ files whose code is compiled INTO a conf target's verification.
+
+    Starts from the target (a contracts/ file or a certora/harnesses/ harness) and walks
+    imports transitively, but only follows into LIBRARIES (contracts/libraries/**) — and,
+    from a harness, into the one full contract it wraps. Sibling full contracts reached
+    through an import are NOT included: the specs summarize those as external NONDET calls,
+    so a change to them cannot alter what is proved here. Libraries, by contrast, are linked
+    in and ARE part of the verified behavior (e.g. FrontendFeeDustLib in the distributor's
+    dust path), so a change to one must re-trip the freshness guard.
+    """
+    deps: set[str] = set()
+    seen: set[str] = set()
+    # A harness is not itself a contracts/ file, so it is a walk root but never a dep.
+    stack = [target_rel]
+    if target_rel.startswith("contracts/"):
+        deps.add(target_rel)
+    while stack:
+        node = stack.pop()
+        if node in seen:
+            continue
+        seen.add(node)
+        node_is_harness = not node.startswith("contracts/")
+        for imp in _resolve_imports(node):
+            follow = _is_library(imp) or node_is_harness  # harness -> its wrapped contract
+            if not follow:
+                continue  # sibling full contract: summarized, out of scope
+            deps.add(imp)
+            stack.append(imp)
+    return deps
+
+
+def build_map() -> dict[str, set[str]]:
+    """contract path (FOUNDRY-relative) -> set of spec paths (FOUNDRY-relative)."""
+    mapping: dict[str, set[str]] = {}
+    for conf in sorted(CONFS_DIR.glob("*.conf")):
+        if conf.name == "base.conf":
+            continue
+        data = json.loads(strip_jsonc(conf.read_text()))
+        verify = data.get("verify", "")
+        if ":" not in verify:
+            continue
+        spec = verify.split(":", 1)[1]
+        deps: set[str] = set()
+        for target in data.get("files", []):
+            if target.startswith("contracts/") or "harnesses/" in target:
+                deps.update(contract_deps(target))
+        for dep in deps:
+            mapping.setdefault(dep, set()).add(spec)
+    return mapping
+
+
+def changed_files(args: argparse.Namespace) -> list[str]:
+    if args.changed_stdin:
+        return [l.strip() for l in sys.stdin if l.strip()]
+    if args.changed_file:
+        return [l.strip() for l in Path(args.changed_file).read_text().splitlines() if l.strip()]
+    if args.changed_from:
+        out = subprocess.run(
+            ["git", "diff", "--name-only", f"{args.changed_from}...HEAD"],
+            capture_output=True, text=True, check=True,
+        ).stdout
+        return [l.strip() for l in out.splitlines() if l.strip()]
+    raise SystemExit("one of --changed-from/--changed-file/--changed-stdin is required")
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--changed-from", help="git ref; diff <ref>...HEAD for changed files")
+    parser.add_argument("--changed-file", help="file containing newline-separated changed paths")
+    parser.add_argument("--changed-stdin", action="store_true", help="read changed paths from stdin")
+    args = parser.parse_args()
+
+    override = os.environ.get("SPEC_FRESHNESS_OVERRIDE", "")
+    if "[spec-ok]" in override:
+        print("spec-freshness: [spec-ok] override present — skipping check.")
+        return 0
+
+    mapping = build_map()
+    changed = set(changed_files(args))
+    # Normalize conf-relative (FOUNDRY-relative) paths to repo-root-relative.
+    changed_foundry = {
+        c[len(FOUNDRY) + 1:] for c in changed if c.startswith(FOUNDRY + "/")
+    }
+
+    stale: list[tuple[str, list[str]]] = []
+    for contract, specs in sorted(mapping.items()):
+        if contract not in changed_foundry:
+            continue
+        if specs & changed_foundry:
+            continue  # at least one covering spec was touched — OK
+        stale.append((contract, sorted(specs)))
+
+    if not stale:
+        print("spec-freshness: OK — every changed covered contract had its spec reviewed.")
+        return 0
+
+    print("spec-freshness: FAIL — covered contract(s) changed without touching the spec.\n")
+    for contract, specs in stale:
+        spec_list = ", ".join(s.replace("certora/specs/", "") for s in specs)
+        msg = f"{contract} changed but its Certora spec(s) were not: {spec_list}"
+        print(f"  - {msg}")
+        # GitHub Actions annotation.
+        print(f"::error file={FOUNDRY}/{contract}::{msg}")
+    print(
+        "\nReview the spec against the contract change. If the change genuinely does "
+        "not affect any proven property, add [spec-ok] to the PR title or body to bypass."
+    )
+    return 1
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/packages/foundry/certora/specs/ClusterPayoutOracle.spec b/packages/foundry/certora/specs/ClusterPayoutOracle.spec
index 94e409340..8ec79fec8 100644
--- a/packages/foundry/certora/specs/ClusterPayoutOracle.spec
+++ b/packages/foundry/certora/specs/ClusterPayoutOracle.spec
@@ -10,6 +10,10 @@
  *     to imply every gate held (pure view properties over arbitrary state).
  *   - rejected-root non-reuse: a blacklisted (snapshotKey, weightRoot) can never be
  *     re-proposed (proposeRoundPayoutSnapshot reverts).
+ *   - rejected correlation-epoch root non-reuse (L-Oracle-4, commit 10ded66c): once an
+ *     epoch's clusterRoot is on the rejected-root blacklist, proposeCorrelationEpoch for
+ *     that exact (epochId, clusterRoot) always reverts. This covers the explicit-root
+ *     rejection path added by rejectCorrelationEpochRoot / rejectFinalizedCorrelationEpochRoot.
  *   - single-use bond-credit withdrawal: a withdrawal zeroes the caller's credit and
  *     an empty withdrawal reverts, so a credit is drawable at most once.
  *
@@ -18,6 +22,11 @@
  *   - rejected digest non-reuse and the consumed-slot permanent-death guard
  *   - challenge-window finalization timing
  *   - parent correlation-epoch rejection cascade
+ *   - the metadata-vs-root rejection split (rejectCorrelationEpoch keeps the deterministic
+ *     root re-proposable; only the *Root variants blacklist it) — proving the metadata path
+ *     does NOT blacklist needs a getter for the snapshot's stored clusterRoot (private struct)
+ *   - the disinterested-challenger guard (a proposer/frontend-operator cannot self-challenge,
+ *     commit 808570b3) — reads the private snapshot struct's proposer/frontendOperator fields
  * See docs/testing/certora.md (Phase 2).
  */
 
@@ -31,6 +40,8 @@ methods {
     function rejectedRoundPayoutSnapshotDigests(bytes32, bytes32) external returns (bool) envfree;
     function rejectedRoundPayoutSnapshotConsumed(bytes32) external returns (bool) envfree;
     function rejectedCorrelationEpochRoots(uint256, bytes32) external returns (bool) envfree;
+    function rejectedCorrelationEpochRootKeys(bytes32) external returns (bool) envfree;
+    function rejectedCorrelationEpochSnapshotDigests(uint256, bytes32) external returns (bool) envfree;
 
     // Summarize the external dependencies (frontend registry, snapshot consumer,
     // bond ERC20) as NONDET so a call to them cannot havoc THIS contract's storage.
@@ -48,7 +59,7 @@ methods {
 // ---------------------------------------------------------------------------
 // Rejected roots cannot be reused: once a (snapshotKey, weightRoot) pair is on
 // the rejected-root blacklist, proposeRoundPayoutSnapshot for that exact root
-// always reverts (guard at ClusterPayoutOracle.sol:385). The blacklists are only
+// always reverts (guard at ClusterPayoutOracle.sol:429). The blacklists are only
 // ever written `true` and never cleared, so a rejected root stays unproposable.
 // ---------------------------------------------------------------------------
 
@@ -59,6 +70,37 @@ rule cannotReproposeRejectedRoot(env e, IClusterPayoutOracle.RoundPayoutSnapshot
     assert lastReverted;
 }
 
+// ---------------------------------------------------------------------------
+// Same guarantee one level up, for correlation epochs (L-Oracle-4, commit
+// 10ded66c "Block replay of rejected correlation roots"): once an epoch's
+// clusterRoot is blacklisted via rejectCorrelationEpochRoot /
+// rejectFinalizedCorrelationEpochRoot, proposeCorrelationEpoch for that exact
+// (epochId, clusterRoot) always reverts at the guard on
+// ClusterPayoutOracle.sol:267-272. This is the contrapositive of that guard's
+// first disjunct; the blacklist is only ever written `true`, so the block is
+// permanent. (The second disjunct — the source-set-keyed rootKeys mapping — is
+// not asserted here because its key derives from the internally-computed
+// sourceSetDigest, which cannot be matched from calldata.)
+// ---------------------------------------------------------------------------
+
+rule cannotReproposeRejectedCorrelationEpochRoot(
+    env e,
+    uint64 epochId,
+    uint64 fromRoundId,
+    uint64 toRoundId,
+    bytes32 clusterRoot,
+    bytes32 parameterHash,
+    bytes32 artifactHash,
+    string artifactURI,
+    IClusterPayoutOracle.CorrelationEpochSourceRef[] sourceRefs
+) {
+    require rejectedCorrelationEpochRoots(require_uint256(epochId), clusterRoot);
+    proposeCorrelationEpoch@withrevert(
+        e, epochId, fromRoundId, toRoundId, clusterRoot, parameterHash, artifactHash, artifactURI, sourceRefs
+    );
+    assert lastReverted;
+}
+
 // ---------------------------------------------------------------------------
 // Bond-credit withdrawal is single-use: a successful withdrawal zeroes the
 // caller's credit, and a withdrawal with no credit reverts. Together these mean a
diff --git a/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec
index 7c25cf7c6..6d7bb6663 100644
--- a/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec
+++ b/packages/foundry/certora/specs/LaunchDistributionPoolCap.spec
@@ -13,13 +13,20 @@
  *   capAssignedWhenPaid — any rater with a non-zero paid-out amount has an assigned cap
  *                         (every payout path assigns the cap before paying).
  *
- * The headline `raterLaunchPaid <= raterLaunchCap` itself remains deferred. Its last
- * missing lemma is `raterLaunchCap <= raterFullLaunchCap`, which at assignment reduces to
- * `fullCap * bps / 10000 <= fullCap` given `bps <= 10000`. That is a nonlinear
- * multiply-then-divide inequality, which the SMT backend cannot discharge precisely (a
- * solver-completeness limit, not a contract defect — by inspection the clamp is correct).
- * Proving it would need a manual nonlinear lemma or a mul-div abstraction. The two
- * invariants below are the sound, machine-checked part of the chain.
+ * The previously-deferred lemma `raterLaunchCap <= raterFullLaunchCap` reduces at
+ * assignment to `fullCap * bps / 10000 <= fullCap` given `bps <= 10000` — a nonlinear
+ * multiply-then-divide the *linear* SMT backend cannot discharge. This conf now enables
+ * the nonlinear-arithmetic backend (`-smt_useNIA`), under which the assignment clamp IS
+ * dischargeable (docs/testing/certora-security-findings.md confirmed NIA discharges the
+ * assignment multiply). `assignedCapWithinFullCap` below machine-checks exactly that clamp
+ * at the point it is computed, via the harness wrapper `assignLaunchCap_`.
+ *
+ * Still deferred (honest residual): the *global* invariant `raterLaunchPaid <= raterLaunchCap`
+ * over every method. Per the findings doc, even with NIA the catch-up paths
+ * (finalizeEarnedRaterRewardCredit / unlockFullEarnedRaterCap) — which contain further
+ * cap * count / rewardingCount mul-div sites — still resist as a standalone inductive
+ * invariant. So this slice proves the per-assignment clamp (the load-bearing step) rather
+ * than the end-to-end invariant. See docs/testing/certora-round3-plan.md (Track B).
  */
 
 methods {
@@ -44,3 +51,14 @@ invariant policyBpsBounded()
 // Any rater that has been paid has an assigned cap (every payout path assigns first).
 invariant capAssignedWhenPaid(address r)
     raterLaunchPaid(r) > 0 => raterLaunchCapAssigned(r);
+
+// The cap-assignment clamp: the active cap computed at assignment never exceeds the full
+// cap. This is the load-bearing mul-div step (activeCap = (fullCap * bps) / 10000 when the
+// full cap is locked, else fullCap), the real-contract instance of MulDivLemma.spec's
+// `(a*b)/c <= a`. Requires the nonlinear SMT backend enabled in this conf. The bps
+// precondition is `policyBpsBounded`, proved as an invariant above.
+rule assignedCapWithinFullCap(env e, address rater, uint256 fullCap) {
+    requireInvariant policyBpsBounded();
+    uint256 activeCap = assignLaunchCap_(e, rater, fullCap);
+    assert activeCap <= fullCap;
+}
diff --git a/packages/foundry/certora/specs/MulDivLemma.spec b/packages/foundry/certora/specs/MulDivLemma.spec
new file mode 100644
index 000000000..ad2d4d8d7
--- /dev/null
+++ b/packages/foundry/certora/specs/MulDivLemma.spec
@@ -0,0 +1,55 @@
+/*
+ * MulDivLemma.spec — reusable nonlinear multiply-then-divide bound.
+ *
+ * Proves the floor-division primitive `(a * b) / c <= a` for `b <= c`, `c != 0`
+ * (and the exact corollary `(a * c) / c == a`). This is the single arithmetic
+ * fact that every "a proportional share never exceeds its pool/cap" conservation
+ * property in the protocol reduces to:
+ *
+ *   - RewardMath.calculateVoterReward = (voterPool * stake) / totalStake
+ *         <= voterPool           when stake <= totalStake   (RoundRewardDistributor)
+ *   - LaunchDistributionPool cap  = (fullCap * bps) / 10000
+ *         <= fullCap             when bps  <= 10000          (Track B)
+ *
+ * docs/testing/certora-security-findings.md records `(fullCap * bps) / 10000 <= fullCap`
+ * as a deferred gap because the default *linear* SMT backend cannot discharge a
+ * nonlinear multiply-then-divide. That doc's own re-run note ("`-smt_useNIA` ...
+ * discharged the assignment multiplication") is the evidence this lemma is provable
+ * once nonlinear arithmetic is enabled — which this conf does via prover_args.
+ *
+ * The rule calls no contract function: it is pure CVL integer arithmetic over the
+ * mathematical integers (to_mathint avoids any 256-bit wraparound, so the bound is
+ * the true mathematical one, which equals the EVM result on the non-overflowing
+ * inputs these formulas are fed). MathHarness is named only because `verify` needs
+ * a contract to attach to.
+ */
+
+methods {
+    // No contract methods are exercised; the lemma is self-contained arithmetic.
+}
+
+// Floor of (a*b)/c is at most a whenever b <= c (c != 0). The workhorse lemma.
+rule mulDivAtMost(uint256 a, uint256 b, uint256 c) {
+    require c != 0;
+    require b <= c;
+    mathint product = to_mathint(a) * to_mathint(b);
+    assert product / to_mathint(c) <= to_mathint(a);
+}
+
+// Exact corollary: a full-fraction allocation (b == c) returns a unchanged. This
+// is the boundary the cap/pool clamps lean on (full cap, 100% bps, last claimant).
+rule mulDivExactWhenFull(uint256 a, uint256 c) {
+    require c != 0;
+    mathint product = to_mathint(a) * to_mathint(c);
+    assert product / to_mathint(c) == to_mathint(a);
+}
+
+// Monotonicity in the numerator factor: a larger share weight never yields a
+// smaller payout. Underpins "a claimant's reward tracks its weight" reasoning.
+rule mulDivMonotoneInB(uint256 a, uint256 b1, uint256 b2, uint256 c) {
+    require c != 0;
+    require b1 <= b2;
+    mathint p1 = to_mathint(a) * to_mathint(b1);
+    mathint p2 = to_mathint(a) * to_mathint(b2);
+    assert p1 / to_mathint(c) <= p2 / to_mathint(c);
+}
diff --git a/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec
new file mode 100644
index 000000000..84249daee
--- /dev/null
+++ b/packages/foundry/certora/specs/RoundRewardDistributorConservation.spec
@@ -0,0 +1,102 @@
+/*
+ * RoundRewardDistributorConservation.spec — Track C (aggregate solvency, slice 1).
+ *
+ * Verification target: contracts/RoundRewardDistributor.sol (verified directly).
+ * Run with:           certoraRun certora/confs/round-reward-distributor-conservation.conf
+ *
+ * The headline solvency property is "the sum of all voter-reward payouts for a round
+ * never exceeds that round's voterPool". The running sum lives in the scalar slot
+ * roundVoterRewardClaimedAmount[contentId][roundId] (written at RoundRewardDistributor.sol
+ * :265 as `claimedAmount + reward` and at :597 as `+= releasedDust`), so the property is
+ * `roundVoterRewardClaimedAmount[c][r] <= voterPool(c,r)`.
+ *
+ * What is proved here (engine-model-free, robust):
+ *   - the accumulator is MONOTONE: neither a voter claim nor dust finalization can ever
+ *     decrease it. Every write adds a non-negative amount or reverts. This is the
+ *     no-clawback / no-underflow half of conservation and the inductive scaffold the
+ *     upper bound builds on.
+ *
+ * Why the upper bound itself is NOT proved here (deferred, with the gap made explicit):
+ *   The per-claimant increment is a PROPORTIONAL share,
+ *   reward = RewardMath.calculateVoterReward(scoreWeight, totalScoreWeight, voterPool)
+ *          = (voterPool * scoreWeight) / totalScoreWeight,
+ *   so `sum(reward) <= voterPool` holds only because `sum(scoreWeight) <= totalScoreWeight`
+ *   across claimants — an aggregate over engine state, not a distributor-storage fact.
+ *   The two pieces it factors into ARE addressed elsewhere:
+ *     - the single-claimant bound `(voterPool * scoreWeight)/totalScoreWeight <= voterPool`
+ *       (for scoreWeight <= totalScoreWeight) is the mul-div lemma in MulDivLemma.spec;
+ *     - the last-claimant settlement pays exactly `voterPool - claimedAmount` (:262),
+ *       landing the sum on voterPool exactly.
+ *   The remaining gap is the score-weight summation invariant across the engine's
+ *   per-commit state, which needs a faithful engine model rather than the NONDET
+ *   summaries used here. Tracked in docs/testing/certora-round3-plan.md (Track C).
+ *
+ * The engine payout (transferReward) and the LREP token transfer are summarized NONDET
+ * exactly as RoundRewardDistributor.spec does: the distributor never custodies rewards,
+ * so those calls cannot write its accumulators, and havoc'd engine view returns only make
+ * the monotonicity argument stronger (it holds for every possible voterPool).
+ */
+
+methods {
+    function roundVoterRewardClaimedAmount(uint256, uint256) external returns (uint256) envfree;
+    function roundFrontendClaimedAmount(uint256, uint256) external returns (uint256) envfree;
+
+    function _.transferReward(address, uint256) external => NONDET;
+    function _.transfer(address, uint256) external => NONDET;
+}
+
+// A voter claim never decreases the per-round claimed-amount accumulator (any round).
+// The only write is `claimedAmount + reward` with reward >= 0; every other path reverts.
+rule claimRewardNeverDecreasesClaimedAmount(env e, uint256 contentId, uint256 roundId, uint256 c, uint256 r) {
+    uint256 before = roundVoterRewardClaimedAmount(c, r);
+    claimReward(e, contentId, roundId);
+    assert roundVoterRewardClaimedAmount(c, r) >= before;
+}
+
+// Dust finalization never decreases the accumulator either: it adds releasedDust (> 0,
+// or the call reverts with NoRewardDust). Together with the rule above, the per-round
+// voter-reward sum is non-decreasing across the whole claim lifecycle.
+rule dustFinalizationNeverDecreasesClaimedAmount(
+    env e,
+    uint256 contentId,
+    uint256 roundId,
+    address[] sortedWinningVoters,
+    uint256 c,
+    uint256 r
+) {
+    uint256 before = roundVoterRewardClaimedAmount(c, r);
+    finalizeVoterRewardDust(e, contentId, roundId, sortedWinningVoters);
+    assert roundVoterRewardClaimedAmount(c, r) >= before;
+}
+
+// Symmetric monotonicity for the frontend-fee accumulator (RoundRewardDistributor.sol:98),
+// which follows the same add-or-revert discipline as the voter accumulator: the only writes
+// are `+= fee` (_consumeFrontendFeeClaim, :750) and `+= releasedDust` (_finalizeProcessed-
+// FrontendFeeDust, :914). Targeted at the three public mutators rather than written as one
+// parametric rule over every method: a free parametric rule over this via_ir, struct-heavy
+// contract yields a spurious counterexample from an unreachable havoc prestate (the known
+// auto-finder artifact documented in certora-security-findings.md), even though every real
+// write only adds. The targeted rules below verify cleanly.
+rule claimFrontendFeeNeverDecreasesClaimedAmount(
+    env e, uint256 contentId, uint256 roundId, address frontend, uint256 c, uint256 r
+) {
+    uint256 before = roundFrontendClaimedAmount(c, r);
+    claimFrontendFee(e, contentId, roundId, frontend);
+    assert roundFrontendClaimedAmount(c, r) >= before;
+}
+
+// NOTE: the public `finalizeFrontendFeeDust(.. address[] sortedFrontends)` wrapper is
+// intentionally NOT given its own rule. Its only write to roundFrontendClaimedAmount is the
+// `+= releasedDust` inside _finalizeProcessedFrontendFeeDust — already covered by the rule
+// below — but it first runs the _processFrontendFeeDustBatch loop over the sorted-frontend
+// array, whose deep internal calls hit the via_ir auto-finder instrumentation gap and
+// produce a spurious "decrease" counterexample from an unreachable havoc state (the artifact
+// documented in certora-security-findings.md). Covering the underlying writer directly keeps
+// the proof sound without that false positive.
+rule finalizeProcessedFrontendFeeDustNeverDecreasesClaimedAmount(
+    env e, uint256 contentId, uint256 roundId, uint256 c, uint256 r
+) {
+    uint256 before = roundFrontendClaimedAmount(c, r);
+    finalizeProcessedFrontendFeeDust(e, contentId, roundId);
+    assert roundFrontendClaimedAmount(c, r) >= before;
+}
diff --git a/packages/foundry/contracts/ClusterPayoutOracle.sol b/packages/foundry/contracts/ClusterPayoutOracle.sol
index 3b327d8f5..88decf8c7 100644
--- a/packages/foundry/contracts/ClusterPayoutOracle.sol
+++ b/packages/foundry/contracts/ClusterPayoutOracle.sol
@@ -1,15 +1,15 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.34;
 
-import {AccessControl} from "@openzeppelin/contracts/access/AccessControl.sol";
-import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
-import {SafeERC20} from "@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol";
-import {MerkleProof} from "@openzeppelin/contracts/utils/cryptography/MerkleProof.sol";
-import {SafeCast} from "@openzeppelin/contracts/utils/math/SafeCast.sol";
-import {ReentrancyGuard} from "@openzeppelin/contracts/utils/ReentrancyGuard.sol";
-import {IClusterPayoutOracle} from "./interfaces/IClusterPayoutOracle.sol";
-import {IFrontendRegistry} from "./interfaces/IFrontendRegistry.sol";
-import {IRoundPayoutSnapshotConsumer} from "./interfaces/IRoundPayoutSnapshotConsumer.sol";
+import { AccessControl } from "@openzeppelin/contracts/access/AccessControl.sol";
+import { IERC20 } from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import { SafeERC20 } from "@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol";
+import { MerkleProof } from "@openzeppelin/contracts/utils/cryptography/MerkleProof.sol";
+import { SafeCast } from "@openzeppelin/contracts/utils/math/SafeCast.sol";
+import { ReentrancyGuard } from "@openzeppelin/contracts/utils/ReentrancyGuard.sol";
+import { IClusterPayoutOracle } from "./interfaces/IClusterPayoutOracle.sol";
+import { IFrontendRegistry } from "./interfaces/IFrontendRegistry.sol";
+import { IRoundPayoutSnapshotConsumer } from "./interfaces/IRoundPayoutSnapshotConsumer.sol";
 
 /// @title ClusterPayoutOracle
 /// @notice Optimistic oracle for correlation epoch snapshots and per-round payout weights.
@@ -1114,7 +1114,7 @@ contract ClusterPayoutOracle is IClusterPayoutOracle, AccessControl, ReentrancyG
         if (challenger == proposer || challenger == frontendOperator) revert InvalidSnapshot();
         try frontendRegistry.isAuthorizedSnapshotProposer(frontendOperator, challenger) returns (bool authorized) {
             if (authorized) revert InvalidSnapshot();
-        } catch {}
+        } catch { }
     }
 
     function _creditBond(address to, uint256 amount) private {
@@ -1131,17 +1131,17 @@ contract ClusterPayoutOracle is IClusterPayoutOracle, AccessControl, ReentrancyG
         } catch {
             revert InvalidAddress();
         }
-        try IFrontendRegistry(newFrontendRegistry).isEligible(address(0)) returns (bool) {}
+        try IFrontendRegistry(newFrontendRegistry).isEligible(address(0)) returns (bool) { }
         catch {
             revert InvalidAddress();
         }
-        try IFrontendRegistry(newFrontendRegistry).authorizedSnapshotFrontend(address(0)) returns (address) {}
+        try IFrontendRegistry(newFrontendRegistry).authorizedSnapshotFrontend(address(0)) returns (address) { }
         catch {
             revert InvalidAddress();
         }
         try IFrontendRegistry(newFrontendRegistry).isAuthorizedSnapshotProposer(address(0), address(0)) returns (
             bool
-        ) {}
+        ) { }
         catch {
             revert InvalidAddress();
         }
diff --git a/packages/foundry/test/ClusterPayoutOracle.t.sol b/packages/foundry/test/ClusterPayoutOracle.t.sol
index 8e6a38f2b..e9d9b41db 100644
--- a/packages/foundry/test/ClusterPayoutOracle.t.sol
+++ b/packages/foundry/test/ClusterPayoutOracle.t.sol
@@ -1,10 +1,10 @@
 // SPDX-License-Identifier: MIT
 pragma solidity ^0.8.34;
 
-import {Test} from "forge-std/Test.sol";
-import {ClusterPayoutOracle} from "../contracts/ClusterPayoutOracle.sol";
-import {IClusterPayoutOracle} from "../contracts/interfaces/IClusterPayoutOracle.sol";
-import {MockERC20} from "../contracts/mocks/MockERC20.sol";
+import { Test } from "forge-std/Test.sol";
+import { ClusterPayoutOracle } from "../contracts/ClusterPayoutOracle.sol";
+import { IClusterPayoutOracle } from "../contracts/interfaces/IClusterPayoutOracle.sol";
+import { MockERC20 } from "../contracts/mocks/MockERC20.sol";
 
 function _questionEpochSources(uint256 rewardPoolId, uint256 contentId, uint256 roundId)
     pure
@@ -43,7 +43,7 @@ contract ClusterPayoutOracleTest is Test {
     MockRoundPayoutSnapshotConsumer internal launchConsumer;
     MockERC20 internal usdc;
 
-    receive() external payable {}
+    receive() external payable { }
 
     function setUp() public {
         usdc = new MockERC20("USD Coin", "USDC", 6);
@@ -179,7 +179,7 @@ contract ClusterPayoutOracleTest is Test {
 
     function test_ProposalsDoNotAcceptEthBonds() public {
         vm.expectRevert(ClusterPayoutOracle.InvalidBond.selector);
-        oracle.proposeCorrelationEpoch{value: 1}(
+        oracle.proposeCorrelationEpoch{ value: 1 }(
             1,
             1,
             20,
@@ -1381,7 +1381,7 @@ contract ClusterPayoutOracleTest is Test {
 
         vm.prank(challenger);
         vm.expectRevert(ClusterPayoutOracle.InvalidBond.selector);
-        oracle.challengeCorrelationEpoch{value: 1}(1, keccak256("bad-root"));
+        oracle.challengeCorrelationEpoch{ value: 1 }(1, keccak256("bad-root"));
     }
 
     function test_ArbiterCanFinalizeChallengedSnapshots() public {
@@ -1929,7 +1929,7 @@ contract ClusterPayoutOracleProposerBondTest is Test {
 
     event ProposerBondUnrecoverable(bytes32 indexed snapshotKey, address indexed proposer, uint256 missingAmount);
 
-    receive() external payable {}
+    receive() external payable { }
 
     function setUp() public {
         arbiter = address(this);
@@ -2137,7 +2137,7 @@ contract MockRoundPayoutSnapshotConsumer {
 contract TestableClusterPayoutOracle is ClusterPayoutOracle {
     constructor(address admin, address frontendRegistry, address challengeBondToken)
         ClusterPayoutOracle(admin, frontendRegistry, challengeBondToken)
-    {}
+    { }
 
     /// @dev Sets proposerBond directly via the inherited (private) mapping. Because the storage
     ///      mapping is `private`, we re-declare an internal shim that maps onto the same slot by