diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index 8673ecfa2e220..9c99dfa15cb86 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -5,6 +5,8 @@ on:
   merge_group:
   pull_request:
     branches: [ main ]
+    # `labeled` lets a maintainer request autoharness on a PR with the run-autoharness label.
+    types: [opened, synchronize, reopened, labeled]
   push:
     paths:
       - 'library/**'
@@ -18,6 +20,8 @@ defaults:
 jobs:
   check-kani-on-std:
     name: Verify std library (partition ${{ matrix.partition }})
+    # Adding a label must not re-run the partitions; they already ran for this commit.
+    if: github.event.action != 'labeled'
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -67,6 +71,15 @@ jobs:
    
   kani_autoharness:
     name: Verify std library using autoharness
+    if: github.event.action != 'labeled' || github.event.label.name == 'run-autoharness'
+    # Autoharness, Metrics, List, Analyzer and Build JSON run only in the merge queue, on
+    # workflow_dispatch, or on PRs with the run-autoharness label (#730): they cost about 5
+    # runner-hours per run and decide how long a PR waits.
+    # This job is a required check under its matrix name, and a job skipped by a job-level
+    # `if:` reports without the "(os)" suffix, which would leave PRs pending. So the gate is
+    # on each step instead: on a PR the job starts, skips every step and passes in seconds.
+    # The job-level `if:` above only skips events for other labels; the required check has
+    # already reported for that commit by then.
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -80,7 +93,7 @@ jobs:
 
     steps:
       - name: Remove unnecessary software to free up disk space
-        if: matrix.os == 'ubuntu-latest'
+        if: matrix.os == 'ubuntu-latest' && (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness'))
         run: |
           # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
           df -h
@@ -89,6 +102,7 @@ jobs:
 
       # Step 1: Check out the repository
       - name: Checkout Repository
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')
         uses: actions/checkout@v4
         with:
           submodules: true
@@ -107,6 +121,7 @@ jobs:
       #   Unicode tables were regenerated (nightly-2026-09-25) they exceed the 10m
       #   timeout on macOS and the ubuntu runner died while verifying them.
       - name: Run Kani Verification
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
             --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
@@ -219,6 +234,7 @@ jobs:
           gzip autoharness-verification.log
 
       - name: Upload Autoharness Verification Log
+        if: github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')
         uses: actions/upload-artifact@v4
         with:
           name: ${{ matrix.os }}-autoharness-verification.log.gz
@@ -229,6 +245,7 @@ jobs:
 
   run_kani_metrics:
     name: Kani Metrics
+    if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness')
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
@@ -299,6 +316,7 @@ jobs:
 
   run-log-analysis:
     name: Build JSON from logs
+    if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness')
     needs: [run_kani_metrics, kani_autoharness]
     runs-on: ${{ matrix.os }}
     strategy:
@@ -351,6 +369,7 @@ jobs:
 
   run-kani-list:
     name: Kani List
+    if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness')
     runs-on: ubuntu-latest
     steps:
       - name: Remove unnecessary software to free up disk space
@@ -396,6 +415,7 @@ jobs:
 
   run-autoharness-analyzer:
     name: Kani Autoharness Analyzer
+    if: (github.event_name == 'merge_group' || github.event_name == 'workflow_dispatch' || contains(github.event.pull_request.labels.*.name, 'run-autoharness')) && (github.event.action != 'labeled' || github.event.label.name == 'run-autoharness')
     runs-on: ubuntu-latest
     steps:
       # Step 1: Check out the repository