diff --git a/Library/scripts/library_substrate_image.py b/Library/scripts/library_substrate_image.py
index c8268d5..36e3b2e 100644
--- a/Library/scripts/library_substrate_image.py
+++ b/Library/scripts/library_substrate_image.py
@@ -18,7 +18,7 @@
 import tempfile
 from collections.abc import Mapping, Sequence
 from pathlib import Path, PurePosixPath
-from typing import Final, NoReturn, cast
+from typing import Final, Literal, NoReturn, cast
 
 if __package__ in {None, ""}:
     repository_root = str(Path(__file__).resolve().parents[2])
@@ -52,9 +52,11 @@
 HELPER_ROOT: Final = WORKER_ROOT / "library-substrate"
 ASSETS: Final = {
     "AutoleanLibrarySubstrateInventory.lean": "INVENTORY_HELPER_SHA256",
+    "AutoleanLibrarySubstrateV2Query.lean": "V2_FACADE_QUERY_HELPER_SHA256",
     "autolean-library-substrate-build": "BUILD_TOOL_SHA256",
     "autolean-library-substrate-build-receipt": "RECEIPT_TOOL_SHA256",
     "autolean-library-substrate-independent-query": "QUERY_WRAPPER_SHA256",
+    "autolean-library-substrate-v2-facade": "V2_FACADE_WRAPPER_SHA256",
 }
 RUNTIME_MANIFEST_SCHEMA: Final = "autolean.library-substrate-runtime-manifest.v1"
 DECLARATION_INVENTORY_SCHEMA: Final = "autolean.library-substrate-declaration-inventory.v1"
@@ -63,6 +65,34 @@
 CANARY_SCHEMA: Final = "autolean.library-substrate-independent-canary.v1"
 RUNTIME_SOURCE_CHECKSUM_FILENAME: Final = "runtime-sources.sha256"
 RUNTIME_FILE_CHECKSUM_FILENAME: Final = "runtime-files.sha256"
+V2_FACADE_CANARY_SCHEMA: Final = "autolean.library-substrate-v2-facade-canary.v2"
+V2_WRAPPER_PATH: Final = "/opt/autolean/bin/autolean-lean-wrapper"
+V2_QUERY_HELPER_PATH: Final = "/opt/autolean/lib/AutoleanLeanQuery.lean"
+V2_RESULT_SCHEMA: Final = "autolean.oci-lean-wrapper.v2"
+V2_LAKE_MANIFEST_SHA256: Final = "e2a93c904f51195d6740cd9abfb35ab155dc0157e0e46642dce0d364b68a9a89"
+V2_FACADE_FAILURE_DIAGNOSTIC_LIMIT: Final = 4096
+V2_COMPOSITIONAL_CANDIDATE_SHA256: Final = (
+    "98cd1d2ae8f48ca368d19c64ddec447185bf13753a8d87dbf79df49bf33a7f78"
+)
+V2_TARGET_IMPORT_SOURCE: Final = (
+    "import AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Targets.ClosedSound\n"
+)
+V2_TARGET_IMPORT_SOURCE_SHA256: Final = (
+    "c1725f40b0091501aaf465cefe318231af157b51ab3ffef9a8669bcb09ee4d4a"
+)
+V2_WRONG_TARGET_TYPE_SOURCE: Final = """\
+import AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude
+
+namespace AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK
+
+theorem Deriv.closed_sound : True := by
+  trivial
+
+end AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK
+"""
+V2_WRONG_TARGET_TYPE_SOURCE_SHA256: Final = (
+    "f938b08d4e6d9de5e0288207f68ccc3122a5bd96dc08c885b71ba98a52919323"
+)
 
 
 class SubstrateImageError(RuntimeError):
@@ -604,6 +634,23 @@ def _image_file_sha256_and_size(image: str, path: str, *, label: str) -> tuple[s
     return digest_fields[0], int(size_fields[0])
 
 
+def _image_file_sha256(image: str, path: str, *, label: str) -> str:
+    output = _run(
+        [
+            *_docker_run_base(),
+            "--entrypoint",
+            "/usr/bin/sha256sum",
+            image,
+            path,
+        ],
+        timeout=120,
+    ).stdout.strip()
+    fields = output.split(maxsplit=1)
+    if len(fields) != 2 or not SHA256_RE.fullmatch(fields[0]):
+        fail(f"{label} hash is unavailable")
+    return fields[0]
+
+
 def _sorted_unique_strings(value: object, *, label: str) -> tuple[str, ...]:
     if not isinstance(value, list) or any(not isinstance(item, str) for item in value):
         fail(f"{label} must be a string array")
@@ -920,6 +967,53 @@ def _validate_image_build_input(
     return records, source_tree_sha256
 
 
+def _validate_host_asset_binding(build_input: Mapping[str, object]) -> None:
+    expected_assets = dict(sorted(_asset_hashes().items()))
+    if build_input.get("assets") != expected_assets:
+        fail("image-owned build input differs from the current host helper assets")
+
+
+def _validate_v2_facade_bindings(
+    receipt: Mapping[str, object],
+    build_input: Mapping[str, object],
+    *,
+    runtime_manifest_file_sha256: str,
+    facade_wrapper_sha256: str,
+    facade_query_helper_sha256: str,
+) -> None:
+    """Bind the standard V2 paths to the same immutable substrate receipt.
+
+    The facade has no protocol extension in its stdout, so its identity must be checked from the
+    image-owned receipt/build input before a host canary treats a V2 record as substrate evidence.
+    """
+
+    for field, actual in (
+        ("v2_facade_wrapper_sha256", facade_wrapper_sha256),
+        ("v2_facade_query_helper_sha256", facade_query_helper_sha256),
+    ):
+        recorded = receipt.get(field)
+        if not isinstance(recorded, str) or not SHA256_RE.fullmatch(recorded) or recorded != actual:
+            fail(f"image receipt does not bind the {field}")
+    assets = build_input.get("assets")
+    if not isinstance(assets, dict):
+        fail("substrate build input assets are unavailable")
+    expected_assets = {
+        "V2_FACADE_WRAPPER_SHA256": facade_wrapper_sha256,
+        "V2_FACADE_QUERY_HELPER_SHA256": facade_query_helper_sha256,
+    }
+    if any(assets.get(name) != digest for name, digest in expected_assets.items()):
+        fail("substrate build input does not bind the V2 facade assets")
+    target = build_input.get("target")
+    if target != {
+        "canonical_type_sha256": TARGET_TYPE_SHA256,
+        "declaration": TARGET_DECLARATION,
+        "forbidden_ordinary_dependency": SOUND_DECLARATION,
+    }:
+        fail("substrate build input target boundary differs from the V2 facade scope")
+    if receipt.get("runtime_manifest_sha256") != runtime_manifest_file_sha256:
+        fail("V2 facade receipt is not bound to the runtime manifest")
+
+
 def verify(image: str) -> dict[str, object]:
     inspected = _inspect(image)
     actual_reference = _child_image_reference(inspected)
@@ -949,6 +1043,8 @@ def verify(image: str) -> dict[str, object]:
         "runtime_source_tree_sha256",
         "schema_version",
         "task_mode",
+        "v2_facade_query_helper_sha256",
+        "v2_facade_wrapper_sha256",
     }
     if set(receipt) != expected_receipt_fields:
         fail("image receipt schema drifted")
@@ -1006,6 +1102,7 @@ def verify(image: str) -> dict[str, object]:
         "/opt/autolean/library-substrate/attestations/build-input.v1.json",
         label="substrate build input",
     )
+    _validate_host_asset_binding(build_input)
     profile, _ = _profile()
     source_checksums = _read_image_text(
         image,
@@ -1029,6 +1126,23 @@ def verify(image: str) -> dict[str, object]:
         or build_input.get("runtime_sources") != source_records
     ):
         fail("image-owned build input differs from the verified profile and parent")
