diff --git a/.github/workflows/dual-proof.yml b/.github/workflows/dual-proof.yml
new file mode 100644
index 00000000..2be7d3f3
--- /dev/null
+++ b/.github/workflows/dual-proof.yml
@@ -0,0 +1,346 @@
+name: Full-domain dual proof
+
+on:
+  workflow_dispatch:
+    inputs:
+      lane_run_ids:
+        description: comma-separated runs carrying the verification lane artifacts of BOTH engines
+        required: true
+
+permissions:
+  contents: read
+  actions: read
+
+concurrency:
+  group: dual-proof-${{ github.run_id }}
+  cancel-in-progress: false
+
+jobs:
+  dual-proof:
+    name: seal one full-domain dual proof from two live source-bound receipts
+    # Both engines run in ONE job because `join_dual_proof_v1` needs their
+    # source-bound receipts, and those have no wire form by design: only the
+    # process that minted them can hold them.  Measured on run 31116022208 the
+    # native RUNs took 63 min (Arb) and 43 min (MPFI), so the sequential pair
+    # plus both builds fits the envelope below with room to spare.
+    #
+    # The lane covers come from an earlier run's artifacts.  They admit against
+    # these fresh receipts because a lane binds the comparator's *source*
+    # identity, which reproduces across runners; the full identity folds build
+    # observation and does not.
+    runs-on: ubuntu-latest
+    timeout-minutes: 330
+    env:
+      PYTHONDONTWRITEBYTECODE: "1"
+      PYTHONHASHSEED: "0"
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: bind run-local native paths
+        shell: bash
+        run: |
+          set -euo pipefail
+          scope="/sys/fs/cgroup/labcolors-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          # One observer subtree per engine.  A shared one cannot work here:
+          # its budget is two tasks, the controller stays in the observer it
+          # entered, and the second engine's BUILD would fork into a full
+          # subtree.  The gate returns to `tasks` between engines and points
+          # LABCOLORS_EXECUTOR_CGROUP_V1 at the next subtree itself.
+          {
+            echo "LABCOLORS_CGROUP_SCOPE_V1=$scope"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_TASKS=$scope/tasks"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_ARB=$scope/proof-arb"
+            echo "LABCOLORS_DUAL_PROOF_CGROUP_MPFI=$scope/proof-mpfi"
+          } >> "$GITHUB_ENV"
+
+      - name: acquire and hash-check the union of both source closures
+        shell: bash
+        run: |
+          set -euo pipefail
+          # GMP and MPFR are pinned to byte-identical archives by both engine
+          # locks, so the union is fetched once; a future divergence makes the
+          # digest check below fail loudly instead of silently preferring one.
+          source_dir="$RUNNER_TEMP/dual-source-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT"
+          install -d -m 0700 "$source_dir"
+          echo "LABCOLORS_DUAL_SOURCE_DIR=$source_dir" >> "$GITHUB_ENV"
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY' > "$source_dir/lock.tsv"
+          import sys
+
+          import provenance
+
+          seen: dict[str, tuple[str, str, int]] = {}
+          for lock in (provenance.arb_source_lock_v1(), provenance.mpfi_source_lock_v1()):
+              for source in lock.sources:
+                  entry = (
+                      source.archive_url,
+                      source.archive_sha256.hex(),
+                      source.archive_length,
+                  )
+                  previous = seen.setdefault(source.role.name, entry)
+                  if previous != entry:
+                      # One role, two different archives: the engines no longer
+                      # share a source and this job's single fetch would give
+                      # one of them the wrong bytes.
+                      print(f"source role diverged: {source.role.name}", file=sys.stderr)
+                      raise SystemExit(64)
+          for role, (url, digest, length) in sorted(seen.items()):
+              print(role, url, digest, length, sep="\t")
+          PY
+          count=0
+          while IFS=$'\t' read -r role url digest length; do
+            archive="$source_dir/${role}.archive"
+            curl --fail --location --silent --show-error \
+              --connect-timeout 30 --max-time 600 --retry 3 --retry-all-errors \
+              "$url" --output "$archive"
+            test "$(stat --format=%s "$archive")" = "$length"
+            echo "$digest  $archive" | sha256sum --check --strict
+            case "$role" in
+              GMP) echo "LABCOLORS_GMP_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              MPFR) echo "LABCOLORS_MPFR_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              FLINT_ARB) echo "LABCOLORS_FLINT_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              MPFI) echo "LABCOLORS_MPFI_ARCHIVE=$archive" >> "$GITHUB_ENV" ;;
+              *) exit 64 ;;
+            esac
+            count=$((count + 1))
+          done < "$source_dir/lock.tsv"
+          test "$count" -eq 4
+
+      - name: acquire both pinned OCI manifests
+        shell: bash
+        run: |
+          set -euo pipefail
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          docker_path="$(realpath "$(command -v docker)")"
+          test -f "$docker_path"
+          test ! -L "$docker_path"
+          python3 - <<'PY' > images.txt
+          from arb import pipeline
+          from mpfi import build
+
+          print(pipeline.OCI_IMAGE_REFERENCE_V1)
+          print(build.MPFI_BUILD_IMAGE_REFERENCE_V1)
+          PY
+          while read -r image; do
+            test -n "$image"
+            "$docker_path" image inspect "$image" >/dev/null 2>&1 ||
+              /usr/bin/timeout --signal=TERM --kill-after=30s 15m \
+                "$docker_path" pull "$image"
+          done < images.txt
+          rm -f images.txt
+          {
+            echo "LABCOLORS_ARB_PIPELINE_DOCKER=$docker_path"
+            echo "LABCOLORS_MPFI_DOCKER=$docker_path"
+          } >> "$GITHUB_ENV"
+
+      - name: require the exact diagnostic Docker boundary
+        shell: bash
+        run: |
+          set -euo pipefail
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          export LABCOLORS_ARB_PIPELINE_DOCKER
+          python3 - <<'PY'
+          import os
+          import sys
+          from pathlib import Path
+
+          from arb import pipeline
+          from build import transport as build_transport
+
+          docker = build_transport.NativeDockerBuildBackendV1(
+              Path(os.environ["LABCOLORS_ARB_PIPELINE_DOCKER"]),
+              pipeline.ARB_BUILD_TRANSPORT_POLICY_V1,
+          ).probe()
+          print(repr(docker))
+          if type(docker) is not build_transport.DockerSupportedV1:
+              sys.exit(78)
+          PY
+
+      - name: download both engines' verification lane covers
+        # Every lane is dispatched as its own run, so the cover spans many
+        # run ids — the same shape `full-domain-corpus.yml` already uses to
+        # assemble lane evidence.  Both engines land in one flat directory:
+        # lane artifact names carry the engine only to keep the files apart,
+        # while which engine a lane serves is decided by the comparator
+        # source identity inside its manifest.
+        #
+        # Each run lands in its own directory first.  Downloading straight
+        # into one would let a re-run of the same window overwrite the
+        # evidence already there — the cover would still look exact while
+        # quietly having used one of two answers.
+        shell: bash
+        env:
+          GH_TOKEN: ${{ github.token }}
+          LANE_RUN_IDS: ${{ inputs.lane_run_ids }}
+        run: |
+          set -euo pipefail
+          mkdir -p lanes-in staged
+          IFS=',' read -r -a RUNS <<< "${LANE_RUN_IDS}"
+          for run in "${RUNS[@]}"; do
+            run="$(echo "${run}" | tr -d '[:space:]')"
+            case "${run}" in
+              ''|*[!0-9]*)
+                echo "lane run id is not a number: ${run}" >&2
+                exit 64
+                ;;
+            esac
+            rm -rf "staged/${run}"
+            mkdir -p "staged/${run}"
+            gh run download "${run}"               --repo '${{ github.repository }}'               --pattern 'verification-lane-*'               --dir "staged/${run}"
+            for lane in "staged/${run}"/*/; do
+              name="$(basename "${lane}")"
+              if [[ -e "lanes-in/${name}" ]]; then
+                echo "two runs claim lane ${name}; one would silently win" >&2
+                exit 64
+              fi
+              mv "${lane}" "lanes-in/${name}"
+            done
+          done
+          rm -rf staged
+          echo "LABCOLORS_DUAL_PROOF_LANES=$GITHUB_WORKSPACE/lanes-in"             >> "$GITHUB_ENV"
+
+      - name: refuse an incomplete cover before anything expensive is built
+        shell: bash
+        run: |
+          set -euo pipefail
+          # Cover arithmetic costs seconds; discovering a missing lane after
+          # both native runs costs the whole job.
+          export PYTHONPATH="$GITHUB_WORKSPACE/proof/region/v1"
+          python3 - <<'PY'
+          import json
+          import sys
+          from collections import defaultdict
+          from pathlib import Path
+
+          import region_proof_protocol as protocol
+
+          domain_points = protocol.OUTPUT_CARDINALITY_V1
+          windows = defaultdict(list)
+          for lane in sorted(Path("lanes-in").iterdir()):
+              manifest_path = lane / "lane-manifest.json"
+              if not manifest_path.is_file():
+                  print(f"not a lane directory: {lane}", file=sys.stderr)
+                  raise SystemExit(64)
+              manifest = json.loads(manifest_path.read_text("ascii"))
+              windows[manifest["comparator_source_identity"]].append(
+                  (manifest["window_start"], manifest["window_points"])
+              )
+          if len(windows) != 2:
+              print(f"expected two engines, found {len(windows)}", file=sys.stderr)
+              raise SystemExit(64)
+          for identity, cover in sorted(windows.items()):
+              cursor = 0
+              for start, points in sorted(cover):
+                  if start != cursor:
+                      print(f"{identity[:16]}: gap or overlap at {cursor}", file=sys.stderr)
+                      raise SystemExit(64)
+                  cursor += points
+              if cursor != domain_points:
+                  print(f"{identity[:16]}: cover ends at {cursor}", file=sys.stderr)
+                  raise SystemExit(64)
+              print(f"{identity[:16]}: {len(cover)} lanes cover the exact domain")
+          PY
+
+      - name: delegate one disposable cgroup subtree
+        shell: bash
+        run: |
+          set -euo pipefail
+          apparmor_userns=/proc/sys/kernel/apparmor_restrict_unprivileged_userns
+          if [[ -f "$apparmor_userns" ]]; then
+            original_userns="$(cat "$apparmor_userns")"
+            case "$original_userns" in
+              0|1) ;;
+              *) exit 78 ;;
+            esac
+            echo "LABCOLORS_APPARMOR_USERNS_V1=$original_userns" >> "$GITHUB_ENV"
+            sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0
+            test "$(cat "$apparmor_userns")" = 0
+          else
+            echo "LABCOLORS_APPARMOR_USERNS_V1=" >> "$GITHUB_ENV"
+          fi
+          scope="$LABCOLORS_CGROUP_SCOPE_V1"
+          sudo mkdir "$scope"
+          sudo chown "$(id -u):$(id -g)" \
+            "$scope" \
+            "$scope/cgroup.procs" \
+            "$scope/cgroup.threads" \
+            "$scope/cgroup.subtree_control"
+          printf '+memory +pids' > "$scope/cgroup.subtree_control"
+          mkdir "$scope/tasks"
+          for engine in proof-arb proof-mpfi; do
+            mkdir "$scope/$engine"
+            printf '+memory +pids' > "$scope/$engine/cgroup.subtree_control"
+            printf '2' > "$scope/$engine/pids.max"
+            mkdir "$scope/$engine/observer"
+            grep --fixed-strings --quiet 'memory' "$scope/$engine/cgroup.subtree_control"
+            grep --fixed-strings --quiet 'pids' "$scope/$engine/cgroup.subtree_control"
+            test "$(cat "$scope/$engine/pids.max")" = 2
+          done
+          echo core | sudo tee /proc/sys/kernel/core_pattern >/dev/null
+          test "$(cat /proc/sys/kernel/core_pattern)" = core
+
+      - name: seal the full-domain dual proof
+        shell: bash
+        env:
+          LABCOLORS_DUAL_PROOF_OUT: dual-proof-out
+        run: |
+          set -euo pipefail
+          # Same cgroup admission contract as the single-engine lanes: root
+          # admits the runner into the owned subtree, and every later observer
+          # placement stays a proven self-migration between delegated groups.
+          echo "$$" | sudo tee \
+            "$LABCOLORS_CGROUP_SCOPE_V1/tasks/cgroup.procs" >/dev/null
+          exec python3 proof/region/v1/tests/dual_proof_gate.py
+
+      - name: upload the sealed dual proof identity
+        uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
+        with:
+          name: dual-proof-identity
+          path: dual-proof-out/
+          if-no-files-found: error
+
+      - name: remove disposable inputs and cgroup
+        if: always()
+        shell: bash
+        run: |
+          set -uo pipefail
+          status=0
+          record_failure() {
+            local code="$?"
+            if (( status == 0 )); then
+              status="$code"
+            fi
+          }
+          if [[ -n "${LABCOLORS_DUAL_SOURCE_DIR:-}" ]]; then
+            rm -rf -- "$LABCOLORS_DUAL_SOURCE_DIR" || record_failure
+          fi
+          if [[ -n "${LABCOLORS_CGROUP_SCOPE_V1:-}" && \
+                -d "$LABCOLORS_CGROUP_SCOPE_V1" ]]; then
+            if [[ -f "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.kill" ]]; then
+              echo 1 | sudo tee "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.kill" \
+                >/dev/null || record_failure
+            fi
+            if [[ -f "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" ]]; then
+              for _ in {1..100}; do
+                grep --fixed-strings --quiet 'populated 0' \
+                  "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" && break
+                sleep 0.01
+              done
+              grep --fixed-strings --quiet 'populated 0' \
+                "$LABCOLORS_CGROUP_SCOPE_V1/cgroup.events" || record_failure
+            fi
+            for child in proof-arb/observer proof-arb proof-mpfi/observer proof-mpfi tasks; do
+              if [[ -d "$LABCOLORS_CGROUP_SCOPE_V1/$child" ]]; then
+                sudo rmdir "$LABCOLORS_CGROUP_SCOPE_V1/$child" || record_failure
+              fi
+            done
+            sudo rmdir "$LABCOLORS_CGROUP_SCOPE_V1" || record_failure
+          fi
+          if [[ -n "${LABCOLORS_APPARMOR_USERNS_V1:-}" ]]; then
+            sudo sysctl -w \
+              "kernel.apparmor_restrict_unprivileged_userns=$LABCOLORS_APPARMOR_USERNS_V1" \
+              >/dev/null || record_failure
+          fi
+          exit "$status"
diff --git a/.github/workflows/verification-lanes.yml b/.github/workflows/verification-lanes.yml
index a34e8e85..5c22d8f8 100644
--- a/.github/workflows/verification-lanes.yml
+++ b/.github/workflows/verification-lanes.yml
@@ -1,5 +1,13 @@
 name: Verification lane replay
 
+# One lane is one run, so a full-domain cover is 512 of them and the dual
+# proof needs their ids.  Naming the run after its coordinates makes that list
+# a query instead of a guess about creation times.
+run-name: >-
+  lane ${{ inputs.evidence_artifact }}
+  ${{ inputs.window_start }}+${{ inputs.window_points }}
+  of ${{ inputs.evidence_run_id }}
+
 on:
   workflow_dispatch:
     inputs:
@@ -97,8 +105,14 @@ jobs:
             --out lane-out
 
       - name: upload the verification lane wire evidence
+        # The engine belongs in the name because both engines replay the same
+        # window plan: without it every Arb lane and its MPFI twin claim one
+        # artifact name, and a cover gathered from many runs would overwrite
+        # itself down to one engine.  The name is only for keeping the files
+        # apart — which engine a lane actually serves is decided by the
+        # comparator source identity inside its manifest.
         uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
         with:
-          name: verification-lane-${{ inputs.window_start }}-${{ inputs.window_points }}
+          name: verification-lane-${{ inputs.evidence_artifact }}-${{ inputs.window_start }}-${{ inputs.window_points }}
           path: lane-out/
           if-no-files-found: error
diff --git a/proof/region/v1/PROTOCOL.md b/proof/region/v1/PROTOCOL.md
index bd52b45c..0c132960 100644
--- a/proof/region/v1/PROTOCOL.md
+++ b/proof/region/v1/PROTOCOL.md
@@ -249,11 +249,24 @@ backend run как `ObserverFailureV1(REQUEST_NOT_ADMITTED)`.
 
 `executor.canonical_cgroup_parent_v1` разбирает объявленный parent без
 разрешения пути через файловую систему.
-`executor.enter_observer_cgroup_v1` — единственная versioned межмодульная
-операция размещения: engine controller передаёт этот
+Размещением контроллера ведают ровно две versioned межмодульные операции.
+`executor.enter_observer_cgroup_v1`: engine controller передаёт этот
 абсолютный канонический parent, а executor помещает текущий controller в
-`parent/observer` и пробрасывает отказ для typed mapping вызывающего. Engine не
-копирует этот descriptor protocol. Executor открывает каждый сегмент cgroup
+`parent/observer` — единственный вход без typed mapping исключений. Engine не
+копирует этот descriptor protocol.
+
+`executor.enter_task_cgroup_v1` — вторая операция размещения: она возвращает
+контроллер в делегированную группу, которая ничего не ограничивает. Это нужно
+ровно там, где один процесс наблюдает две сборки подряд: контроллер остаётся в
+том observer'е, куда вошёл, а поддерево того observer'а допускает ровно две
+задачи, поэтому второй BUILD форкал бы в исчерпанный бюджет. Containment
+прогона при этом не расширяется — бюджет наблюдателя действует для каждого
+исполнения по отдельности. Операция проверяет собственное пост-условие:
+группа, где процесс оказался, обязана быть той же, что названа, и сверяется
+она по иноде, а не по написанию пути — два имени одной группы не должны
+стоить прогона.
+
+Executor открывает каждый сегмент cgroup
 descriptor-relative с `O_PATH|O_NOFOLLOW`: metadata-проверка допускает каталог,
 доступный только для поиска, но символическая ссылка не может незаметно связать
 controller с другой cgroup. Размещение остаётся self-migration: kernel
@@ -862,6 +875,32 @@ quadrant-развёртка `sin`/`cos` ограничена dyadic числом
 продолжения вычисления engine с hull `[-1, 1]` — третий верификатор не вправе
 выносить заключение, которое не следует из committed грамматики.
 
+## Где может быть запечатано дуальное доказательство
+
+`join_dual_proof_v1` принимает пять цепей доказательств, и две из них —
+source-bound квитанции движков — **не имеют wire-формы намеренно**: квитанция,
+которую можно разобрать из байтов, позволила бы чужому коду начеканить
+провенанс. Отсюда закон размещения: дуальное доказательство может быть
+запечатано только внутри процесса, который сам начеканил обе квитанции.
+
+Практически это означает один job, последовательно собирающий и запускающий оба
+движка над полным манифестом. Два job'а не годятся ни в каком виде: между ними
+квитанция может пройти только по проводу, а провода у неё нет.
+
+Остальные три цепи приходят с диска. Семантические квитанции пересобираются из
+полос предыдущего прогона, и это возможно ровно потому, что полоса связывает
+**source-идентичность** компаратора (см. «Две идентичности компаратора»).
+Полоса, связанная с полной идентичностью, умерла бы вместе с прогоном, который
+дал ей evidence, и ни один процесс не смог бы держать одновременно свежую
+квитанцию и покрытие полос.
+
+Та же source-идентичность разделяет покрытие по движкам: принадлежность полосы
+выводится из её манифеста, а не из имени артефакта или каталога.
+
+Наружу из прогона уходит только идентичность запечатанной квитанции. Артефакта,
+который можно разобрать обратно в провенанс, не появляется.
+
+
 ## Ошибки допуска
 
 `ProtocolReasonV1` — закрытая сумма:
diff --git a/proof/region/v1/arb/tests/full_domain_receipt.py b/proof/region/v1/arb/tests/full_domain_receipt.py
index d181eb69..d4350909 100644
--- a/proof/region/v1/arb/tests/full_domain_receipt.py
+++ b/proof/region/v1/arb/tests/full_domain_receipt.py
@@ -43,6 +43,41 @@
 EVIDENCE_OUT_ENV_V1 = "LABCOLORS_FULL_DOMAIN_EVIDENCE_OUT"
 
 
+def seal_full_domain_receipt_v1() -> receipt.SourceBoundEvaluatorReceiptV1:
+    """One controller-observed BUILD to RUN over the exact full manifest.
+
+    Extracted so the dual-proof gate mints the same receipt this lane does
+    instead of restating the request: two copies of the build coordinates
+    would drift, and the drift would surface as an unrelated admission
+    failure hours into a native run.
+    """
+
+    source_lock = provenance.arb_source_lock_v1()
+    archive_names = (
+        "LABCOLORS_GMP_ARCHIVE",
+        "LABCOLORS_MPFR_ARCHIVE",
+        "LABCOLORS_FLINT_ARCHIVE",
+    )
+    safe = tuple(
+        provenance.admit_source_archive(lock, Path(os.environ[name]).read_bytes())
+        for lock, name in zip(source_lock.sources, archive_names, strict=True)
+    )
+    admitted = provenance.admit_arb_sources(source_lock, safe)
+    request = _request(
+        source_lock=source_lock,
+        admitted_sources=admitted,
+        job=corpus.full_domain_job_v1(_job()),
+        runtime_binding=_runtime_binding(
+            wall_timeout_ns=FULL_DOMAIN_WALL_TIMEOUT_NS_V1,
+            memory_max_bytes=FULL_DOMAIN_MEMORY_MAX_BYTES_V1,
+        ),
+    )
+    return receipt.SourceBoundArbControllerV1(
+        Path(os.environ["LABCOLORS_ARB_PIPELINE_DOCKER"]),
+        Path(os.environ["LABCOLORS_EXECUTOR_CGROUP_V1"]),
+    ).execute(request)
+
+
 @unittest.skipUnless(
     sys.platform == "linux"
     and os.environ.get("LABCOLORS_ARB_PIPELINE_DOCKER")
@@ -54,31 +89,8 @@
 )
 class NativeSourceBoundFullDomainReceiptIntegrationTests(unittest.TestCase):
     def test_full_domain_build_run_seal_and_verification_evidence(self) -> None:
-        source_lock = provenance.arb_source_lock_v1()
-        archive_names = (
-            "LABCOLORS_GMP_ARCHIVE",
-            "LABCOLORS_MPFR_ARCHIVE",
-            "LABCOLORS_FLINT_ARCHIVE",
-        )
-        safe = tuple(
-            provenance.admit_source_archive(lock, Path(os.environ[name]).read_bytes())
-            for lock, name in zip(source_lock.sources, archive_names, strict=True)
-        )
-        admitted = provenance.admit_arb_sources(source_lock, safe)
         full_job = corpus.full_domain_job_v1(_job())
-        request = _request(
-            source_lock=source_lock,
-            admitted_sources=admitted,
-            job=full_job,
-            runtime_binding=_runtime_binding(
-                wall_timeout_ns=FULL_DOMAIN_WALL_TIMEOUT_NS_V1,
-                memory_max_bytes=FULL_DOMAIN_MEMORY_MAX_BYTES_V1,
-            ),
-        )
-        result = receipt.SourceBoundArbControllerV1(
-            Path(os.environ["LABCOLORS_ARB_PIPELINE_DOCKER"]),
-            Path(os.environ["LABCOLORS_EXECUTOR_CGROUP_V1"]),
-        ).execute(request)
+        result = seal_full_domain_receipt_v1()
 
         self.assertIs(type(result), receipt.SourceBoundEvaluatorReceiptV1, result)
         self.assertTrue(receipt.replay_evidence_is_well_bound_v1(result.evidence))
diff --git a/proof/region/v1/arb/tests/gate.py b/proof/region/v1/arb/tests/gate.py
index e4d97d4b..f893c7fc 100644
--- a/proof/region/v1/arb/tests/gate.py
+++ b/proof/region/v1/arb/tests/gate.py
@@ -19,7 +19,7 @@
     "test_mpfi_input.py",
 )
 EXPECTED_TEST_INVENTORY_SHA256 = (
-    "030cd7d43490c3aea5e10ba7d29baa2ab7de61639f05b9e9a98d0007cd990c05"
+    "86c723aa43fe0bb8f0f5a182a09da9886429ca03ab42d5001b9b5bec603071e2"
 )
 _EVALUATOR_REASON = "set LABCOLORS_ARB_EVALUATOR to the controlled C17 binary"
 EXPECTED_SKIPS = frozenset(
diff --git a/proof/region/v1/executor.py b/proof/region/v1/executor.py
index 20cabd20..e7f3fa6d 100644
--- a/proof/region/v1/executor.py
+++ b/proof/region/v1/executor.py
@@ -1514,6 +1514,70 @@ def _open_cgroup_directory_v1(parent: object) -> int:
             os.close(descriptor)
 
 
+def enter_task_cgroup_v1(group: Path) -> None:
+    """Return this controller to a delegated group that constrains nothing.
+
+    A controller that observed one BUILD to RUN stays in the observer group it
+    entered, and that group's subtree admits exactly two tasks — the observer
+    and the one child it watched.  A process that must observe a *second*
+    execution therefore has to start where a fresh process would: outside any
+    observer, before it builds anything.  Without this the second BUILD forks
+    into a saturated subtree and dies, an hour into a native run.
+
+    This never widens a run's containment: the observer budget still applies
+    to each execution, and the group entered here is the same unconstrained
+    one root admitted this process into at the start.
+    """
+
+    if not isinstance(group, Path):
+        raise TypeError("cgroup group must be an absolute canonical Path")
+    # Descriptors pin every path component, for the same reason the observer
+    # placement does: resolving a pathname would follow a symlink before this
+    # controller can prove which cgroup it entered.
+    directory_fd = _open_cgroup_directory_v1(group)
+    try:
+        _write_own_pid_v1(directory_fd)
+    finally:
+        os.close(directory_fd)
+    # The observer placement is always followed by a budget probe; this one
+    # would otherwise take the caller's word for where it landed.  The path
+    # arrives from configuration, and a wrong one silently moves where the
+    # next BUILD runs — which no later check looks at.
+    #
+    # Compared by inode like the observer's own probe, not by spelling: two
+    # names for one group would fail a string comparison and cost the run,
+    # and a false refusal here is as expensive as no check at all.
+    current_fd = _open_cgroup_directory_v1(_current_unified_cgroup_v1())
+    try:
+        named_fd = _open_cgroup_directory_v1(group)
+        try:
+            current_stat = os.fstat(current_fd)
+            named_stat = os.fstat(named_fd)
+        finally:
+            os.close(named_fd)
+    finally:
+        os.close(current_fd)
+    if (
+        current_stat.st_dev != named_stat.st_dev
+        or current_stat.st_ino != named_stat.st_ino
+    ):
+        raise OSError(errno_module.EBUSY, "controller did not enter the named group")
+
+
+def _write_own_pid_v1(directory_fd: int) -> None:
+    procs_fd = os.open(
+        b"cgroup.procs",
+        os.O_WRONLY | os.O_CLOEXEC | os.O_NOFOLLOW,
+        dir_fd=directory_fd,
+    )
+    try:
+        payload = str(os.getpid()).encode("ascii")
+        if os.write(procs_fd, payload) != len(payload):
+            raise OSError(errno_module.EIO, "short cgroup placement write")
+    finally:
+        os.close(procs_fd)
+
+
 def enter_observer_cgroup_v1(parent: Path) -> None:
     """Move the dedicated controller into the declared observer group."""
 
@@ -1525,17 +1589,7 @@ def enter_observer_cgroup_v1(parent: Path) -> None:
     try:
         directory_fd = _open_cgroup_child_directory_v1(parent_fd, b"observer")
         try:
-            procs_fd = os.open(
-                b"cgroup.procs",
-                os.O_WRONLY | os.O_CLOEXEC | os.O_NOFOLLOW,
-                dir_fd=directory_fd,
-            )
-            try:
-                payload = str(os.getpid()).encode("ascii")
-                if os.write(procs_fd, payload) != len(payload):
-                    raise OSError(errno_module.EIO, "short cgroup placement write")
-            finally:
-                os.close(procs_fd)
+            _write_own_pid_v1(directory_fd)
         finally:
             os.close(directory_fd)
     finally:
diff --git a/proof/region/v1/mpfi/tests/full_domain_receipt.py b/proof/region/v1/mpfi/tests/full_domain_receipt.py
index 8f2d554f..710a7a14 100644
--- a/proof/region/v1/mpfi/tests/full_domain_receipt.py
+++ b/proof/region/v1/mpfi/tests/full_domain_receipt.py
@@ -58,6 +58,46 @@ def _full_domain_binding() -> mpfi_runtime.MpfiRuntimeBindingV1:
     )
 
 
+def seal_full_domain_receipt_v1() -> receipt.MpfiSourceBoundEvaluatorReceiptV1:
+    """One controller-observed MPFI BUILD to RUN over the exact full manifest.
+
+    Extracted for the same reason as the Arb lane: the dual-proof gate mints
+    the receipt through this function instead of restating the request, so
+    the two cannot drift apart.
+    """
+
+    source_lock = provenance.mpfi_source_lock_v1()
+    archive_names = (
+        "LABCOLORS_GMP_ARCHIVE",
+        "LABCOLORS_MPFR_ARCHIVE",
+        "LABCOLORS_MPFI_ARCHIVE",
+    )
+    safe = tuple(
+        provenance.admit_source_archive(lock, Path(os.environ[name]).read_bytes())
+        for lock, name in zip(source_lock.sources, archive_names, strict=True)
+    )
+    admitted = provenance.admit_mpfi_sources(source_lock, safe)
+    base = _request()
+    request = receipt.MpfiPipelineRequestV1(
+        source_lock,
+        admitted,
+        base.build_sources,
+        base.generated_formula,
+        _limits_for_bundle(
+            source_lock,
+            admitted,
+            base.build_sources,
+            base.generated_formula,
+        ),
+        corpus.full_domain_job_v1(base.job),
+        _full_domain_binding(),
+    )
+    return receipt.MpfiSourceBoundControllerV1(
+        Path(os.environ["LABCOLORS_MPFI_DOCKER"]),
+        Path(os.environ["LABCOLORS_EXECUTOR_CGROUP_V1"]),
+    ).execute(request)
+
+
 @unittest.skipUnless(
     sys.platform == "linux"
     and os.environ.get("LABCOLORS_MPFI_DOCKER")
@@ -69,37 +109,8 @@ def _full_domain_binding() -> mpfi_runtime.MpfiRuntimeBindingV1:
 )
 class NativeMpfiSourceBoundFullDomainReceiptIntegrationTests(unittest.TestCase):
     def test_full_domain_build_run_seal_and_verification_evidence(self) -> None:
-        source_lock = provenance.mpfi_source_lock_v1()
-        archive_names = (
-            "LABCOLORS_GMP_ARCHIVE",
-            "LABCOLORS_MPFR_ARCHIVE",
-            "LABCOLORS_MPFI_ARCHIVE",
-        )
-        safe = tuple(
-            provenance.admit_source_archive(lock, Path(os.environ[name]).read_bytes())
-            for lock, name in zip(source_lock.sources, archive_names, strict=True)
-        )
-        admitted = provenance.admit_mpfi_sources(source_lock, safe)
-        base = _request()
-        full_job = corpus.full_domain_job_v1(base.job)
-        request = receipt.MpfiPipelineRequestV1(
-            source_lock,
-            admitted,
-            base.build_sources,
-            base.generated_formula,
-            _limits_for_bundle(
-                source_lock,
-                admitted,
-                base.build_sources,
-                base.generated_formula,
-            ),
-            full_job,
-            _full_domain_binding(),
-        )
-        result = receipt.MpfiSourceBoundControllerV1(
-            Path(os.environ["LABCOLORS_MPFI_DOCKER"]),
-            Path(os.environ["LABCOLORS_EXECUTOR_CGROUP_V1"]),
-        ).execute(request)
+        full_job = corpus.full_domain_job_v1(_request().job)
+        result = seal_full_domain_receipt_v1()
 
         self.assertIs(type(result), receipt.MpfiSourceBoundEvaluatorReceiptV1, result)
         self.assertTrue(receipt.replay_mpfi_evidence_is_well_bound_v1(result.evidence))
diff --git a/proof/region/v1/tests/dual_proof_gate.py b/proof/region/v1/tests/dual_proof_gate.py
new file mode 100644
index 00000000..b2f8ba88
--- /dev/null
+++ b/proof/region/v1/tests/dual_proof_gate.py
@@ -0,0 +1,336 @@
+#!/usr/bin/env python3
+"""The one place a full-domain dual proof can be sealed.
+
+`join_dual_proof_v1` needs five live objects, and two of them — the engines'
+source-bound receipts — have no wire form on purpose: a receipt that could be
+parsed from bytes would let foreign code mint provenance.  So the join can
+only happen inside a process that minted both receipts itself, which means
+one job that builds and runs both engines back to back.
+
+The other three come from disk.  The semantic receipts are re-sealed here
+from the verification lanes, and that is only possible because a lane binds
+the comparator's *source* identity: two runs of the same sources observe
+different build environments, so a lane bound to the full identity would die
+with the run that produced its evidence, and no single process could ever
+hold both a fresh receipt and a lane cover.  That same source identity is
+what sorts the lane cover into engines — the discriminator is derived from
+the sources, never a name written into the artifact.
+
+Holding both engines in one interpreter is what makes this module delicate:
+the two test directories carry five same-named modules (`full_domain_receipt`,
+`gate`, `native_gate`, `test_evaluator_source`, `test_receipt`), and an import
+cached by the first engine would silently answer for the second.  Both lane
+modules are therefore loaded by path under distinct names, and the load is
+checked against the file it was meant to be.
+
+This module stays outside the fast `test_*.py` inventory: it is one long
+native integration, dispatched deliberately, never swept up by a quick gate.
+"""
+
+from __future__ import annotations
+
+import importlib.util
+import json
+import os
+import sys
+import unittest
+from pathlib import Path
+from types import ModuleType
+
+
+PROOF = Path(__file__).resolve().parents[1]
+ARB_LANE_MODULE = PROOF / "arb" / "tests" / "full_domain_receipt.py"
+MPFI_LANE_MODULE = PROOF / "mpfi" / "tests" / "full_domain_receipt.py"
+sys.path.insert(0, str(PROOF))
+
+import corpus_assembly  # noqa: E402
+import dual_proof  # noqa: E402
+import executor  # noqa: E402
+import region_proof_protocol as protocol  # noqa: E402
+import verification_assembly  # noqa: E402
+from arb import receipt as arb_receipt  # noqa: E402
+from mpfi import receipt as mpfi_receipt  # noqa: E402
+from semantic.receipt import SemanticVerificationReceiptV1  # noqa: E402
+
+LANES_ENV_V1 = "LABCOLORS_DUAL_PROOF_LANES"
+RECEIPT_OUT_ENV_V1 = "LABCOLORS_DUAL_PROOF_OUT"
+# One observer subtree per engine, plus the unconstrained group this process
+# returns to between them.  A shared subtree cannot work: its budget is two
+# tasks, and the second engine's BUILD forks into it.
+ARB_CGROUP_ENV_V1 = "LABCOLORS_DUAL_PROOF_CGROUP_ARB"
+MPFI_CGROUP_ENV_V1 = "LABCOLORS_DUAL_PROOF_CGROUP_MPFI"
+TASK_CGROUP_ENV_V1 = "LABCOLORS_DUAL_PROOF_CGROUP_TASKS"
+EXECUTOR_CGROUP_ENV_V1 = "LABCOLORS_EXECUTOR_CGROUP_V1"
+# Every variable the two lane modules read.  Calling their seal functions
+# directly bypasses the `skipUnless` that used to enumerate these, so an
+# incomplete environment would otherwise surface as a bare KeyError from deep
+# inside a pipeline instead of the refusal this gate promises.
+REQUIRED_ENVIRONMENT_V1 = (
+    "LABCOLORS_ARB_PIPELINE_DOCKER",
+    "LABCOLORS_MPFI_DOCKER",
+    "LABCOLORS_GMP_ARCHIVE",
+    "LABCOLORS_MPFR_ARCHIVE",
+    "LABCOLORS_FLINT_ARCHIVE",
+    "LABCOLORS_MPFI_ARCHIVE",
+    ARB_CGROUP_ENV_V1,
+    MPFI_CGROUP_ENV_V1,
+    TASK_CGROUP_ENV_V1,
+    LANES_ENV_V1,
+)
+
+
+def _load_lane_module_v1(name: str, path: Path) -> ModuleType:
+    """Load one engine's lane module under a name that cannot collide."""
+
+    specification = importlib.util.spec_from_file_location(name, path)
+    if specification is None or specification.loader is None:
+        raise AssertionError(f"cannot load {path}")
+    module = importlib.util.module_from_spec(specification)
+    sys.modules[name] = module
+    specification.loader.exec_module(module)
+    if Path(module.__file__ or "").resolve() != path:
+        raise AssertionError(f"{name} resolved to {module.__file__}, not {path}")
+    return module
+
+
+def _assert_engine_modules_are_unmixed_v1() -> None:
+    """No engine's sibling module may be answering for the other's.
+
+    The lane modules are loaded by path under distinct names, but what they
+    import by bare name is resolved through `sys.path`, and the two test
+    directories carry same-named modules.  Today that resolves correctly only
+    because of the order the two loads happen in — an invariant nothing
+    enforces, so it is asserted rather than assumed.
+    """
+
+    expected = {
+        "test_receipt": MPFI_LANE_MODULE.parent,
+        "test_pipeline": ARB_LANE_MODULE.parent,
+    }
+    for name, directory in expected.items():
+        module = sys.modules.get(name)
+        if module is None:
+            # Absence is not safety: the pin exists because these names are
+            # reached by bare import, and one that stopped being imported
+            # would quietly retire the check instead of failing it.
+            raise AssertionError(f"{name} was not imported by either lane module")
+        resolved = Path(module.__file__ or "").resolve().parent
+        if resolved != directory:
+            raise AssertionError(f"{name} resolved to {resolved}, not {directory}")
+
+
+def _sealed_engine_receipt_v1(module: ModuleType, cgroup_env: str, expected: type):
+    """Seal one engine's receipt in its own observer subtree.
+
+    The process returns to the unconstrained task group first: it may still be
+    inside the previous engine's observer, whose subtree admits two tasks and
+    would refuse this engine's BUILD.
+    """
+
+    executor.enter_task_cgroup_v1(Path(os.environ[TASK_CGROUP_ENV_V1]))
+    os.environ[EXECUTOR_CGROUP_ENV_V1] = os.environ[cgroup_env]
+    sealed = module.seal_full_domain_receipt_v1()
+    if type(sealed) is not expected:
+        # The seal returns a union: every rejection carries the reason this
+        # run failed, and losing it costs another two hours to learn again.
+        raise AssertionError(f"{expected.__name__} not sealed: {sealed!r}")
+    return sealed
+
+
+def _lane_cover_v1(
+    root: Path,
+    job: protocol.ProofJobV1,
+    comparator: protocol.ContentResolvedComparatorManifestV2,
+) -> tuple[tuple[object, ...], frozenset[str]]:
+    """Admit every lane under `root` that this comparator's sources produced.
+
+    The cover is selected by the comparator's source identity rather than by
+    directory name, so a lane from the other engine is not merely rejected
+    later — it is never offered to this receipt in the first place.
+    """
+
+    wanted = comparator.source_identity.hex()
+    lanes = []
+    names = []
+    foreign = 0
+    for directory in sorted(path for path in root.iterdir() if path.is_dir()):
+        manifest_path = directory / "lane-manifest.json"
+        if not manifest_path.is_file():
+            raise AssertionError(f"not a lane directory: {directory}")
+        manifest = json.loads(manifest_path.read_text("ascii"))
+        if manifest["comparator_source_identity"] != wanted:
+            foreign += 1
+            continue
+        lane = corpus_assembly.load_lane_v1(directory, job, comparator)
+        if type(lane) is not corpus_assembly.AdmittedLaneV1:
+            raise AssertionError(f"lane rejected: {directory.name} ({lane!r})")
+        lanes.append(lane)
+        names.append(directory.name)
+    if not lanes:
+        raise AssertionError(f"no lane of this engine under {root} ({foreign} foreign)")
+    lanes.sort(key=lambda lane: lane.window_start)
+    return tuple(lanes), frozenset(names)
+
+
+def _sealed_semantic_receipt_v1(
+    job: protocol.ProofJobV1,
+    comparator: protocol.ContentResolvedComparatorManifestV2,
+    transcript: protocol.DecisionTranscriptV1,
+    run: protocol.RunClaimV1,
+    root: Path,
+) -> tuple[SemanticVerificationReceiptV1, frozenset[str]]:
+    """Re-seal one engine's semantic receipt from its own live coordinates.
+
+    The lanes replayed an earlier run of the same sources; they admit here
+    because they bind the comparator's source identity, which reproduces.
+    Returns the cover's directory names as well: the receipt cannot report
+    which lanes fed it, so proving the two engines used different lanes has
+    to happen out here.
+    """
+
+    lanes, names = _lane_cover_v1(root, job, comparator)
+    sealed = verification_assembly.assemble_semantic_verification_v1(
+        job, comparator, transcript, run, lanes
+    )
+    if type(sealed) is not SemanticVerificationReceiptV1:
+        raise AssertionError(f"semantic verification rejected: {sealed!r}")
+    return sealed, names
+
+
+class NativeFullDomainDualProofIntegrationTests(unittest.TestCase):
+    def test_one_process_seals_the_full_domain_dual_proof(self) -> None:
+        # Deliberately a failure and never a skip: this module is only ever
+        # invoked as its own gate, so an incomplete environment means the
+        # proof did not happen — it must not read as a pass.
+        missing = [name for name in REQUIRED_ENVIRONMENT_V1 if not os.environ.get(name)]
+        self.assertEqual(missing, [], f"missing native environment: {missing}")
+        self.assertEqual(sys.platform, "linux")
+
+        arb_lane = _load_lane_module_v1("labcolors_arb_full_domain", ARB_LANE_MODULE)
+        mpfi_lane = _load_lane_module_v1("labcolors_mpfi_full_domain", MPFI_LANE_MODULE)
+        _assert_engine_modules_are_unmixed_v1()
+
+        arb = _sealed_engine_receipt_v1(
+            arb_lane, ARB_CGROUP_ENV_V1, arb_receipt.SourceBoundEvaluatorReceiptV1
+        )
+        mpfi = _sealed_engine_receipt_v1(
+            mpfi_lane,
+            MPFI_CGROUP_ENV_V1,
+            mpfi_receipt.MpfiSourceBoundEvaluatorReceiptV1,
+        )
+
+        # One job, two engines: a mismatch here means the lanes drifted apart
+        # before any proof could exist.
+        self.assertEqual(arb.job.identity, mpfi.job.identity)
+
+        # The hostile check the single-engine lanes run on their receipts.
+        # Nothing downstream repeats it, and this is the only place a
+        # full-domain receipt is ever sealed.
+        # Only Arb's: its constructor binds a narrower identity relation than
+        # this, so the check can still fail.  MPFI's constructor already
+        # requires the same predicate, so asserting it there would be a line
+        # that cannot fail — the kind of assurance this gate exists to avoid.
+        self.assertTrue(arb_receipt.replay_evidence_is_well_bound_v1(arb.evidence))
+        full_domain = protocol.exact_full_domain_manifest_v1().identity
+        for engine in (arb, mpfi):
+            transcript = engine.transcript
+            self.assertEqual(transcript.point_count, protocol.OUTPUT_CARDINALITY_V1)
+            self.assertEqual(transcript.domain_identity, full_domain)
+            # The engine echoes the coordinate it was told, and it is told the
+            # comparator's source identity: without that the lanes of an
+            # earlier run could never admit against this one.
+            self.assertEqual(
+                transcript.comparator_identity,
+                engine.comparator.manifest.source_identity,
+            )
+            self.assertNotEqual(
+                engine.comparator.manifest.source_identity,
+                engine.comparator.manifest.identity,
+            )
+
+        lanes_root = Path(os.environ[LANES_ENV_V1])
+        arb_semantic, arb_lanes = _sealed_semantic_receipt_v1(
+            arb.job, arb.comparator.manifest, arb.transcript, arb.run_claim, lanes_root
+        )
+        mpfi_semantic, mpfi_lanes = _sealed_semantic_receipt_v1(
+            mpfi.job,
+            mpfi.comparator.manifest,
+            mpfi.transcript,
+            mpfi.evidence.run_claim,
+            lanes_root,
+        )
+        # Disjointness would be tautological: the covers are partitioned by
+        # source identity, and the two engines cannot share one.  What is not
+        # guaranteed is that the partition consumed everything — a lane of a
+        # third identity is silently foreign to both engines, and this is the
+        # only place a full-domain proof is ever sealed.
+        present = frozenset(
+            path.name for path in lanes_root.iterdir() if path.is_dir()
+        )
+        self.assertEqual(arb_lanes | mpfi_lanes, present)
+
+        candidate = protocol.compare_dual_transcripts(
+            arb.job,
+            arb.comparator.manifest,
+            arb.transcript,
+            arb.run_claim,
+            mpfi.comparator.manifest,
+            mpfi.transcript,
+            mpfi.evidence.run_claim,
+        )
+        self.assertIs(type(candidate), protocol.DualComparisonCandidateV1)
+        self.assertIs(dual_proof.claim_spans_full_domain_v1(candidate.claim), True)
+
+        sealed = dual_proof.join_dual_proof_v1(
+            candidate, arb, mpfi, arb_semantic, mpfi_semantic
+        )
+        self.assertIs(type(sealed), dual_proof.DualProofReceiptV1, sealed)
+        self.assertTrue(sealed.full_domain)
+
+        out = os.environ.get(RECEIPT_OUT_ENV_V1)
+        if out:
+            # The receipt has no wire form by design, so what leaves the run
+            # is the identity it sealed: a checkable trace that invents no
+            # parseable provenance artifact.
+            directory = Path(out)
+            directory.mkdir(parents=True, exist_ok=True)
+            (directory / "dual-proof-identity.txt").write_text(
+                sealed.identity.hex() + "\n", encoding="ascii"
+            )
+        print(f"dual proof sealed identity={sealed.identity.hex()}")
+
+
+def main() -> int:
+    """Run the single dual-proof integration with no room to vanish.
+
+    The engine gates pin a discovered inventory against drift; this one has a
+    single named test, so the law that matters is only that it ran, was not
+    skipped, and passed.
+    """
+
+    suite = unittest.defaultTestLoader.loadTestsFromTestCase(
+        NativeFullDomainDualProofIntegrationTests
+    )
+    tests = unittest.defaultTestLoader.getTestCaseNames(
+        NativeFullDomainDualProofIntegrationTests
+    )
+    if len(tests) != 1:
+        print(f"dual proof gate must carry exactly one test, found {tests}", file=sys.stderr)
+        return 1
+    result = unittest.TextTestRunner(verbosity=2).run(suite)
+    if result.skipped:
+        print(f"dual proof gate must not skip: {result.skipped!r}", file=sys.stderr)
+        return 1
+    if (
+        result.failures
+        or result.errors
+        or result.expectedFailures
+        or result.unexpectedSuccesses
+        or not result.wasSuccessful()
+    ):
+        return 1
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/proof/region/v1/tests/test_build.py b/proof/region/v1/tests/test_build.py
index 3c1ac84d..a8ea9ddd 100644
--- a/proof/region/v1/tests/test_build.py
+++ b/proof/region/v1/tests/test_build.py
@@ -54,12 +54,12 @@ def _temporary_mode(path: Path, mode: int) -> Iterator[None]:
 # Keep an independent outer oracle: importing the gate's expected hash here
 # would let a coordinated gate edit hide inventory drift.
 ARB_INVENTORY_SHA256_V1 = (
-    "030cd7d43490c3aea5e10ba7d29baa2ab7de61639f05b9e9a98d0007cd990c05"
+    "86c723aa43fe0bb8f0f5a182a09da9886429ca03ab42d5001b9b5bec603071e2"
 )
 ARB_ORDER_SHA256_V1 = (
-    "d7210149257cb51bd3df3397f8a69323977db8b83425ee28baa42d441685bcbf"
+    "fe5a3419f15812f618cb188a02bc6ca150e51abfdded5e2f5858f6cf574a22e7"
 )
-ARB_TEST_COUNT_V1 = 267
+ARB_TEST_COUNT_V1 = 271
 
 MOVED_INPUT_SURFACE_V1 = (
     "CanonicalInputLimitsV1",
diff --git a/proof/region/v1/tests/test_decorator_placement.py b/proof/region/v1/tests/test_decorator_placement.py
new file mode 100644
index 00000000..66efb3cd
--- /dev/null
+++ b/proof/region/v1/tests/test_decorator_placement.py
@@ -0,0 +1,105 @@
+#!/usr/bin/env python3
+"""A skip decorator that slipped off its test case, caught as source.
+
+`unittest.skip*` only means something on a test: on a test case it gates the
+case, and on a plain module-level function it turns every call into a raised
+`SkipTest`.  So when an extraction inserts a helper between a module's env
+gate and the class it guarded, two defects appear at once — the helper
+becomes uncallable, and the native test loses the gate that kept it out of a
+run that cannot host it.
+
+Neither defect is visible to a syntax check, and the long native lanes live
+outside the fast `test_*.py` inventory, so nothing else in the tree would
+notice until a dispatched job failed an hour in.  This gate reads the tree as
+source, like the arity gate next to it, so it also covers the modules that
+refuse to import on this platform.
+"""
+
+from __future__ import annotations
+
+import ast
+import unittest
+from pathlib import Path
+
+PROOF = Path(__file__).resolve().parents[1]
+SKIP_DECORATORS_V1 = frozenset({"skip", "skipIf", "skipUnless"})
+
+
+def _sources_v1() -> list[Path]:
+    return sorted(
+        path for path in PROOF.rglob("*.py") if "__pycache__" not in path.parts
+    )
+
+
+def _is_unittest_skip_v1(decorator: ast.expr) -> bool:
+    """True for `@unittest.skip*` and for a bare imported `@skipUnless`."""
+
+    target = decorator.func if isinstance(decorator, ast.Call) else decorator
+    if isinstance(target, ast.Attribute):
+        return (
+            target.attr in SKIP_DECORATORS_V1
+            and isinstance(target.value, ast.Name)
+            and target.value.id == "unittest"
+        )
+    return isinstance(target, ast.Name) and target.id in SKIP_DECORATORS_V1
+
+
+class SkipDecoratorPlacementTests(unittest.TestCase):
+    def test_no_module_level_function_carries_a_skip_decorator(self) -> None:
+        offenders = []
+        for path in _sources_v1():
+            tree = ast.parse(path.read_text("utf-8"), str(path))
+            # Only module level: inside a class body a decorated function is
+            # a test method, where skipping is exactly the intended meaning.
+            for node in tree.body:
+                if not isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)):
+                    continue
+                for decorator in node.decorator_list:
+                    if _is_unittest_skip_v1(decorator):
+                        offenders.append(
+                            f"{path.relative_to(PROOF)}:{node.lineno} {node.name}"
+                        )
+        self.assertEqual(offenders, [], f"skip decorator on a non-test: {offenders}")
+
+    def test_the_gate_sees_the_defect_it_exists_for(self) -> None:
+        # The exact shape that slipped through: an extracted helper placed
+        # between the env gate and the class it was written to guard.
+        defect = ast.parse(
+            "import unittest\n"
+            "@unittest.skipUnless(True, 'reason')\n"
+            "def seal_v1():\n"
+            "    return 1\n"
+            "class T(unittest.TestCase):\n"
+            "    pass\n"
+        )
+        functions = [
+            node
+            for node in defect.body
+            if isinstance(node, ast.FunctionDef)
+            and any(_is_unittest_skip_v1(item) for item in node.decorator_list)
+        ]
+        self.assertEqual([node.name for node in functions], ["seal_v1"])
+
+        healthy = ast.parse(
+            "import unittest\n"
+            "def seal_v1():\n"
+            "    return 1\n"
+            "@unittest.skipUnless(True, 'reason')\n"
+            "class T(unittest.TestCase):\n"
+            "    @unittest.skipIf(False, 'reason')\n"
+            "    def test_x(self):\n"
+            "        pass\n"
+        )
+        self.assertEqual(
+            [
+                node.name
+                for node in healthy.body
+                if isinstance(node, ast.FunctionDef)
+                and any(_is_unittest_skip_v1(item) for item in node.decorator_list)
+            ],
+            [],
+        )
+
+
+if __name__ == "__main__":
+    unittest.main(verbosity=2)
diff --git a/proof/region/v1/tests/test_executor.py b/proof/region/v1/tests/test_executor.py
index 2e24fc58..4892459d 100644
--- a/proof/region/v1/tests/test_executor.py
+++ b/proof/region/v1/tests/test_executor.py
@@ -1830,6 +1830,67 @@ def test_observer_cgroup_placement_supports_search_only_directories(self) -> Non
                 parent.chmod(0o755)
             self.assertEqual(procs.read_bytes(), str(os.getpid()).encode("ascii"))
 
+    def test_task_cgroup_placement_writes_this_pid_into_the_named_group(self) -> None:
+        # A controller that observed one execution stays in that observer,
+        # whose subtree admits two tasks.  Returning to the unconstrained
+        # group is what lets the same process observe a second engine: without
+        # it the next BUILD forks into a full subtree.
+        with tempfile.TemporaryDirectory() as temporary:
+            group = Path(temporary).resolve() / "tasks"
+            group.mkdir(parents=True)
+            procs = group / "cgroup.procs"
+            procs.write_bytes(b"")
+            # The placement's own post-condition reads the real cgroup of this
+            # process, which no fixture can move it into.
+            with mock.patch.object(
+                executor, "_current_unified_cgroup_v1", return_value=group
+            ):
+                executor.enter_task_cgroup_v1(group)
+            self.assertEqual(procs.read_bytes(), str(os.getpid()).encode("ascii"))
+
+    def test_task_cgroup_placement_refuses_when_it_did_not_land(self) -> None:
+        # The write can succeed while the process ends up elsewhere; without
+        # this check a misconfigured path silently moves where the next BUILD
+        # runs, and nothing downstream looks at that.
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary).resolve()
+            group = root / "tasks"
+            group.mkdir(parents=True)
+            (group / "cgroup.procs").write_bytes(b"")
+            elsewhere = root / "elsewhere"
+            elsewhere.mkdir()
+            with mock.patch.object(
+                executor, "_current_unified_cgroup_v1", return_value=elsewhere
+            ):
+                with self.assertRaises(OSError):
+                    executor.enter_task_cgroup_v1(group)
+
+    def test_task_cgroup_placement_rejects_invalid_group_values(self) -> None:
+        for invalid in (
+            object(),
+            Path("relative"),
+            Path("/absolute\0"),
+            Path("/absolute\ud800"),
+            "/absolute",
+        ):
+            with self.subTest(invalid=invalid):
+                with self.assertRaises(TypeError):
+                    executor.enter_task_cgroup_v1(invalid)  # type: ignore[arg-type]
+
+    def test_task_cgroup_placement_refuses_a_symlinked_procs_file(self) -> None:
+        # Same law as the observer placement: a pathname would follow the
+        # link before this controller could prove which group it entered.
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary).resolve()
+            group = root / "tasks"
+            group.mkdir(parents=True)
+            elsewhere = root / "elsewhere"
+            elsewhere.write_bytes(b"")
+            (group / "cgroup.procs").symlink_to(elsewhere)
+            with self.assertRaises(OSError):
+                executor.enter_task_cgroup_v1(group)
+            self.assertEqual(elsewhere.read_bytes(), b"")
+
     def test_observer_cgroup_placement_rejects_invalid_parent_values(self) -> None:
         for invalid in (
             object(),
diff --git a/proof/region/v1/tests/test_workflow_inputs.py b/proof/region/v1/tests/test_workflow_inputs.py
new file mode 100644
index 00000000..bf93a84c
--- /dev/null
+++ b/proof/region/v1/tests/test_workflow_inputs.py
@@ -0,0 +1,140 @@
+#!/usr/bin/env python3
+"""A workflow that reads an input it never declared, caught before it runs.
+
+`${{ inputs.x }}` on an undeclared input is not an error in GitHub Actions —
+it expands to the empty string.  So a one-letter drift between the input's
+declaration and its use costs a whole dispatched run to discover, and the
+proof workflows are the expensive kind: the dual-proof job would have spent
+two hours of native execution before noticing its lane cover was empty.
+
+The dispatch workflows are pinned elsewhere by naming the coordinates they
+must carry (`test_verification_dispatch.py`).  That catches a missing
+coordinate but not a misspelt one, which is the defect that actually
+happened.  This gate closes the class for every workflow at once, without a
+YAML parser the proof tree does not have.
+"""
+
+from __future__ import annotations
+
+import re
+import unittest
+from pathlib import Path
+
+PROOF = Path(__file__).resolve().parents[1]
+REPO = PROOF.parents[2]
+WORKFLOWS = REPO / ".github" / "workflows"
+
+_INPUT_REFERENCE_V1 = re.compile(r"\$\{\{\s*(?:github\.event\.)?inputs\.([A-Za-z0-9_-]+)")
+_DECLARED_INPUT_V1 = re.compile(r"^      ([A-Za-z0-9_-]+):\s*$")
+_INPUTS_BLOCK_V1 = re.compile(r"^    inputs:\s*$")
+
+
+def _declared_inputs_v1(text: str) -> frozenset[str]:
+    """Input names under `workflow_dispatch:`/`workflow_call:`.
+
+    Read by indentation rather than parsed: the proof tree carries no YAML
+    dependency, and every workflow here is written at the canonical depth.
+    """
+
+    names = []
+    inside = False
+    for line in text.splitlines():
+        if _INPUTS_BLOCK_V1.match(line):
+            inside = True
+            continue
+        if inside:
+            match = _DECLARED_INPUT_V1.match(line)
+            if match:
+                names.append(match.group(1))
+                continue
+            if line.strip() and not line.startswith("        "):
+                inside = False
+    return frozenset(names)
+
+
+class WorkflowInputReferenceTests(unittest.TestCase):
+    def test_every_referenced_input_is_declared(self) -> None:
+        offenders = []
+        checked = 0
+        for workflow in sorted(WORKFLOWS.glob("*.yml")):
+            text = workflow.read_text(encoding="utf-8")
+            referenced = frozenset(_INPUT_REFERENCE_V1.findall(text))
+            if not referenced:
+                continue
+            checked += 1
+            for name in sorted(referenced - _declared_inputs_v1(text)):
+                offenders.append(f"{workflow.name}: {name}")
+        self.assertEqual(offenders, [], f"undeclared workflow inputs: {offenders}")
+        # Anti-vacuity: a gate that checked nothing would also pass.
+        self.assertGreater(checked, 0)
+
+    def test_the_gate_sees_a_misspelt_reference(self) -> None:
+        # The exact drift that happened: the input was declared plural and
+        # read singular, so the job silently received an empty string.
+        drifted = (
+            "on:\n"
+            "  workflow_dispatch:\n"
+            "    inputs:\n"
+            "      lane_run_ids:\n"
+            "        required: true\n"
+            "jobs:\n"
+            "  one:\n"
+            "    steps:\n"
+            "      - run: echo ${{ inputs.lane_run_id }}\n"
+        )
+        self.assertEqual(_declared_inputs_v1(drifted), frozenset({"lane_run_ids"}))
+        self.assertEqual(
+            frozenset(_INPUT_REFERENCE_V1.findall(drifted)), frozenset({"lane_run_id"})
+        )
+
+        healthy = drifted.replace("inputs.lane_run_id }}", "inputs.lane_run_ids }}")
+        self.assertEqual(
+            frozenset(_INPUT_REFERENCE_V1.findall(healthy))
+            - _declared_inputs_v1(healthy),
+            frozenset(),
+        )
+
+
+class DualProofContainmentContractTests(unittest.TestCase):
+    """The dual-proof job must not share one observer subtree between engines."""
+
+    def setUp(self) -> None:
+        workflow = WORKFLOWS / "dual-proof.yml"
+        self.assertTrue(workflow.is_file(), "dual-proof.yml is missing")
+        self.text = workflow.read_text(encoding="utf-8")
+
+    def test_each_engine_gets_its_own_observer_subtree(self) -> None:
+        # A shared subtree admits two tasks, and the controller stays in the
+        # observer it entered: the second engine's BUILD would fork into a
+        # full budget and die an hour into the run.
+        for group in ("proof-arb", "proof-mpfi"):
+            self.assertIn(f"{group}/observer", self.text)
+        self.assertIn("LABCOLORS_DUAL_PROOF_CGROUP_TASKS", self.text)
+        self.assertNotIn("LABCOLORS_EXECUTOR_CGROUP_V1=", self.text)
+
+    def test_the_cover_is_gathered_from_many_runs(self) -> None:
+        # One lane is one dispatch is one run, so a full-domain cover never
+        # lives in a single run id.
+        self.assertIn("lane_run_ids", self.text)
+        self.assertIn("verification-lane-*", self.text)
+        self.assertNotIn("run-id:", self.text)
+
+    def test_two_runs_cannot_quietly_claim_one_lane(self) -> None:
+        # Downloading straight into one directory lets a re-run of the same
+        # window overwrite the evidence already there: the cover still looks
+        # exact while one of two answers silently won.
+        self.assertIn("staged/", self.text)
+        self.assertIn("one would silently win", self.text)
+
+    def test_a_lane_run_id_that_is_not_a_number_is_refused(self) -> None:
+        # An element starting with `-` would be read by `gh` as a flag.
+        self.assertIn("''|*[!0-9]*)", self.text)
+
+    def test_the_cover_is_checked_before_anything_is_built(self) -> None:
+        cover_check = self.text.index("refuse an incomplete cover")
+        first_build = self.text.index("seal the full-domain dual proof")
+        self.assertLess(cover_check, first_build)
+
+
+if __name__ == "__main__":
+    unittest.main(verbosity=2)