+    facade_wrapper_sha256 = _image_file_sha256(
+        image,
+        V2_WRAPPER_PATH,
+        label="image-owned V2 facade wrapper",
+    )
+    facade_query_helper_sha256 = _image_file_sha256(
+        image,
+        V2_QUERY_HELPER_PATH,
+        label="image-owned V2 facade query helper",
+    )
+    _validate_v2_facade_bindings(
+        receipt,
+        build_input,
+        runtime_manifest_file_sha256=manifest_file_sha256,
+        facade_wrapper_sha256=facade_wrapper_sha256,
+        facade_query_helper_sha256=facade_query_helper_sha256,
+    )
     runtime_files, records, auxiliary = _validate_manifest(manifest, receipt=receipt)
     verified_runtime_files = _validate_runtime_file_closure(
         image,
@@ -1041,6 +1155,10 @@ def verify(image: str) -> dict[str, object]:
         "image": image,
         "image_id": image_id,
         "image_receipt_sha256": image_receipt_sha256,
+        "v2_facade_identity": {
+            "query_helper_sha256": facade_query_helper_sha256,
+            "wrapper_sha256": facade_wrapper_sha256,
+        },
         "parent_receipt_canonical_sha256": current_parent_receipt_sha256,
         "receipt": receipt,
         "runtime_file_count": len(runtime_files),
@@ -1109,6 +1227,252 @@ def _query_candidate(image: str, compiled: Path) -> dict[str, object]:
     return _json_record(output, label="independent Candidate query")
 
 
+def _v2_compile_candidate(image: str, candidate: Path, output: Path) -> Path:
+    output.mkdir()
+    output.chmod(0o777)
+    _run(
+        [
+            *_docker_run_base(),
+            "--mount",
+            f"type=bind,src={candidate.parent},dst=/input,readonly",
+            "--mount",
+            f"type=bind,src={output},dst=/output",
+            image,
+            *_v2_compile_wrapper_argv(),
+        ],
+        timeout=300,
+    )
+    compiler_output = output / "Candidate.olean"
+    if (
+        compiler_output.is_symlink()
+        or not compiler_output.is_file()
+        or compiler_output.stat().st_size <= 0
+        or compiler_output.stat().st_size > 64 * 1024 * 1024
+    ):
+        fail("V2 facade compiler did not emit a regular Candidate.olean")
+    sealed_root = output.parent / "sealed"
+    sealed_root.mkdir(mode=0o700)
+    sealed = sealed_root / "Candidate.olean"
+    sealed.write_bytes(compiler_output.read_bytes())
+    sealed.chmod(0o444)
+    return sealed
+
+
+def _v2_query_candidate(image: str, compiled: Path) -> dict[str, object]:
+    output = _run(
+        [
+            *_docker_run_base(),
+            "--mount",
+            f"type=bind,src={compiled},dst=/compiled/Candidate.olean,readonly",
+            image,
+            *_v2_query_wrapper_argv(),
+        ],
+        timeout=300,
+    ).stdout
+    return _json_record(output, label="V2 facade Candidate query")
+
+
+def _v2_compile_wrapper_argv() -> tuple[str, ...]:
+    return (
+        V2_WRAPPER_PATH,
+        "--protocol",
+        V2_RESULT_SCHEMA,
+        "--phase",
+        "compile",
+        "--candidate",
+        "/input/Candidate.lean",
+        "--output",
+        "/output/Candidate.olean",
+    )
+
+
+def _v2_query_wrapper_argv() -> tuple[str, ...]:
+    return (
+        V2_WRAPPER_PATH,
+        "--protocol",
+        V2_RESULT_SCHEMA,
+        "--phase",
+        "query",
+        "--compiled",
+        "/compiled/Candidate.olean",
+        "--declaration",
+        TARGET_DECLARATION,
+        "--type-format",
+        "autolean.lean-pp-expr.v1",
+    )
+
+
+def _v2_rejection_observation(
+    result: subprocess.CompletedProcess[str],
+    *,
+    label: str,
+    actual_phase: Literal["compile", "query"],
+    expected_phase: Literal["compile", "query"],
+    expected_returncode: int,
+    reason_marker: str,
+    candidate_source_sha256: str,
+    expected_candidate_source_sha256: str,
+) -> dict[str, object]:
+    if candidate_source_sha256 != expected_candidate_source_sha256:
+        fail(f"V2 facade {label} candidate source hash drifted")
+    if actual_phase != expected_phase:
+        fail(f"V2 facade {label} rejected during {actual_phase}, expected {expected_phase}")
+    if result.returncode != expected_returncode:
+        fail(f"V2 facade {label} returned {result.returncode}, expected {expected_returncode}")
+    if result.stdout:
+        fail(f"V2 facade {label} failure emitted stdout")
+    prefix = f"autolean-library-substrate-v2-facade: phase={expected_phase} failed"
+    stderr = result.stderr
+    maximum_bytes = len(prefix.encode("utf-8")) + V2_FACADE_FAILURE_DIAGNOSTIC_LIMIT + 8
+    if (
+        not stderr
+        or len(stderr.encode("utf-8")) > maximum_bytes
+        or prefix not in stderr
+        or reason_marker not in stderr
+    ):
+        fail(f"V2 facade {label} failure reason is unavailable or unbounded")
+    return {
+        "candidate_source_sha256": candidate_source_sha256,
+        "reason_marker": reason_marker,
+        "rejection_phase": actual_phase,
+        "returncode": result.returncode,
+        "stderr_summary": stderr.strip(),
+    }
+
+
+def _expect_v2_candidate_rejected(
+    image: str,
+    candidate: Path,
+    *,
+    label: str,
+    expected_phase: Literal["compile", "query"],
+    expected_returncode: int,
+    reason_marker: str,
+    expected_candidate_source_sha256: str,
+) -> dict[str, object]:
+    candidate_source_sha256 = _sha256_bytes(
+        _regular_bytes(candidate, label=f"V2 facade {label} candidate source")
+    )
+    with tempfile.TemporaryDirectory(
+        prefix="autolean-library-substrate-v2-negative-", dir="/tmp"
+    ) as raw:
+        output = Path(raw) / "output"
+        output.mkdir(mode=0o777)
+        output.chmod(0o777)
+        compile_result = subprocess.run(
+            [
+                *_docker_run_base(),
+                "--mount",
+                f"type=bind,src={candidate.parent},dst=/input,readonly",
+                "--mount",
+                f"type=bind,src={output},dst=/output",
+                image,
+                *_v2_compile_wrapper_argv(),
+            ],
+            check=False,
+            capture_output=True,
+            errors="replace",
+            timeout=300,
+            text=True,
+        )
+        if compile_result.returncode != 0:
+            return _v2_rejection_observation(
+                compile_result,
+                label=label,
+                actual_phase="compile",
+                expected_phase=expected_phase,
+                expected_returncode=expected_returncode,
+                reason_marker=reason_marker,
+                candidate_source_sha256=candidate_source_sha256,
+                expected_candidate_source_sha256=expected_candidate_source_sha256,
+            )
+        compiler_output = output / "Candidate.olean"
+        if (
+            compiler_output.is_symlink()
+            or not compiler_output.is_file()
+            or compiler_output.stat().st_size <= 0
+            or compiler_output.stat().st_size > 64 * 1024 * 1024
+        ):
+            fail(f"V2 facade {label} compile did not emit a regular Candidate.olean")
+        sealed_root = Path(raw) / "sealed"
+        sealed_root.mkdir(mode=0o700)
+        sealed = sealed_root / "Candidate.olean"
+        sealed.write_bytes(compiler_output.read_bytes())
+        sealed.chmod(0o444)
+        query_result = subprocess.run(
+            [
+                *_docker_run_base(),
+                "--mount",
+                f"type=bind,src={sealed},dst=/compiled/Candidate.olean,readonly",
+                image,
+                *_v2_query_wrapper_argv(),
+            ],
+            check=False,
+            capture_output=True,
+            errors="replace",
+            timeout=300,
+            text=True,
+        )
+    if query_result.returncode == 0:
+        fail("V2 facade accepted a candidate that the substrate policy must reject")
+    return _v2_rejection_observation(
+        query_result,
+        label=label,
+        actual_phase="query",
+        expected_phase=expected_phase,
+        expected_returncode=expected_returncode,
+        reason_marker=reason_marker,
+        candidate_source_sha256=candidate_source_sha256,
+        expected_candidate_source_sha256=expected_candidate_source_sha256,
+    )
+
+
+def _validate_v2_facade_record(
+    record: Mapping[str, object], *, identity: Mapping[str, str]
+) -> dict[str, object]:
+    expected_fields = {
+        "schema_version",
+        "declaration",
+        "canonical_type",
+        "lean_version",
+        "mathlib_revision",
+        "lake_manifest_hash",
+        "observed_axioms",
+        "image_identity",
+    }
+    if set(record) != expected_fields:
+        fail("V2 facade query record schema drifted")
+    canonical_type = record.get("canonical_type")
+    if (
+        not isinstance(canonical_type, str)
+        or _sha256_bytes(canonical_type.encode("utf-8")) != TARGET_TYPE_SHA256
+    ):
+        fail("V2 facade did not preserve the historical target type hash")
+    axioms = _sorted_unique_strings(record.get("observed_axioms"), label="V2 facade axioms")
+    expected_identity = {
+        "schema_version": "autolean.image-owned-verifier-identity.v2",
+        "wrapper_path": V2_WRAPPER_PATH,
+        "wrapper_sha256": identity["wrapper_sha256"],
+        "query_helper_path": V2_QUERY_HELPER_PATH,
+        "query_helper_sha256": identity["query_helper_sha256"],
+    }
+    if (
+        record.get("schema_version") != V2_RESULT_SCHEMA
+        or record.get("declaration") != TARGET_DECLARATION
+        or record.get("lean_version") != "v4.28.0"
+        or record.get("mathlib_revision") != EXPECTED_MATHLIB_REVISION
+        or record.get("lake_manifest_hash") != V2_LAKE_MANIFEST_SHA256
+        or axioms != EXPECTED_TARGET_AXIOMS
+        or record.get("image_identity") != expected_identity
+    ):
+        fail("V2 facade record differs from the fixed independent substrate profile")
+    return {
+        "canonical_type_sha256": TARGET_TYPE_SHA256,
+        "observed_axioms": list(axioms),
+        "standard_v2_record": True,
+    }
+
+
 def _validate_query(
     query: dict[str, object],
     *,
@@ -1273,7 +1637,6 @@ def canary(image: str) -> dict[str, object]:
             "no_contract_or_gateway_integration",
             "no_external_dependency_capsule",
             "no_formal_asset_admission",
-            "no_oci_lean_runner_v2_adapter",
             "no_provider_execution",
             "no_v2_evidence_or_gateway_receipt",
         ],
@@ -1285,6 +1648,100 @@ def canary(image: str) -> dict[str, object]:
     }
 
 
+def v2_facade_canary(image: str) -> dict[str, object]:
+    """Exercise the unchanged V2 argv and result shape against one recorded child digest."""
+
+    verified = verify(image)
+    identity = cast(dict[str, str], verified["v2_facade_identity"])
+    with tempfile.TemporaryDirectory(
+        prefix="autolean-library-substrate-v2-facade-", dir="/tmp"
+    ) as raw:
+        root = Path(raw)
+        candidate, candidate_sha256 = _snapshot_candidate(root / "independent")
+        compiled = _v2_compile_candidate(image, candidate, root / "compiled")
+        record = _v2_query_candidate(image, compiled)
+
+        compositional_root = root / "compositional"
+        compositional_root.mkdir()
+        compositional_candidate = compositional_root / "Candidate.lean"
+        compositional_candidate.write_bytes(
+            _regular_bytes(
+                FIXTURE_ROOT / "candidates" / "compositional_bridge" / "Candidate.lean",
+                label="compositional Candidate source",
+            )
+        )
+        compositional_candidate.chmod(0o444)
+        compositional_rejection = _expect_v2_candidate_rejected(
+            image,
+            compositional_candidate,
+            label="compositional",
+            expected_phase="compile",
+            expected_returncode=20,
+            reason_marker="Targets/DerivSound.olean",
+            expected_candidate_source_sha256=V2_COMPOSITIONAL_CANDIDATE_SHA256,
+        )
+
+        target_import_root = root / "target-import"
+        target_import_root.mkdir()
+        target_import_candidate = target_import_root / "Candidate.lean"
+        target_import_candidate.write_text(
+            V2_TARGET_IMPORT_SOURCE,
+            encoding="utf-8",
+            newline="\n",
+        )
+        target_import_candidate.chmod(0o444)
+        target_import_rejection = _expect_v2_candidate_rejected(
+            image,
+            target_import_candidate,
+            label="target-import",
+            expected_phase="compile",
+            expected_returncode=20,
+            reason_marker="Targets/ClosedSound.olean",
+            expected_candidate_source_sha256=V2_TARGET_IMPORT_SOURCE_SHA256,
+        )
+
+        wrong_target_type_root = root / "wrong-target-type"
+        wrong_target_type_root.mkdir()
+        wrong_target_type_candidate = wrong_target_type_root / "Candidate.lean"
+        wrong_target_type_candidate.write_text(
+            V2_WRONG_TARGET_TYPE_SOURCE,
+            encoding="utf-8",
+            newline="\n",
+        )
+        wrong_target_type_candidate.chmod(0o444)
+        wrong_target_type_rejection = _expect_v2_candidate_rejected(
+            image,
+            wrong_target_type_candidate,
+            label="wrong-target-type",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker="Candidate target type differs from the historical frozen hash",
+            expected_candidate_source_sha256=V2_WRONG_TARGET_TYPE_SOURCE_SHA256,
+        )
+
+    observation = _validate_v2_facade_record(record, identity=identity)
+    return {
+        "authority": "operator-local-v2-compatible-preflight-only",
+        "candidate_source_sha256": candidate_sha256,
+        "image": image,
+        "image_id": verified["image_id"],
+        "negative_cases": {
+            "compositional_candidate": compositional_rejection,
+            "target_import_candidate": target_import_rejection,
+            "wrong_target_type_candidate": wrong_target_type_rejection,
+        },
+        "non_claims": [
+            "no_contract_or_gateway_integration",
+            "no_formal_asset_admission",
+            "no_provider_execution",
+            "no_t6_completion",
+        ],
+        "observation": observation,
+        "schema_version": V2_FACADE_CANARY_SCHEMA,
+        "task_mode": "independent_reproof",
+    }
+
+
 def _wsl_path(path: Path) -> str:
     completed = _run(
         ["wsl.exe", "-d", WSL_DISTRIBUTION, "-e", "wslpath", "-a", str(path)],
@@ -1317,11 +1774,11 @@ def _delegate_to_wsl(arguments: argparse.Namespace) -> int:
 
 def parse_arguments(arguments: Sequence[str] | None = None) -> argparse.Namespace:
     parser = argparse.ArgumentParser(description=__doc__)
-    parser.add_argument("action", choices=("build", "verify", "canary", "all"))
+    parser.add_argument("action", choices=("build", "verify", "canary", "facade-canary", "all"))
     parser.add_argument("--image")
     parser.add_argument("--native", action="store_true", help=argparse.SUPPRESS)
     parsed = parser.parse_args(arguments)
-    if parsed.action in {"verify", "canary"} and parsed.image is None:
+    if parsed.action in {"verify", "canary", "facade-canary"} and parsed.image is None:
         parser.error(f"{parsed.action} requires --image")
     if parsed.action in {"build", "all"} and parsed.image is not None:
         parser.error(f"{parsed.action} does not accept --image")
@@ -1339,11 +1796,14 @@ def main(arguments: Sequence[str] | None = None) -> int:
             result = verify(cast(str, parsed.image))
         elif parsed.action == "canary":
             result = canary(cast(str, parsed.image))
+        elif parsed.action == "facade-canary":
+            result = v2_facade_canary(cast(str, parsed.image))
         else:
             build_result = build()
             result = {
                 "build": build_result,
                 "canary": canary(cast(str, build_result["image"])),
+                "v2_facade_canary": v2_facade_canary(cast(str, build_result["image"])),
                 "schema_version": "autolean.library-substrate-image-all.v1",
             }
         print(json.dumps(result, ensure_ascii=True, sort_keys=True))
diff --git a/Prover/tests/test_oci_lean_runner.py b/Prover/tests/test_oci_lean_runner.py
index c44bd75..200797f 100644
--- a/Prover/tests/test_oci_lean_runner.py
+++ b/Prover/tests/test_oci_lean_runner.py
@@ -8,7 +8,12 @@
 from pathlib import Path
 
 import pytest
-from autolean_contracts import HashKindV1, ProofSubmissionV1, digest_text
+from autolean_contracts import (
+    HashKindV1,
+    OciVerifierExecutionPolicyV2,
+    ProofSubmissionV1,
+    digest_text,
+)
 from autolean_prover.errors import ValidationError
 from autolean_prover.execution import (
     MaterializedWorkspace,
@@ -186,33 +191,12 @@ def test_oci_lean_runner_uses_fixed_wrapper_argv_and_emits_execution_evidence(tm
     assert len(harness.requests) == 2
     compile_argv = harness.requests[0].argv
     query_argv = harness.requests[1].argv
+    policy = workspace.bundle.contract.formal.environment.verifier_execution_policy
+    assert isinstance(policy, OciVerifierExecutionPolicyV2)
     compile_image_index = compile_argv.index(spec.image)
-    assert compile_argv[compile_image_index:] == (
-        spec.image,
-        "/opt/autolean/bin/autolean-lean-wrapper",
-        "--protocol",
-        "autolean.oci-lean-wrapper.v2",
-        "--phase",
-        "compile",
-        "--candidate",
-        "/input/Candidate.lean",
-        "--output",
-        "/output/Candidate.olean",
-    )
-    image_index = query_argv.index(spec.image)
-    assert query_argv[image_index:] == (
-        spec.image,
-        "/opt/autolean/bin/autolean-lean-wrapper",
-        "--protocol",
-        "autolean.oci-lean-wrapper.v2",
-        "--phase",
-        "query",
-        "--compiled",
-        "/compiled/Candidate.olean",
-        "--declaration",
-        bundle.proof_boundary.expected_declaration,
-        "--type-format",
-        "autolean.lean-pp-expr.v1",
+    assert compile_argv[compile_image_index + 1 :] == policy.compile_wrapper_argv()
+    assert query_argv[query_argv.index(spec.image) + 1 :] == policy.wrapper_argv(
+        bundle.proof_boundary.expected_declaration
     )
     for argv in (compile_argv, query_argv):
         assert (argv[argv.index("--network")], argv[argv.index("--network") + 1]) == (
diff --git a/Prover/worker/Dockerfile.library-substrate b/Prover/worker/Dockerfile.library-substrate
index abd8461..bbb1e9e 100644
--- a/Prover/worker/Dockerfile.library-substrate
+++ b/Prover/worker/Dockerfile.library-substrate
@@ -12,6 +12,8 @@ ARG QUERY_WRAPPER_SHA256
 ARG RECEIPT_TOOL_SHA256
 ARG RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256
 ARG RUNTIME_SOURCE_TREE_SHA256
+ARG V2_FACADE_QUERY_HELPER_SHA256
+ARG V2_FACADE_WRAPPER_SHA256
 
 COPY build-input.v1.json /build/input/build-input.v1.json
 COPY runtime-sources.sha256 /build/input/runtime-sources.sha256
@@ -20,6 +22,8 @@ COPY helpers/AutoleanLibrarySubstrateInventory.lean /build/tools/AutoleanLibrary
 COPY helpers/autolean-library-substrate-build /build/tools/autolean-library-substrate-build
 COPY helpers/autolean-library-substrate-independent-query /build/tools/autolean-library-substrate-independent-query
 COPY helpers/autolean-library-substrate-build-receipt /build/tools/autolean-library-substrate-build-receipt
+COPY helpers/AutoleanLibrarySubstrateV2Query.lean /build/tools/AutoleanLibrarySubstrateV2Query.lean
+COPY helpers/autolean-library-substrate-v2-facade /build/tools/autolean-library-substrate-v2-facade
 COPY Dockerfile.library-substrate /build/tools/Dockerfile.library-substrate
 
 RUN /build/tools/autolean-library-substrate-build \
@@ -32,7 +36,9 @@ RUN /build/tools/autolean-library-substrate-build \
       "${QUERY_WRAPPER_SHA256}" \
       "${RECEIPT_TOOL_SHA256}" \
       "${RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256}" \
-      "${RUNTIME_SOURCE_TREE_SHA256}"
+      "${RUNTIME_SOURCE_TREE_SHA256}" \
+      "${V2_FACADE_QUERY_HELPER_SHA256}" \
+      "${V2_FACADE_WRAPPER_SHA256}"
 
 FROM autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6
 
@@ -51,10 +57,20 @@ LABEL org.opencontainers.image.title="AutoLean library-substrate-v1 preflight" \
 
 COPY --from=library-substrate-builder --chown=0:0 \
   /build/final/ /opt/autolean/library-substrate/
+COPY --from=library-substrate-builder --chown=0:0 \
+  /build/final/bin/autolean-library-substrate-v2-facade \
+  /opt/autolean/bin/autolean-lean-wrapper
+COPY --from=library-substrate-builder --chown=0:0 \
+  /build/tools/AutoleanLibrarySubstrateV2Query.lean \
+  /opt/autolean/lib/AutoleanLeanQuery.lean
 
 RUN test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt \
     && test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query \
+    && test -x /opt/autolean/bin/autolean-lean-wrapper \
+    && test -f /opt/autolean/lib/AutoleanLeanQuery.lean \
     && test -z "$(find /opt/autolean/library-substrate -name '*.lean' -o -name '*.ilean')" \
+    && chmod 0555 /opt/autolean/bin/autolean-lean-wrapper \
+    && chmod 0444 /opt/autolean/lib/AutoleanLeanQuery.lean \
     && /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt >/dev/null
 
 USER 65532:65532
diff --git a/Prover/worker/library-substrate/AutoleanLibrarySubstrateV2Query.lean b/Prover/worker/library-substrate/AutoleanLibrarySubstrateV2Query.lean
new file mode 100644
index 0000000..035929f
--- /dev/null
+++ b/Prover/worker/library-substrate/AutoleanLibrarySubstrateV2Query.lean
@@ -0,0 +1,64 @@
+import Mathlib.ModelTheory.Semantics
+import Lean.PrettyPrinter
+import Lean.Util.CollectAxioms
+
+open Lean
+
+private def canonicalOptions : Options :=
+  ((((({} : Options).setBool `pp.all true).setBool `pp.explicit true).setBool
+        `pp.universes true).setBool `pp.notation false).set `pp.width (1000000 : Nat)
+
+private def canonicalType (env : Environment) (declaration : Name) : IO String := do
+  let some info := env.checked.get.find? declaration
+    | throw <| IO.userError s!"declaration not found: {declaration}"
+  if info.type.hasMVar then
+    throw <| IO.userError "declaration type contains a metavariable"
+  let rendered :=
+    (← PrettyPrinter.ppExprLegacy env {} {} canonicalOptions info.type).pretty 1000000
+  if rendered.isEmpty || rendered.length > 1000000 then
+    throw <| IO.userError "canonical declaration type is outside the verifier limit"
+  if rendered.any fun char => char == '\x00' || char == '\n' || char == '\r' then
+    throw <| IO.userError "canonical declaration type is not one line"
+  return rendered
+
+private def observedAxioms (env : Environment) (declaration : Name) : IO (Array Name) := do
+  let context : Core.Context := {
+    fileName := "<AutoLeanLibrarySubstrateV2Query>"
+    fileMap := default
+    options := canonicalOptions
+  }
+  let state : Core.State := { env := env }
+  let axioms ← Core.CoreM.toIO' (collectAxioms declaration) context state
+  return Array.qsort axioms fun left right => left.toString < right.toString
+
+private def query (declarationText wrapperSha256 queryHelperSha256 : String) : IO Json := do
+  let environment ← importModules #[{ module := `Candidate }] canonicalOptions
+  let declaration := declarationText.toName
+  return Json.mkObj [
+    ("schema_version", Json.str "autolean.oci-lean-wrapper.v2"),
+    ("declaration", Json.str declarationText),
+    ("canonical_type", Json.str (← canonicalType environment declaration)),
+    ("lean_version", Json.str "v4.28.0"),
+    ("mathlib_revision", Json.str "8f9d9cff6bd728b17a24e163c9402775d9e6a365"),
+    ("lake_manifest_hash",
+      Json.str "e2a93c904f51195d6740cd9abfb35ab155dc0157e0e46642dce0d364b68a9a89"),
+    ("observed_axioms", Json.arr <| (← observedAxioms environment declaration).map fun name =>
+      Json.str name.toString),
+    ("image_identity", Json.mkObj [
+      ("schema_version", Json.str "autolean.image-owned-verifier-identity.v2"),
+      ("wrapper_path", Json.str "/opt/autolean/bin/autolean-lean-wrapper"),
+      ("wrapper_sha256", Json.str wrapperSha256),
+      ("query_helper_path", Json.str "/opt/autolean/lib/AutoleanLeanQuery.lean"),
+      ("query_helper_sha256", Json.str queryHelperSha256)
+    ])
+  ]
+
+def main (arguments : List String) : IO UInt32 := do
+  try
+    let [declaration, wrapperSha256, queryHelperSha256] := arguments
+      | throw <| IO.userError "expected declaration and image-owned identity arguments"
+    IO.println (← query declaration wrapperSha256 queryHelperSha256).compress
+    return (0 : UInt32)
+  catch error =>
+    IO.eprintln s!"autolean-library-substrate-v2-query: {error}"
+    return (2 : UInt32)
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-build b/Prover/worker/library-substrate/autolean-library-substrate-build
index 76abc7d..be0711d 100644
--- a/Prover/worker/library-substrate/autolean-library-substrate-build
+++ b/Prover/worker/library-substrate/autolean-library-substrate-build
@@ -6,7 +6,7 @@ fail() {
   exit 2
 }
 
-[ "$#" -eq 10 ] || fail "expected the frozen build argument profile"
+[ "$#" -eq 12 ] || fail "expected the frozen build argument profile"
 build_input_sha256=$1
 build_tool_sha256=$2
 dockerfile_sha256=$3
@@ -17,6 +17,8 @@ query_wrapper_sha256=$7
 receipt_tool_sha256=$8
 runtime_source_checksum_manifest_sha256=$9
 runtime_source_tree_sha256=${10}
+v2_facade_query_helper_sha256=${11}
+v2_facade_wrapper_sha256=${12}
 
 for digest in "$@"; do
   case "$digest" in
@@ -50,6 +52,10 @@ test "$(sha256sum "$tools/autolean-library-substrate-independent-query" | awk '{
   "$query_wrapper_sha256"
 test "$(sha256sum "$tools/autolean-library-substrate-build-receipt" | awk '{print $1}')" = \
   "$receipt_tool_sha256"
+test "$(sha256sum "$tools/AutoleanLibrarySubstrateV2Query.lean" | awk '{print $1}')" = \
+  "$v2_facade_query_helper_sha256"
+test "$(sha256sum "$tools/autolean-library-substrate-v2-facade" | awk '{print $1}')" = \
+  "$v2_facade_wrapper_sha256"
 test "$(sha256sum "$parent_receipt" | awk '{print $1}')" = \
   "$parent_receipt_file_sha256"
 test "$(
@@ -187,6 +193,8 @@ cp "$tools/autolean-library-substrate-independent-query" \
   "$final/bin/autolean-library-substrate-independent-query"
 cp "$tools/autolean-library-substrate-build-receipt" \
   "$final/bin/autolean-library-substrate-build-receipt"
+cp "$tools/autolean-library-substrate-v2-facade" \
+  "$final/bin/autolean-library-substrate-v2-facade"
 chmod 0555 "$final/bin/"*
 find "$final/lib" -type f -exec chmod 0444 {} \;
 find "$final/attestations" -type f -exec chmod 0444 {} \;
@@ -254,6 +262,8 @@ runtime_manifest_sha256=$(
   printf '"runtime_manifest_sha256":"%s",' "$runtime_manifest_sha256"
   printf '"runtime_source_checksum_manifest_sha256":"%s",' "$runtime_source_checksum_manifest_sha256"
   printf '"runtime_source_tree_sha256":"%s",' "$runtime_source_tree_sha256"
+  printf '"v2_facade_query_helper_sha256":"%s",' "$v2_facade_query_helper_sha256"
+  printf '"v2_facade_wrapper_sha256":"%s",' "$v2_facade_wrapper_sha256"
   printf '"schema_version":"autolean.library-substrate-image-receipt.v1",'
   printf '"task_mode":"independent_reproof"'
   printf '}\n'
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-build-receipt b/Prover/worker/library-substrate/autolean-library-substrate-build-receipt
index 04b51dc..153dc2b 100644
--- a/Prover/worker/library-substrate/autolean-library-substrate-build-receipt
+++ b/Prover/worker/library-substrate/autolean-library-substrate-build-receipt
@@ -49,6 +49,8 @@ check_hash runtime_source_checksum_manifest_sha256 "$runtime_sources"
 check_hash query_wrapper_sha256 \
   "$root/bin/autolean-library-substrate-independent-query"
 check_hash receipt_tool_sha256 "$root/bin/autolean-library-substrate-build-receipt"
+check_hash v2_facade_wrapper_sha256 /opt/autolean/bin/autolean-lean-wrapper
+check_hash v2_facade_query_helper_sha256 /opt/autolean/lib/AutoleanLeanQuery.lean
 check_hash parent_receipt_file_sha256 \
   /opt/autolean/attestations/mathlib-source-build-receipt.v2.json
 
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-independent-query b/Prover/worker/library-substrate/autolean-library-substrate-independent-query
index a3edb6e..198005f 100644
--- a/Prover/worker/library-substrate/autolean-library-substrate-independent-query
+++ b/Prover/worker/library-substrate/autolean-library-substrate-independent-query
@@ -41,6 +41,14 @@ import Lean.Util.FoldConsts
 
 open Lean
 
+private def targetTypeSha256 :=
+  "66d1fe3cbd2a62831bf57b9761248bf3fa5d84b95879be25c7e591c48ebeef8a"
+
+private def expectedAxioms : Array String := #["Classical.choice", "Quot.sound", "propext"]
+
+private def forbiddenDirectDependency :=
+  `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.sound
+
 private def runtimeModules : Array (Name × System.FilePath) := #[
   (`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core,
     "/opt/autolean/library-substrate/lib/lean/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core.olean"),
@@ -80,6 +88,17 @@ private def canonicalType (environment : Environment) (info : ConstantInfo) : IO
     throw <| IO.userError s!"canonical type is not one line: {info.name}"
   return rendered
 
+private def sha256Text (value : String) : IO String := do
+  let path : System.FilePath := "/tmp/autolean-library-substrate-query-type.txt"
+  IO.FS.writeFile path value
+  let output ← IO.Process.output { cmd := "sha256sum", args := #[path.toString] }
+  if output.exitCode != 0 then
+    throw <| IO.userError "sha256sum failed while hashing the target type"
+  let digest := (output.stdout.trimAscii.take 64).toString
+  if digest.length != 64 || !digest.all fun char => char.isDigit || ('a' ≤ char && char ≤ 'f') then
+    throw <| IO.userError "sha256sum emitted an invalid target type digest"
+  return digest
+
 private def observedAxioms (environment : Environment) (name : Name) : IO (Array Name) := do
   let context : Core.Context := {
     fileName := "<AutoLeanLibrarySubstrateIndependentQuery>"
@@ -218,18 +237,28 @@ private def query
   let some targetInfo := environment.checked.get.find? target
     | throw <| IO.userError "owned target has no ConstantInfo"
   let direct := uniqueSortedNames (← targetProof environment target).getUsedConstants
-  let candidateImports := candidate.imports.map (·.module)
+  if direct.any (· == forbiddenDirectDependency) then
+    throw <| IO.userError "Candidate directly depends on the forbidden Deriv.sound declaration"
+  let candidateImports := uniqueSortedNames (candidate.imports.map (·.module))
+  if candidateImports != #[`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude, `Init] then
+    throw <| IO.userError "Candidate direct imports differ from the independent substrate profile"
+  let renderedType ← canonicalType environment targetInfo
+  if (← sha256Text renderedType) != targetTypeSha256 then
+    throw <| IO.userError "Candidate target type differs from the historical frozen hash"
+  let axioms ← observedAxioms environment target
+  if axioms.map (·.toString) != expectedAxioms then
+    throw <| IO.userError "Candidate target axioms differ from the historical frozen set"
   return Json.mkObj [
-    ("candidate_direct_imports", namesJson (sortedNames candidateImports)),
+    ("candidate_direct_imports", namesJson candidateImports),
     ("candidate_ir_auxiliary_names", namesJson candidateAuxiliaryNames),
     ("candidate_kernel_names", namesJson candidateKernelNames),
     ("candidate_namespace_disjoint", Json.bool true),
     ("candidate_owns_target", Json.bool true),
-    ("canonical_type", Json.str (← canonicalType environment targetInfo)),
+    ("canonical_type", Json.str renderedType),
     ("declaration", Json.str target.toString),
     ("direct_proof_dependencies", namesJson direct),
     ("loaded_module_closure", namesJson (sortedNames environment.header.moduleNames)),
-    ("observed_axioms", namesJson (← observedAxioms environment target)),
+    ("observed_axioms", namesJson axioms),
     ("runtime_declarations", Json.arr (← runtimeInventory environment)),
     ("runtime_ir_auxiliary_names", Json.arr (← runtimeIrAuxiliaryNames environment)),
     ("schema_version", Json.str "autolean.library-substrate-independent-query.v1"),
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-v2-facade b/Prover/worker/library-substrate/autolean-library-substrate-v2-facade
new file mode 100644
index 0000000..5ed4041
--- /dev/null
+++ b/Prover/worker/library-substrate/autolean-library-substrate-v2-facade
@@ -0,0 +1,104 @@
+#!/bin/sh
+set -eu
+
+fail() {
+  printf '%s\n' "autolean-library-substrate-v2-facade: $1" >&2
+  exit 2
+}
+
+emit_phase_failure() {
+  failure_phase=$1
+  failure_stdout=$2
+  failure_stderr=$3
+  printf '%s\n' \
+    "autolean-library-substrate-v2-facade: phase=$failure_phase failed" >&2
+  {
+    cat "$failure_stdout"
+    cat "$failure_stderr"
+  } | head -c 4096 >&2
+  printf '\n' >&2
+}
+
+[ "$#" -ge 4 ] || fail "expected the frozen V2 wrapper argument profile"
+[ "$1" = "--protocol" ] || fail "missing protocol argument"
+[ "$2" = "autolean.oci-lean-wrapper.v2" ] || fail "unsupported protocol"
+[ "$3" = "--phase" ] || fail "missing phase argument"
+phase=$4
+
+root=/opt/autolean/library-substrate
+receipt_tool=$root/bin/autolean-library-substrate-build-receipt
+preflight_query=$root/bin/autolean-library-substrate-independent-query
+runtime=$root/lib/lean
+parent_lean_path=$(cat /opt/autolean/environment/lean-path)
+[ -n "$parent_lean_path" ] || fail "image-owned parent LEAN_PATH is unavailable"
+lean_path="$runtime:$parent_lean_path"
+
+# The receipt checker binds this facade and its V2 helper to the build input and runtime manifest
+# before either phase can accept a candidate artifact.
+"$receipt_tool" >/dev/null || fail "image-owned substrate receipt verification failed"
+
+wrapper_sha256=$(sha256sum /opt/autolean/bin/autolean-lean-wrapper | awk '{print $1}')
+query_helper_sha256=$(sha256sum /opt/autolean/lib/AutoleanLeanQuery.lean | awk '{print $1}')
+case "$wrapper_sha256:$query_helper_sha256" in
+  *[!0-9a-f:]*|*:|:*|*::* ) fail "image-owned verifier hashes are malformed" ;;
+esac
+
+scratch=$(mktemp -d /tmp/autolean-library-substrate-v2.XXXXXX)
+cleanup() {
+  rm -rf "$scratch"
+}
+trap cleanup EXIT HUP INT TERM
+
+case "$phase" in
+  compile)
+    [ "$#" -eq 8 ] || fail "expected the frozen V2 compile argument profile"
+    [ "$5" = "--candidate" ] || fail "missing candidate argument"
+    [ "$6" = "/input/Candidate.lean" ] || fail "candidate path is not frozen"
+    [ "$7" = "--output" ] || fail "missing output argument"
+    [ "$8" = "/output/Candidate.olean" ] || fail "compiled output path is not frozen"
+    test -f /input/Candidate.lean && test ! -L /input/Candidate.lean ||
+      fail "candidate source is unavailable"
+    test -d /output && test ! -L /output || fail "compiler output is unavailable"
+    if ! LEAN_PATH="$lean_path" lean -R /input -o /output/Candidate.olean \
+      /input/Candidate.lean >"$scratch/compiler.stdout" 2>"$scratch/compiler.stderr"
+    then
+      emit_phase_failure compile "$scratch/compiler.stdout" "$scratch/compiler.stderr"
+      exit 20
+    fi
+    ;;
+  query)
+    [ "$#" -eq 10 ] || fail "expected the frozen V2 query argument profile"
+    [ "$5" = "--compiled" ] || fail "missing compiled candidate argument"
+    [ "$6" = "/compiled/Candidate.olean" ] || fail "compiled candidate path is not frozen"
+    [ "$7" = "--declaration" ] || fail "missing declaration argument"
+    declaration=$8
+    [ "$9" = "--type-format" ] || fail "missing type-format argument"
+    [ "${10}" = "autolean.lean-pp-expr.v1" ] || fail "unsupported type format"
+    [ "$declaration" = "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.closed_sound" ] ||
+      fail "unsupported substrate target declaration"
+    test -f /compiled/Candidate.olean && test ! -L /compiled/Candidate.olean ||
+      fail "sealed Candidate.olean is unavailable"
+
+    # This preflight owns all substrate-specific semantics; stdout is intentionally discarded so
+    # the externally visible protocol remains the unchanged V2 single-record result.
+    if ! LEAN_PATH="/compiled:$lean_path" "$preflight_query" --phase query \
+      --target "$declaration" >"$scratch/preflight.stdout" 2>"$scratch/preflight.stderr"
+    then
+      emit_phase_failure query "$scratch/preflight.stdout" "$scratch/preflight.stderr"
+      exit 21
+    fi
+    if ! LEAN_PATH="/compiled:$lean_path" lean --run /opt/autolean/lib/AutoleanLeanQuery.lean \
+      "$declaration" "$wrapper_sha256" "$query_helper_sha256" \
+      >"$scratch/query.stdout" 2>"$scratch/query.stderr"
+    then
+      emit_phase_failure query "$scratch/query.stdout" "$scratch/query.stderr"
+      exit 22
+    fi
+    [ "$(wc -l <"$scratch/query.stdout" | tr -d ' ')" -eq 1 ] ||
+      fail "V2 query helper did not emit exactly one record"
+    cat "$scratch/query.stdout"
+    ;;
+  *)
+    fail "unsupported phase"
+    ;;
+esac
diff --git a/docs/README.md b/docs/README.md
index ab66f9d..099fd31 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -53,7 +53,8 @@ runner reports success.
     `library-substrate-v1` pilot profile from any future general Mathlib substrate, and defines
     independent versus compositional proof-dependency gates. The
     [image-owned substrate preflight](library-substrate-image-preflight.md) records the exact
-    child build, typed/IR inventory, sealed-Candidate query, and deliberately missing V2 adapter.
+    child build, typed/IR inventory, sealed-Candidate query, and V2-compatible preflight facade
+    without a contract, gateway, or T6 claim.
     The
     [executable proof-dependency spike](proof-dependency-gate-spike.md) records a host-mounted
     source-v2 replay and the remaining image, type, origin, contract, and gateway blockers.
diff --git a/docs/library-substrate-decision.md b/docs/library-substrate-decision.md
index f7f36b6..b1f1ed4 100644
--- a/docs/library-substrate-decision.md
+++ b/docs/library-substrate-decision.md
@@ -42,7 +42,7 @@ presented as the implementation or evidence for the focused Library profile.
 
 | Profile | Immediate purpose | Mathlib scope | Decision state |
 | --- | --- | --- | --- |
-| `library-substrate-v1` | Target-free AutoLean definitions for the first T5/T6 pilot | Reuse the locked `Mathlib.ModelTheory.Semantics` closure | Operator-local image preflight verified; not admitted or V2-integrated |
+| `library-substrate-v1` | Target-free AutoLean definitions for the first T5/T6 pilot | Reuse the locked `Mathlib.ModelTheory.Semantics` closure | Operator-local image preflight verified with a V2-compatible facade; not admitted, contract-bound, or gateway-integrated |
 | `mathlib-substrate-v1` | Possible general upstream Mathlib basis for later domains | Full default target or reviewed closures, as preflight determines | Deferred; no build choice accepted |
 | external `/deps` V3 | Dynamic accepted AutoLean theorem dependencies across project frontiers | Image-owned Mathlib plus a sealed external capsule | Deferred until the multi-file trigger below |
 
@@ -150,10 +150,11 @@ write only the proof slot, and the final image contains no target module to disc
 Registration must allowlist the new image only after its manifest and build receipt pass the
 release checks.
 
-The implemented preflight query intentionally uses a distinct command and schema. It neither
-occupies the V2 wrapper path nor emits V2 OCI evidence or a gateway receipt. See the
+The implemented direct facade occupies the V2 wrapper path and accepts the exact V2
+compile/query argv and stdout shape. It remains an image-local preflight only: it emits neither
+an OCI evidence record nor a gateway receipt. See the
 [image-owned substrate preflight](library-substrate-image-preflight.md) for the exact observed
-digest, receipt boundary, and remaining adapter gate.
+digest, receipt boundary, and remaining admission gates.
 
 ## Required rejection tests
 
diff --git a/docs/library-substrate-image-preflight.md b/docs/library-substrate-image-preflight.md
index 2a93911..1e67f9b 100644
--- a/docs/library-substrate-image-preflight.md
+++ b/docs/library-substrate-image-preflight.md
@@ -1,8 +1,8 @@
 # Library Substrate Image Preflight
 
-Status: operator-local image-owned preflight verified; not admitted and not V2-integrated
+Status: operator-local image-owned preflight with a V2-compatible facade; not admitted
 
-Observed date: 2026-07-25
+Observed date: 2026-07-26
 
 ## Result and authority boundary
 
@@ -12,13 +12,15 @@ independent-reproof canary:
 | Evidence | Observed value |
 | --- | --- |
 | Exact parent | `autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6` |
-| Docker-recorded child RepoDigest | `autolean/library-substrate@sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e` |
-| Child image ID | `sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e` |
-| Build-input SHA-256 | `858b1dafb9150e117eb0886fd53cf5d4707b5c42880e5374ebab7c9a94066883` |
-| Raw child receipt SHA-256 | `02f7fd99edbc29f817e2f87477fb6f4b69364b160a5659e5b2ccb8eab8e59fa9` |
-| Runtime-manifest SHA-256 | `923914c53d499eb21d405035ecc0df7ee145eda570bd476b799c7011ba287817` |
+| Docker-recorded child RepoDigest | `autolean/library-substrate@sha256:bc336196592536658395ff0867f3008fc256dc6a3fd9098f414e118f18d5d1ef` |
+| Child image ID | `sha256:bc336196592536658395ff0867f3008fc256dc6a3fd9098f414e118f18d5d1ef` |
+| Build-input SHA-256 | `2159b72cd598b4e1c6d9d8c3a33008f3f764d10c0343f8def794ddf43f570424` |
+| Raw child receipt SHA-256 | `f98010e0c4efb3a43a06bb7782507aa74e799e10822c0cecba890a858e8590df` |
+| Runtime-manifest SHA-256 | `007afe33d7268227c52ac42e7dee7e2880ccd97954005baf7e1b23cc114ebcc5` |
 | Runtime-source checksum-manifest SHA-256 | `e6638ec0117dcb0b700e695b760bb32c87bb7290b38ed98329d158e92e2ed2f3` |
-| Query-wrapper SHA-256 | `f1c09f0002af1b0729305534433286659e4af343c78a01b2d9873b368348d8d3` |
+| Query-wrapper SHA-256 | `c6c45a498bf3e21cbf76634fa9235a236d6cb176d34ff41223d74923dbf49882` |
+| V2 facade-wrapper SHA-256 | `a61d289bce7aec547e23826480435abbdee821c84810033a05babd2f086e0f49` |
+| V2 query-helper SHA-256 | `7b7595c6003981bd8d5c3136318f514ef4a1b72a3cbaf95a683a305938db3f3d` |
 | Runtime closure | 3 Library `.olean` files, 77 typed AutoLean declarations, 22 IR auxiliaries |
 
 The RepoDigest above came from Docker's `RepoDigests` inspection field. The runner refuses to
@@ -32,7 +34,7 @@ admitted into a frozen contract, or exercised through the OCI V2 evidence and si
 exact build context. It contains:
 
 - the child Dockerfile and one canonical build-input record;
-- four image-owned helper assets; and
+- six image-owned helper assets; and
 - exactly the `Core`, `SemanticPrelude`, and `RulePrelude` Library sources selected by the
   `independent_reproof` profile.
 
@@ -46,7 +48,8 @@ The three Library runtime module source files and their `.ilean` files are absen
 dedicated final tree. This is deliberately not a claim that every parent-image source or every
 piece of Lean text is absent from the whole child image. In particular, the independent query's
 Lean program is embedded in a here-document inside the hashed query wrapper and materialized
-only in a temporary, read-only-container run.
+only in a temporary, read-only-container run. The facade shell wrapper and its V2 query helper
+are separate image-owned build assets, hashed in the build input and child receipt.
 
 The source-v2 Dockerfile, receipt, and historical `UniversalLK.lean` inputs remain unchanged.
 The fresh context never includes the aggregate module, target modules, controls, Candidate
@@ -63,6 +66,10 @@ receipt. The host verifier retrieves the image-owned build input and source mani
 fixed Docker RepoDigest, then independently rereads the current three profile sources and
 recomputes all per-file hashes, sizes, manifest bytes, and the tree hash. A source change between
 input capture and context staging is therefore rejected instead of silently changing compilation.
+The same fixed-digest replay hashes the current Dockerfile and all six helper assets and requires
+the complete sorted map to equal the receipt-bound image build input. Replaying an older image
+after any current-checkout wrapper, helper, query, receipt, or build asset drift is therefore a
+failure rather than an image-self-consistency result attributed to the new checkout.
 
 `runtime-files.sha256` has a separate role: it is the exact three-line checksum manifest for the
 final `.olean` files. The image-owned receipt command validates it, parses the runtime manifest,
@@ -103,7 +110,7 @@ The image canary regenerates both inventories from the runtime `.olean` files an
 replay against the manifest.
 
 The content receipts above are replayable for the observed image. Two measured no-cache builds
-produced different image identities (`bb271a4362f4b3a7fc7e858f9d8349790cbdf8191a53085c95e3d9b1fa860903`
+produced different image identities (`7f517c627da00e1266493e17b48f15b09aad0839413bfdf1b4597c2a14e92f61`
 and the recorded final digest above), while their build input, both checksum manifests, runtime
 manifest, raw receipt, and all three `.olean` hashes matched. This is not a claim that two Docker
 builds are byte-identical or will always have the same content: Docker image/config metadata can
@@ -125,12 +132,32 @@ fresh container. The query proves that:
 - the proof expression does not directly use `Deriv.sound`; and
 - the query is bound to the runtime manifest, raw image receipt, query wrapper, and profile hash.
 
-The helper lives at
-`/opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query`. It does not
-occupy `/opt/autolean/bin/autolean-lean-wrapper`, does not implement
-`autolean.oci-lean-wrapper.v2`, and is not a drop-in `OciLeanRunner` adapter. It emits neither V2
-OCI evidence nor a gateway receipt. A separate integration change must adapt this verified
-runtime/query boundary to the existing V2 compile/query and evidence protocol.
+The rich independent-query helper lives at
+`/opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query`. It remains a
+rich internal diagnostic, not a public protocol. The same image now installs a narrow facade at
+`/opt/autolean/bin/autolean-lean-wrapper` that accepts the existing V2 compile/query argv and
+emits the unchanged single V2 record. Before emitting that record, its query phase runs the rich
+preflight and rejects anything outside this image-owned independent boundary: the Candidate must
+own the target, have the historical type hash and axiom set, avoid direct `Deriv.sound`, use the
+independent import boundary, and avoid all runtime kernel-plus-IR collisions. The image receipt
+and build input bind both the facade wrapper and V2 query-helper hashes; the host verifier accepts
+only the Docker-recorded child RepoDigest and rechecks those bindings against the runtime manifest.
+The facade canary treats rejection as a full compile-to-sealed-query property: each negative must
+fail in its frozen expected phase, with its exact source hash, return code, and reason marker. The
+compositional source hash
+`98cd1d2ae8f48ca368d19c64ddec447185bf13753a8d87dbf79df49bf33a7f78`
+fails compile with the absent `Targets/DerivSound.olean` marker; the direct target-import hash
+`c1725f40b0091501aaf465cefe318231af157b51ab3ffef9a8669bcb09ee4d4a`
+fails compile with the absent `Targets/ClosedSound.olean` marker. A third replacement-statement
+hash `f938b08d4e6d9de5e0288207f68ccc3122a5bd96dc08c885b71ba98a52919323`
+must compile successfully and then fail the sealed query with the rich canonical-type marker.
+Failure stdout is forbidden; a fixed phase prefix and at most 4,096 child diagnostic bytes are
+retained on facade stderr. Acceptance, a different phase, a different return code, source drift,
+or an unrelated failure is always a canary failure.
+
+This is V2-compatible preflight only. It does not alter a statement contract, the control plane,
+the signing gateway, or any public protocol. It emits no gateway receipt and does
+not establish T6, formal-asset admission, or provider execution.
 
 ## Operator commands
 
@@ -140,25 +167,25 @@ From the repository root:
 uv run --frozen python -m Library.scripts.library_substrate_image build
 uv run --frozen python -m Library.scripts.library_substrate_image verify --image <recorded-repodigest>
 uv run --frozen python -m Library.scripts.library_substrate_image canary --image <recorded-repodigest>
+uv run --frozen python -m Library.scripts.library_substrate_image facade-canary --image <recorded-repodigest>
 uv run --frozen python -m Library.scripts.library_substrate_image all
 ```
 
-Windows delegates the Docker work to WSL `Ubuntu-24.04`; Linux runs it natively. `verify` and
-`canary` require the exact Docker-recorded child RepoDigest.
+Windows delegates the Docker work to WSL `Ubuntu-24.04`; Linux runs it natively. `verify`,
+`canary`, and `facade-canary` require the exact Docker-recorded child RepoDigest.
 
 Focused negative tests cover context leakage, missing offline flags, fabricated child references,
 source-to-context TOCTOU, source checksum-manifest drift, synchronized runtime
 manifest/inventory/checksum forgery against unchanged actual `.olean` bytes, typed/IR inventory
 drift, invalid IR kind and origin, kernel/IR/target collisions, forbidden pilot theorems, exact
-target-type collision, and accidental V2-wrapper claims.
+target-type collision, host asset drift, facade receipt/manifest drift, complete V2 policy argv
+drift, and negative phase/reason/source drift.
 
 ## Non-claims and next gate
 
 This preflight does not implement a contract, the signing gateway, a provider run, an external
 dependency capsule, formal-asset admission, or T6. It is limited to `independent_reproof`;
-`compositional_bridge` and external `/deps` remain deferred.
+`compositional_bridge` is a required negative canary and external `/deps` remains deferred.
 
-The next Prover step is a narrow V2 adapter and adversarial integration suite that carries the
-verified child digest, runtime-manifest identity, task mode, type/origin inventory, Candidate
-ownership, and ordinary-dependency observation through OCI evidence and gateway replay. Builder
-admission and semantic review remain separate prerequisites.
+The next gate, if this preflight is retained, is a separately reviewed contract and gateway
+integration. Builder admission and semantic review remain separate prerequisites.
diff --git a/docs/phase-1-progress.md b/docs/phase-1-progress.md
index 948c695..138f582 100644
--- a/docs/phase-1-progress.md
+++ b/docs/phase-1-progress.md
@@ -67,7 +67,7 @@ These labels are deliberately non-interchangeable:
 | Imported-declaration module-origin API note | Design note, not replayable evidence | PR #19 documents Lean 4.28's imported-only lookup: an imported `ConstantInfo` may resolve through `getModuleIdxFor?`; a declaration in the current `Candidate` normally yields `none`, so Candidate ownership remains a separate sealed-`ModuleData` check | The early ad hoc probe was not retained and is not evidence. The note supplies no image-owned helper, module-origin observation, collision check, or admission result |
 | Dashboard | Verified, loopback | Projection/API tests, 15 UI tests, production build, controlled-browser desktop/mobile rendering, XSS/display sanitization, stable three-lane graph layout, and task/gap/verification drill-down | Remote mode remains unapproved; current JS bundle has a non-blocking 500 kB chunk warning |
 | Independent Library workspace | Verified, local diagnostic | Pinned Lean 4.28.0 and mathlib `8f9d9cff6bd728b17a24e163c9402775d9e6a365`; WSL/ext4 build of public root plus the three-node DAG fixture passed in 11.3 s | A local Lake build is not a Builder freeze, semantic review, OCI verification, or promotion |
-| Target-free Library substrate | Operator-local image preflight verified | The exact source-v2 child build completed offline with Docker-recorded RepoDigest `autolean/library-substrate@sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e`. Its dedicated runtime tree contains three target-free Library `.olean` files, a receipt-bound inventory of 77 typed declarations and 22 separately validated IR auxiliaries, and an image-owned sealed-Candidate query. The independent canary preserved the historical target type/axioms, rejected `Deriv.sound` as an ordinary dependency, replayed both inventories, and established Candidate/runtime kernel-plus-IR name disjointness. The fixed-digest verifier also recomputed each staged source and final `.olean` hash/size against the receipt-bound checksum manifests | Local preflight only: no registry publication, production signer, frozen contract/environment revision, formal-asset admission, provider run, V2 `OciLeanRunner` adapter/evidence, gateway receipt, or T6 result exists. The query's Lean source is embedded in its hashed wrapper; only the three Library runtime source files are absent from the dedicated final substrate tree. Receipt replay is not a claim that separate Docker builds have identical image metadata or RepoDigest |
+| Target-free Library substrate | Operator-local image preflight verified | The exact source-v2 child build completed offline at Docker RepoDigest `autolean/library-substrate@sha256:bc336196592536658395ff0867f3008fc256dc6a3fd9098f414e118f18d5d1ef`, with raw receipt SHA-256 `f98010e0c4efb3a43a06bb7782507aa74e799e10822c0cecba890a858e8590df`. Its dedicated runtime tree contains three target-free Library `.olean` files, a receipt-bound inventory of 77 typed declarations and 22 separately validated IR auxiliaries, an image-owned sealed-Candidate query, and a narrow facade accepting the existing V2 argv/result shape. The independent/facade canaries preserve the historical target type/axioms, reject direct `Deriv.sound`, replay both inventories, establish Candidate/runtime kernel-plus-IR name disjointness, and recompute staged-source and final-OLean hash/size facts against receipt-bound checksum manifests. Facade negatives bind source hash, exact phase, return code, and reason: the two forbidden target-module imports fail compilation, while a wrong-type replacement compiles and is rejected by the rich sealed query | Local V2-compatible preflight only: no registry publication, production signer, frozen contract/environment revision, formal-asset admission, provider run, V2 OCI evidence, gateway receipt, or T6 result exists. The facade does not change contracts, control plane, or gateway. The query's Lean source is embedded in its hashed wrapper; only the three Library runtime source files are absent from the dedicated final substrate tree. Receipt replay is not a claim that separate Docker builds have identical image metadata or RepoDigest |
 | Builder self-calibration and pilot selection | T3 gap, `not_selected`; review tooling merged | The pinned Library packet includes the kernel-checked `UniversalLK` micro-slice for the classical two-sided `⊥`, `→`, and `∀` fragment: level-indexed formulas, capture-avoiding instantiation, eigenvariable-safe universal rules, local/global soundness, the level-zero sentence bridge, and retained Bool rejection controls. The immutable public-safe V2 decision records the gap; a digest-only attachment covers all nine fine-anchor requirements with ten machine-located spans, and a separate exact-image attachment binds the source-v2 query artifact, all 46 declaration types/axiom sets, and the 2,744-module closure without changing that decision. PR #13 adds a byte-bound, versioned human-review packet and reproducible page-rendering workflow for the two ambiguous page pairs | No independent reviewer response has been accepted. Every fine span remains `machine_located_pending_review`; generating or visually opening the packet is not semantic review. The source-v2 observation still conflicts with the old decision's image/import/strict empty-axiom profile and requires an explicit successor profile plus authenticated admission authority. The fragment has no existential constructors or sequent-level structural rules; it is not frozen or handed to Prover |
 | Model-theory source egress | Enforced, source-specific `local_only` | The current reference manifest, source-rule matrix, and human-review packet all bind `model_egress_policy=local_only` | Exact textbook bytes or rendered pages may not be sent to an external provider or model-backed subagent. This is the current source record's rights/egress decision, not a missing Provider or Harness capability; changing it requires a reviewed manifest/rights revision |
 | Builder reference cache | Verified offline | Five locked source/derived records. The manifest-v2 fifth record is the 437-page `pypdf 6.14.2` extraction of Open Logic Project *Sets, Logic, Computation*, text SHA `6184495568a4487848e747f25385cb4081be1cd87f77488c9de0046d600cfa6d`; manifest SHA `b947a08ef2455beb77d9481c4cbddc481ec6590f03746fd22affb03dd8b06f91` | Retained only as local reference/provenance material; no human-calibrated pilot statement is recorded and model egress remains forbidden |
@@ -112,7 +112,7 @@ permits an RC.
 | Pilot self-calibration | T3 gap, blocked | V2 records `gap/not_selected` and remains unchanged. Complete local review of the ten machine-located spans, resolve the Section 7.5 and universal-right (`∀R`) locator ambiguity, decide a successor formal profile consistent with the exact image/import/axiom observation, and close semantic-review and admission-authority checks. The two audited backups are not selected, so a different backup requires its own audit |
 | Pinned Library selection spike | Partial passed with gap | The universal fragment is kernel-checked, but local replay does not select it or establish source fidelity |
 | First calibrated contract slice (T5) | Blocked by T3 | A different backup may be audited, but no statement may freeze until one boundary is admitted with rights and review readiness |
-| Target-free substrate and dependency gate (T6) | Image-owned preflight verified; blocked by T5 and integration | The focused child image now binds its parent/build/runtime receipts, complete typed and IR-owned declaration inventories, imported origins, collision checks, sealed Candidate ownership, and independent ordinary-dependency observation. T6 still needs an admitted immutable contract/environment revision, the V2 `OciLeanRunner` adapter and evidence, signing-gateway replay, adversarial integration rejections, and an accepted frozen-to-verified result |
+| Target-free substrate and dependency gate (T6) | Image-owned preflight verified; blocked by T5 and integration | The focused child image now binds its parent/build/runtime receipts, complete typed and IR-owned declaration inventories, imported origins, collision checks, sealed Candidate ownership, and independent ordinary-dependency observation. Its direct V2-compatible facade is preflight evidence only. T6 still needs an admitted immutable contract/environment revision, signing-gateway replay, adversarial integration rejections, and an accepted frozen-to-verified result |
 | Real project-scale loop (T7) | Input preflight only | The synthetic scheduling fixture and real Lean content fixture are both retained, but acceptance still needs changed-source rebuild, lease/bundle flow, clean integration, and per-node verification evidence |
 | Authoritative Prover path | Partially verified | One unchanged source-backed synthetic bundle passed the full local pure-Lean path through real OCI, an independent gateway rerun, and terminal acceptance. Preserve that contract while extending the same path to the exact mathlib profile and closing production-authority and full adversarial-suite gaps |
 | Controlled model/benchmark evaluation | Blocked before egress | External execution authorization and production evaluators must exist before requesting an API secret. Once ready, fixed suites and ablations remain secondary diagnostics; no FATE result closes a Builder or Library gate |
diff --git a/scripts/tests/test_library_substrate_image.py b/scripts/tests/test_library_substrate_image.py
index 0fc1701..5a104ac 100644
--- a/scripts/tests/test_library_substrate_image.py
+++ b/scripts/tests/test_library_substrate_image.py
@@ -1,10 +1,12 @@
 from __future__ import annotations
 
 import copy
+import subprocess
 from pathlib import Path
 from typing import cast
 
 import pytest
+from autolean_contracts import OciVerifierExecutionPolicyV2
 
 from Library.scripts import library_substrate_image as substrate
 from Library.scripts.verify_substrate_fixture import (
@@ -135,9 +137,10 @@ def test_stage_build_context_contains_only_runtime_sources(
     prepared, arguments = substrate.stage_build_context(tmp_path / "context")
 
     inventory = cast(dict[str, str], prepared["context_inventory"])
-    assert len(inventory) == 10
+    assert len(inventory) == 12
     assert set(path for path in inventory if path.endswith(".lean")) == {
         "helpers/AutoleanLibrarySubstrateInventory.lean",
+        "helpers/AutoleanLibrarySubstrateV2Query.lean",
         *(f"source/{cast(str, source['path'])}" for source in sources),
     }
     assert not any(
@@ -372,3 +375,235 @@ def test_query_wrapper_does_not_claim_v2_gateway_compatibility() -> None:
     assert "autolean.oci-lean-wrapper.v2" not in wrapper
     assert "runtime_manifest_sha256" in wrapper
     assert "image_receipt_sha256" in wrapper
+
+
+def test_v2_facade_bindings_reject_receipt_and_manifest_drift() -> None:
+    wrapper_sha256 = "a" * 64
+    helper_sha256 = "b" * 64
+    manifest_file_sha256 = "c" * 64
+    build_input: dict[str, object] = {
+        "assets": {
+            "V2_FACADE_QUERY_HELPER_SHA256": helper_sha256,
+            "V2_FACADE_WRAPPER_SHA256": wrapper_sha256,
+        },
+        "target": {
+            "canonical_type_sha256": substrate.TARGET_TYPE_SHA256,
+            "declaration": TARGET_DECLARATION,
+            "forbidden_ordinary_dependency": SOUND_DECLARATION,
+        },
+    }
+    receipt: dict[str, object] = {
+        "runtime_manifest_sha256": manifest_file_sha256,
+        "v2_facade_query_helper_sha256": helper_sha256,
+        "v2_facade_wrapper_sha256": wrapper_sha256,
+    }
+
+    substrate._validate_v2_facade_bindings(
+        receipt,
+        build_input,
+        runtime_manifest_file_sha256=manifest_file_sha256,
+        facade_wrapper_sha256=wrapper_sha256,
+        facade_query_helper_sha256=helper_sha256,
+    )
+
+    receipt_drift = copy.deepcopy(receipt)
+    receipt_drift["v2_facade_wrapper_sha256"] = "c" * 64
+    with pytest.raises(substrate.SubstrateImageError, match="v2_facade_wrapper_sha256"):
+        substrate._validate_v2_facade_bindings(
+            receipt_drift,
+            build_input,
+            runtime_manifest_file_sha256=manifest_file_sha256,
+            facade_wrapper_sha256=wrapper_sha256,
+            facade_query_helper_sha256=helper_sha256,
+        )
+
+    with pytest.raises(substrate.SubstrateImageError, match="runtime manifest"):
+        substrate._validate_v2_facade_bindings(
+            receipt,
+            build_input,
+            runtime_manifest_file_sha256="d" * 64,
+            facade_wrapper_sha256=wrapper_sha256,
+            facade_query_helper_sha256=helper_sha256,
+        )
+
+
+def test_host_asset_binding_rejects_checkout_drift(
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    assets = {
+        "DOCKERFILE_SHA256": "a" * 64,
+        "V2_FACADE_QUERY_HELPER_SHA256": "b" * 64,
+        "V2_FACADE_WRAPPER_SHA256": "c" * 64,
+    }
+    monkeypatch.setattr(substrate, "_asset_hashes", lambda: assets)
+
+    substrate._validate_host_asset_binding({"assets": dict(sorted(assets.items()))})
+
+    drifted = dict(assets)
+    drifted["V2_FACADE_WRAPPER_SHA256"] = "d" * 64
+    with pytest.raises(substrate.SubstrateImageError, match="current host helper assets"):
+        substrate._validate_host_asset_binding({"assets": drifted})
+
+
+def test_v2_facade_keeps_the_existing_runner_protocol_and_runs_preflight() -> None:
+    facade = (substrate.HELPER_ROOT / "autolean-library-substrate-v2-facade").read_text(
+        encoding="utf-8"
+    )
+    independent_query = (
+        substrate.HELPER_ROOT / "autolean-library-substrate-independent-query"
+    ).read_text(encoding="utf-8")
+
+    assert '"--protocol"' in facade
+    assert '"autolean.oci-lean-wrapper.v2"' in facade
+    assert '"--candidate"' in facade
+    assert '"--compiled"' in facade
+    assert '"--type-format"' in facade
+    assert '"autolean.lean-pp-expr.v1"' in facade
+    assert '"$preflight_query" --phase query' in facade
+    assert "phase=$failure_phase failed" in facade
+    assert "head -c 4096" in facade
+    assert "targetTypeSha256" in independent_query
+    assert "forbidden Deriv.sound declaration" in independent_query
+    assert (
+        "Candidate direct imports differ from the independent substrate profile"
+        in independent_query
+    )
+
+
+def test_v2_facade_argv_matches_the_complete_v2_policy() -> None:
+    policy = OciVerifierExecutionPolicyV2(worker_image_digest="sha256:" + "a" * 64)
+
+    assert substrate._v2_compile_wrapper_argv() == policy.compile_wrapper_argv()
+    assert substrate._v2_query_wrapper_argv() == policy.wrapper_argv(TARGET_DECLARATION)
+
+
+def test_v2_negative_candidate_sources_have_frozen_hashes() -> None:
+    compositional = (
+        FIXTURE_ROOT / "candidates" / "compositional_bridge" / "Candidate.lean"
+    ).read_bytes()
+
+    assert substrate._sha256_bytes(compositional) == substrate.V2_COMPOSITIONAL_CANDIDATE_SHA256
+    assert (
+        substrate._sha256_bytes(substrate.V2_TARGET_IMPORT_SOURCE.encode("utf-8"))
+        == substrate.V2_TARGET_IMPORT_SOURCE_SHA256
+    )
+    assert (
+        substrate._sha256_bytes(substrate.V2_WRONG_TARGET_TYPE_SOURCE.encode("utf-8"))
+        == substrate.V2_WRONG_TARGET_TYPE_SOURCE_SHA256
+    )
+
+
+def test_v2_rejection_observation_requires_exact_phase_reason_rc_and_source() -> None:
+    prefix = "autolean-library-substrate-v2-facade: phase=query failed"
+    marker = "Candidate target type differs from the historical frozen hash"
+    result = subprocess.CompletedProcess(
+        args=("docker", "run"),
+        returncode=21,
+        stdout="",
+        stderr=f"{prefix}\nautolean-library-substrate-independent-query: {marker}\n",
+    )
+    expected_hash = "a" * 64
+
+    observation = substrate._v2_rejection_observation(
+        result,
+        label="wrong-target-type",
+        actual_phase="query",
+        expected_phase="query",
+        expected_returncode=21,
+        reason_marker=marker,
+        candidate_source_sha256=expected_hash,
+        expected_candidate_source_sha256=expected_hash,
+    )
+
+    assert observation == {
+        "candidate_source_sha256": expected_hash,
+        "reason_marker": marker,
+        "rejection_phase": "query",
+        "returncode": 21,
+        "stderr_summary": result.stderr.strip(),
+    }
+
+    with pytest.raises(substrate.SubstrateImageError, match="expected query"):
+        substrate._v2_rejection_observation(
+            result,
+            label="wrong-target-type",
+            actual_phase="compile",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker=marker,
+            candidate_source_sha256=expected_hash,
+            expected_candidate_source_sha256=expected_hash,
+        )
+    with pytest.raises(substrate.SubstrateImageError, match="returned 21, expected 20"):
+        substrate._v2_rejection_observation(
+            result,
+            label="wrong-target-type",
+            actual_phase="query",
+            expected_phase="query",
+            expected_returncode=20,
+            reason_marker=marker,
+            candidate_source_sha256=expected_hash,
+            expected_candidate_source_sha256=expected_hash,
+        )
+    with pytest.raises(substrate.SubstrateImageError, match="source hash drifted"):
+        substrate._v2_rejection_observation(
+            result,
+            label="wrong-target-type",
+            actual_phase="query",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker=marker,
+            candidate_source_sha256="b" * 64,
+            expected_candidate_source_sha256=expected_hash,
+        )
+    missing_reason = subprocess.CompletedProcess(
+        args=result.args,
+        returncode=21,
+        stdout="",
+        stderr=f"{prefix}\nunrelated failure\n",
+    )
+    with pytest.raises(substrate.SubstrateImageError, match="reason is unavailable"):
+        substrate._v2_rejection_observation(
+            missing_reason,
+            label="wrong-target-type",
+            actual_phase="query",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker=marker,
+            candidate_source_sha256=expected_hash,
+            expected_candidate_source_sha256=expected_hash,
+        )
+    stdout_failure = subprocess.CompletedProcess(
+        args=result.args,
+        returncode=21,
+        stdout="unexpected output\n",
+        stderr=result.stderr,
+    )
+    with pytest.raises(substrate.SubstrateImageError, match="failure emitted stdout"):
+        substrate._v2_rejection_observation(
+            stdout_failure,
+            label="wrong-target-type",
+            actual_phase="query",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker=marker,
+            candidate_source_sha256=expected_hash,
+            expected_candidate_source_sha256=expected_hash,
+        )
+    unbounded_failure = subprocess.CompletedProcess(
+        args=result.args,
+        returncode=21,
+        stdout="",
+        stderr=f"{prefix}\n{marker}\n{'x' * 5000}",
+    )
+    with pytest.raises(substrate.SubstrateImageError, match="reason is unavailable or unbounded"):
+        substrate._v2_rejection_observation(
+            unbounded_failure,
+            label="wrong-target-type",
+            actual_phase="query",
+            expected_phase="query",
+            expected_returncode=21,
+            reason_marker=marker,
+            candidate_source_sha256=expected_hash,
+            expected_candidate_source_sha256=expected_hash,
+        )