diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e36cc2c037..ab4f203ff6 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -728,6 +728,8 @@ jobs:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           persist-credentials: false
+      - name: Test Kani cover-result checker
+        run: python3 ci/check_kani_cover_test.py
       - uses: model-checking/kani-github-action@f838096619a707b0f6b2118cf435eaccfa33e51f # v1.1
         with:
           command: zerocopy/ci/run_kani.sh
@@ -743,8 +745,10 @@ jobs:
           # specifying a particular toolchain.
           # Memory-safety, overflow, undefined-function, and unwinding checks
           # are enabled by default. Kani 0.65 removed their positive flags.
-          # The custom command enters the `zerocopy` crate directory before
-          # forwarding these arguments.
+          # Kani 0.67 does not make an unsatisfied `kani::cover!` fail the
+          # invocation. The custom runner enters the `zerocopy` crate, keeps
+          # the combined output for diagnostics, and independently validates
+          # the complete per-harness result inventory from one fresh target.
           args: "--manifest-path Cargo.toml --package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse -Zfunction-contracts --randomize-layout"
           # This version is automatically rolled by
           # `roll-pinned-toolchain-versions.yml`.
diff --git a/ci/check_kani_cover.py b/ci/check_kani_cover.py
new file mode 100644
index 0000000000..77d7b07a41
--- /dev/null
+++ b/ci/check_kani_cover.py
@@ -0,0 +1,789 @@
+#!/usr/bin/env python3
+# Copyright 2026 The Fuchsia Authors
+#
+# Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+# <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+# license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+# This file may not be copied, modified, or distributed except according to
+# those terms.
+"""Require every Kani 0.67 cover property to be satisfied.
+
+Kani 0.67 deliberately excludes `kani::cover!` properties from its overall
+verification status. Its exact property parser, renderer, per-harness writer,
+and metadata schema are pinned here:
+
+https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/cbmc_output_parser.rs
+https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/cbmc_property_renderer.rs
+https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/call_cbmc.rs
+https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/harness_runner.rs
+https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani_metadata/src/lib.rs
+
+This checker consumes one fresh, private `--target-dir` produced by a single,
+unfiltered Kani invocation with `-Zunstable-options --output-into-files`. Kani
+metadata describes the harnesses discovered in the crate, so result/metadata
+inventory equality is intentionally also a no-filter protocol check. Each
+filesystem component below the target must be an actual directory or regular
+file, never a symlink.
+
+The protocol requires Kani 0.67's exact six-field metadata root, `zerocopy` as
+both root and proof-harness crate identity, at least one proof harness, no test
+harnesses, and no autoharness metadata. It validates the types of root fields
+which are not otherwise consumed, and decodes only the inventory-bearing
+`pretty_name`, nested crate identity, and `should_panic` harness fields.
+
+The result parser accepts only the Kani 0.67 regular renderer's ordered record
+framing, exact audited zerocopy property-class vocabulary, and unique property
+identifiers per harness. The renderer does not escape descriptions, so this
+parser supports the multiline descriptions present in the audited zerocopy
+corpus but rejects control-record text inside a multiline description. This
+conservative subset avoids treating an injected record as verification
+evidence. Source-location fields remain opaque because Kani accepts arbitrary
+optional strings for each component; their framing and control-free envelope,
+not their internal meaning, are validated. The informational verification time
+is restricted to necessary Duration/binary32 bounds rather than claimed to be
+an exact inverse of Rust's shortest-decimal formatter.
+"""
+
+import json
+import os
+import re
+import stat
+import sys
+from decimal import Decimal
+from pathlib import Path, PurePosixPath
+
+U32_MAX = (1 << 32) - 1
+U64_MAX = (1 << 64) - 1
+UINT_RE = re.compile(r"0|[1-9][0-9]*")
+PROPERTY_CLASS_RE = re.compile(r"NaN|[a-z_-]+")
+# This is the exact class vocabulary observed in the authentic, unfiltered
+# zerocopy Kani 0.67 corpus audited with this parser. A source or tool change
+# which emits another class must update this pinned protocol deliberately.
+# Known source variants such as `NaN`, `finite_check`, and `recursion` remain
+# excluded because the audited corpus did not emit them; accepting a newly
+# observed variant requires re-auditing the complete corpus rather than guessing.
+AUDITED_PROPERTY_CLASSES = frozenset(
+    {
+        "arithmetic_overflow",
+        "array_bounds",
+        "assertion",
+        "assigns",
+        "assume",
+        "bit_count",
+        "cover",
+        "division-by-zero",
+        "exact_div",
+        "frees",
+        "missing_definition",
+        "no_alloc_dealloc_in_ensures",
+        "no_alloc_dealloc_in_requires",
+        "no_recursive_call",
+        "pointer",
+        "pointer_dereference",
+        "precondition",
+        "precondition_instance",
+        "safety_check",
+        "single_top_level_call",
+        "unreachable",
+        "unsupported_construct",
+        "unwind",
+    }
+)
+METADATA_ROOT_FIELDS = frozenset(
+    {
+        "crate_name",
+        "proof_harnesses",
+        "unsupported_features",
+        "test_harnesses",
+        "contracted_functions",
+        "autoharness_md",
+    }
+)
+EXPECTED_CRATE_NAME = "zerocopy"
+CHECK_RE = re.compile(r"Check ([1-9][0-9]*): (.+)")
+THREAD_RE = re.compile(r"Thread (0|[1-9][0-9]*):")
+STATUS_RE = re.compile(r"\t - Status: ([A-Z]+)")
+# Kani's `SourceLocation` fields are arbitrary optional strings. In particular,
+# any nonempty payload can be the `file` field by itself, so the renderer does
+# not provide a tighter grammar that this parser could authenticate. This
+# expression validates only the record's nonempty, single-line envelope; the
+# raw-input control-character check below supplies the other useful bound.
+LOCATION_ENVELOPE_RE = re.compile(r"\t - Location: (.+)")
+FAILURE_LOCATION_RE = re.compile(r' File: "(.*)", line (0|[1-9][0-9]*), in (.*)')
+# `Duration::as_secs_f32()` is rendered with Rust's ordinary `Display`, not
+# exponential formatting. `Display` omits redundant leading/trailing zeroes.
+# Decimal syntax plus `_validate_verification_time` enforces necessary bounds
+# on this informational field; it intentionally does not claim to recognize
+# the exact image of Rust's binary32 shortest-decimal formatter.
+TIME_RE = re.compile(
+    r"Verification Time: ((?:0|[1-9][0-9]*)(?:\.[0-9]*[1-9])?)s"
+)
+MIN_POSITIVE_DURATION_SECONDS = Decimal(1) / Decimal(1_000_000_000)
+# `Duration::MAX.as_secs_f32()` rounds to binary32 2^64, rather than to the
+# exact integer `u64::MAX` seconds stored by `Duration`.
+MAX_RENDERED_DURATION_SECONDS = Decimal(1 << 64)
+DESCRIPTION_PREFIX = '\t - Description: "'
+NONCOVER_STATUSES = {
+    "FAILURE",
+    "SUCCESS",
+    "UNDETERMINED",
+    "UNREACHABLE",
+}
+COVER_STATUSES = {"SATISFIED", "UNDETERMINED", "UNREACHABLE", "UNSATISFIABLE"}
+KNOWN_STATUSES = NONCOVER_STATUSES | COVER_STATUSES
+MULTILINE_DESCRIPTION_CONTROL_PREFIXES = (
+    "Check ",
+    "\t - Status:",
+    "\t - Description:",
+    "\t - Location:",
+    "SUMMARY:",
+    " ** ",
+    "Failed Checks:",
+    " File:",
+    "VERIFICATION:-",
+    "Verification Time:",
+    "Thread ",
+)
+
+
+class ValidationError(Exception):
+    """A fail-closed Kani output validation error."""
+
+
+def _contains_control_characters(value):
+    return any(
+        ord(character) < 0x20 or 0x7F <= ord(character) <= 0x9F
+        for character in value
+    )
+
+
+def _read_lines(path):
+    try:
+        text = path.read_bytes().decode("utf-8")
+    except (OSError, UnicodeError) as error:
+        raise ValidationError(f"cannot read {path}: {error}") from error
+    if not text:
+        raise ValidationError(f"empty result file: {path}")
+    # Tabs and line feeds are structural parts of Kani's regular renderer, but
+    # C1 controls are no more valid in its textual records than C0 controls.
+    if any(
+        (ord(character) < 0x20 and character not in "\t\n")
+        or 0x7F <= ord(character) <= 0x9F
+        for character in text
+    ):
+        raise ValidationError(f"{path}: result contains a non-Kani control character")
+    if not text.endswith("\n"):
+        raise ValidationError(f"result file lacks Kani's final newline: {path}")
+    lines = text.split("\n")
+    lines.pop()
+    return lines
+
+
+def _canonical_uint(token, maximum, description, path, line_number=None):
+    where = str(path)
+    if line_number is not None:
+        where += f":{line_number}"
+    if UINT_RE.fullmatch(token) is None:
+        raise ValidationError(f"{where}: noncanonical {description} {token!r}")
+    value = int(token)
+    if value > maximum:
+        raise ValidationError(f"{where}: {description} exceeds {maximum}: {token}")
+    return value
+
+
+def _validate_verification_time(token, path, line_number):
+    """Validate necessary numeric bounds on Kani's informational runtime."""
+
+    value = Decimal(token)
+    if value != 0 and value < MIN_POSITIVE_DURATION_SECONDS:
+        raise ValidationError(
+            f"{path}:{line_number}: verification time is below Duration's "
+            f"one-nanosecond resolution: {token}"
+        )
+    if value > MAX_RENDERED_DURATION_SECONDS:
+        raise ValidationError(
+            f"{path}:{line_number}: verification time exceeds Kani's rendered "
+            f"Duration range: {token}"
+        )
+
+    # A finite binary32 has at most nine significant decimal digits in its
+    # shortest round-tripping representation. Positional zeroes do not count:
+    # for example, both 0.000000001 and 18446744000000000000 remain admissible.
+    significant_digits = token.replace(".", "").lstrip("0").rstrip("0")
+    if len(significant_digits) > 9:
+        raise ValidationError(
+            f"{path}:{line_number}: verification time exceeds binary32's "
+            f"shortest-decimal precision envelope: {token}"
+        )
+
+
+def _property_class(property_name, path, line_number):
+    if property_name != property_name.strip() or _contains_control_characters(
+        property_name
+    ):
+        raise ValidationError(
+            f"{path}:{line_number}: noncanonical whitespace/control in Kani property name"
+        )
+    attributes = property_name.rsplit(".", 2)
+    if len(attributes) == 2:
+        property_class, property_id = attributes
+    elif len(attributes) == 3:
+        function, property_class, property_id = attributes
+        if not function:
+            raise ValidationError(
+                f"{path}:{line_number}: empty function in Kani property name"
+            )
+    else:
+        raise ValidationError(
+            f"{path}:{line_number}: malformed Kani property name {property_name!r}"
+        )
+    if PROPERTY_CLASS_RE.fullmatch(property_class) is None:
+        raise ValidationError(
+            f"{path}:{line_number}: malformed Kani property class {property_class!r}"
+        )
+    if property_class not in AUDITED_PROPERTY_CLASSES:
+        raise ValidationError(
+            f"{path}:{line_number}: Kani 0.67 property class {property_class!r} "
+            "is outside the audited zerocopy vocabulary; re-audit before allowing it"
+        )
+    _canonical_uint(property_id, U32_MAX, "Kani property id", path, line_number)
+    return property_class
+
+
+def _need_line(lines, cursor, expected, path, description):
+    if cursor >= len(lines) or lines[cursor] != expected:
+        actual = "end of file" if cursor >= len(lines) else repr(lines[cursor])
+        raise ValidationError(
+            f"{path}:{cursor + 1}: expected {description} {expected!r}; found {actual}"
+        )
+    return cursor + 1
+
+
+def _parse_description(lines, cursor, path, ordinal):
+    if cursor >= len(lines) or not lines[cursor].startswith(DESCRIPTION_PREFIX):
+        actual = "end of file" if cursor >= len(lines) else repr(lines[cursor])
+        raise ValidationError(
+            f"{path}:{cursor + 1}: expected description for check {ordinal}; found {actual}"
+        )
+
+    first = lines[cursor][len(DESCRIPTION_PREFIX) :]
+    cursor += 1
+    if first.endswith('"'):
+        return first[:-1], cursor
+    if '"' in first:
+        raise ValidationError(
+            f"{path}:{cursor}: ambiguous quote in multiline description for check {ordinal}"
+        )
+
+    description_lines = [first]
+    while cursor < len(lines):
+        line = lines[cursor]
+        if line.startswith(MULTILINE_DESCRIPTION_CONTROL_PREFIXES):
+            raise ValidationError(
+                f"{path}:{cursor + 1}: control record in unterminated description "
+                f"for check {ordinal}"
+            )
+        cursor += 1
+        if line.endswith('"'):
+            if '"' in line[:-1]:
+                raise ValidationError(
+                    f"{path}:{cursor}: ambiguous quote in multiline description "
+                    f"for check {ordinal}"
+                )
+            description_lines.append(line[:-1])
+            return "\n".join(description_lines), cursor
+        if '"' in line:
+            raise ValidationError(
+                f"{path}:{cursor}: ambiguous quote in multiline description for check {ordinal}"
+            )
+        description_lines.append(line)
+
+    raise ValidationError(f"{path}: unterminated description for check {ordinal}")
+
+
+def _parse_check(lines, cursor, ordinal, path):
+    line_number = cursor + 1
+    match = CHECK_RE.fullmatch(lines[cursor])
+    if match is None:
+        raise ValidationError(f"{path}:{line_number}: malformed Kani check header")
+    rendered_ordinal = _canonical_uint(
+        match.group(1), sys.maxsize, "Kani check number", path, line_number
+    )
+    if rendered_ordinal != ordinal:
+        raise ValidationError(
+            f"{path}:{line_number}: noncontiguous check number {rendered_ordinal}; "
+            f"expected {ordinal}"
+        )
+    property_name = match.group(2)
+    property_class = _property_class(property_name, path, line_number)
+    cursor += 1
+
+    if cursor >= len(lines):
+        raise ValidationError(f"{path}: missing status for check {ordinal}")
+    status_match = STATUS_RE.fullmatch(lines[cursor])
+    if status_match is None:
+        raise ValidationError(
+            f"{path}:{cursor + 1}: malformed status for check {ordinal}"
+        )
+    status_value = status_match.group(1)
+    if status_value not in KNOWN_STATUSES:
+        raise ValidationError(
+            f"{path}:{cursor + 1}: unknown Kani status {status_value!r}"
+        )
+    cursor += 1
+
+    description, cursor = _parse_description(lines, cursor, path, ordinal)
+    if cursor < len(lines) and lines[cursor].startswith("\t - Location:"):
+        if LOCATION_ENVELOPE_RE.fullmatch(lines[cursor]) is None:
+            raise ValidationError(
+                f"{path}:{cursor + 1}: malformed location for check {ordinal}"
+            )
+        cursor += 1
+    cursor = _need_line(
+        lines, cursor, "", path, f"record terminator for check {ordinal}"
+    )
+
+    is_cover = property_class == "cover"
+    allowed_statuses = COVER_STATUSES if is_cover else NONCOVER_STATUSES
+    if status_value not in allowed_statuses:
+        kind = "cover" if is_cover else "non-cover"
+        raise ValidationError(
+            f"{path}:{line_number}: {kind} property has impossible Kani 0.67 "
+            f"status {status_value!r}"
+        )
+    return {
+        "name": property_name,
+        "class": property_class,
+        "status": status_value,
+        "description": description,
+    }, cursor
+
+
+def _expected_breakdown(statuses):
+    breakdown = []
+    for status_value, label in (
+        ("UNDETERMINED", "undetermined"),
+        ("UNREACHABLE", "unreachable"),
+    ):
+        count = statuses.count(status_value)
+        if count:
+            breakdown.append(f"{count} {label}")
+    return ",".join(breakdown)
+
+
+def _expected_summary(kind, statuses):
+    if kind == "normal":
+        summary = f" ** {statuses.count('FAILURE')} of {len(statuses)} failed"
+    else:
+        summary = (
+            f" ** {statuses.count('SATISFIED')} of {len(statuses)} "
+            "cover properties satisfied"
+        )
+    breakdown = _expected_breakdown(statuses)
+    if breakdown:
+        summary += f" ({breakdown})"
+    return summary
+
+
+def _parse_failure_details(lines, cursor, failed_checks, path):
+    for check in failed_checks:
+        description_lines = check["description"].split("\n")
+        cursor = _need_line(
+            lines,
+            cursor,
+            "Failed Checks: " + description_lines[0],
+            path,
+            f"failure detail for {check['name']!r}",
+        )
+        for description_line in description_lines[1:]:
+            cursor = _need_line(
+                lines,
+                cursor,
+                description_line,
+                path,
+                f"multiline failure detail for {check['name']!r}",
+            )
+        if cursor < len(lines) and lines[cursor].startswith(" File:"):
+            location_match = FAILURE_LOCATION_RE.fullmatch(lines[cursor])
+            if location_match is None:
+                raise ValidationError(
+                    f"{path}:{cursor + 1}: malformed failed-check location"
+                )
+            _canonical_uint(
+                location_match.group(2),
+                U64_MAX,
+                "failed-check line number",
+                path,
+                cursor + 1,
+            )
+            cursor += 1
+    return cursor
+
+
+def _parse_result(path, should_panic):
+    lines = _read_lines(path)
+    cursor = 0
+    if cursor < len(lines) and lines[cursor].startswith("Thread "):
+        thread_match = THREAD_RE.fullmatch(lines[cursor])
+        if thread_match is None:
+            raise ValidationError(f"{path}:1: malformed Kani thread header")
+        _canonical_uint(
+            thread_match.group(1), sys.maxsize, "Kani thread index", path, 1
+        )
+        cursor += 1
+    cursor = _need_line(lines, cursor, "", path, "blank line before RESULTS")
+    cursor = _need_line(lines, cursor, "RESULTS:", path, "Kani RESULTS header")
+
+    checks = []
+    property_names = set()
+    while cursor < len(lines):
+        if lines[cursor].startswith("Check "):
+            check, cursor = _parse_check(lines, cursor, len(checks) + 1, path)
+            if check["name"] in property_names:
+                raise ValidationError(
+                    f"{path}: duplicate Kani property name {check['name']!r}"
+                )
+            property_names.add(check["name"])
+            checks.append(check)
+            continue
+        if (
+            lines[cursor] == ""
+            and cursor + 1 < len(lines)
+            and lines[cursor + 1] == "SUMMARY:"
+        ):
+            cursor += 2
+            break
+        raise ValidationError(
+            f"{path}:{cursor + 1}: unexpected record in Kani RESULTS section: "
+            f"{lines[cursor]!r}"
+        )
+    else:
+        raise ValidationError(f"{path}: missing Kani SUMMARY header")
+
+    cover_checks = [check for check in checks if check["class"] == "cover"]
+    noncover_checks = [check for check in checks if check["class"] != "cover"]
+    cover_statuses = [check["status"] for check in cover_checks]
+    noncover_statuses = [check["status"] for check in noncover_checks]
+
+    expected_main = _expected_summary("normal", noncover_statuses)
+    cursor = _need_line(
+        lines, cursor, expected_main, path, "canonical normal-property summary"
+    )
+    if cover_checks:
+        cursor = _need_line(lines, cursor, "", path, "blank line before cover summary")
+        expected_cover = _expected_summary("cover", cover_statuses)
+        cursor = _need_line(
+            lines, cursor, expected_cover, path, "canonical cover-property summary"
+        )
+        cursor = _need_line(lines, cursor, "", path, "blank line after cover summary")
+
+    failed_checks = [check for check in noncover_checks if check["status"] == "FAILURE"]
+    if failed_checks:
+        cursor = _parse_failure_details(lines, cursor, failed_checks, path)
+    cursor = _need_line(lines, cursor, "", path, "blank line before result banner")
+
+    if should_panic:
+        if not failed_checks:
+            raise ValidationError(
+                f"{path}: expected-panic success contains no failed assertion property"
+            )
+        non_assertion_failure = next(
+            (check["name"] for check in failed_checks if check["class"] != "assertion"),
+            None,
+        )
+        if non_assertion_failure is not None:
+            raise ValidationError(
+                f"{path}: expected-panic success contains non-assertion failure "
+                f"{non_assertion_failure!r}"
+            )
+        expected_banner = (
+            "VERIFICATION:- SUCCESSFUL " "(encountered one or more panics as expected)"
+        )
+    else:
+        if failed_checks:
+            raise ValidationError(
+                f"{path}: ordinary successful verification contains failed property "
+                f"{failed_checks[0]['name']!r}"
+            )
+        expected_banner = "VERIFICATION:- SUCCESSFUL"
+    cursor = _need_line(lines, cursor, expected_banner, path, "Kani success banner")
+
+    time_match = None if cursor >= len(lines) else TIME_RE.fullmatch(lines[cursor])
+    if time_match is None:
+        actual = "end of file" if cursor >= len(lines) else repr(lines[cursor])
+        raise ValidationError(
+            f"{path}:{cursor + 1}: expected verification-time footer within the "
+            "supported numeric envelope; "
+            f"found {actual}"
+        )
+    _validate_verification_time(time_match.group(1), path, cursor + 1)
+    cursor += 1
+    cursor = _need_line(lines, cursor, "", path, "writer's final blank line")
+    if cursor != len(lines):
+        raise ValidationError(f"{path}:{cursor + 1}: nonempty data follows Kani footer")
+
+    undetermined_noncover = next(
+        (
+            check["name"]
+            for check in noncover_checks
+            if check["status"] == "UNDETERMINED"
+        ),
+        None,
+    )
+    if undetermined_noncover is not None:
+        raise ValidationError(
+            f"{path}: successful verification contains undetermined non-cover property "
+            f"{undetermined_noncover!r}"
+        )
+    unsatisfied_cover = next(
+        (check for check in cover_checks if check["status"] != "SATISFIED"), None
+    )
+    if unsatisfied_cover is not None:
+        raise ValidationError(
+            f"{path}: cover property {unsatisfied_cover['name']!r} is "
+            f"{unsatisfied_cover['status']}, not SATISFIED"
+        )
+    return len(cover_checks)
+
+
+def _require_real_directory(path, description):
+    try:
+        mode = path.lstat().st_mode
+    except OSError as error:
+        raise ValidationError(
+            f"cannot inspect {description} {path}: {error}"
+        ) from error
+    if not stat.S_ISDIR(mode):
+        raise ValidationError(f"{description} is not a real directory: {path}")
+
+
+def _walk_real_files(root, description):
+    """Yield regular files without following any symlink below `root`."""
+
+    try:
+        with os.scandir(root) as entries:
+            ordered_entries = sorted(entries, key=lambda entry: entry.name)
+    except OSError as error:
+        raise ValidationError(
+            f"cannot inspect {description} {root}: {error}"
+        ) from error
+    for entry in ordered_entries:
+        path = Path(entry.path)
+        try:
+            mode = entry.stat(follow_symlinks=False).st_mode
+        except OSError as error:
+            raise ValidationError(f"cannot inspect {path}: {error}") from error
+        if stat.S_ISLNK(mode):
+            raise ValidationError(f"symlink is forbidden in {description}: {path}")
+        if stat.S_ISDIR(mode):
+            yield from _walk_real_files(path, description)
+        elif stat.S_ISREG(mode):
+            yield path
+        else:
+            raise ValidationError(f"non-regular path in {description}: {path}")
+
+
+def _abbreviate(names):
+    ordered = sorted(names)
+    shown = ", ".join(repr(name) for name in ordered[:10])
+    if len(ordered) > 10:
+        shown += f", ... ({len(ordered) - 10} more)"
+    return shown
+
+
+def _validate_metadata_root(data, metadata_path):
+    """Validate the pinned root protocol before trusting its proof inventory."""
+
+    if not isinstance(data, dict):
+        raise ValidationError(f"{metadata_path}: Kani metadata root is not an object")
+    actual_root_fields = set(data)
+    if actual_root_fields != METADATA_ROOT_FIELDS:
+        missing = METADATA_ROOT_FIELDS - actual_root_fields
+        unexpected = actual_root_fields - METADATA_ROOT_FIELDS
+        details = []
+        if missing:
+            details.append(f"missing {_abbreviate(missing)}")
+        if unexpected:
+            details.append(f"unexpected {_abbreviate(unexpected)}")
+        raise ValidationError(
+            f"{metadata_path}: metadata root does not match Kani 0.67 schema: "
+            + "; ".join(details)
+        )
+    if data["crate_name"] != EXPECTED_CRATE_NAME:
+        raise ValidationError(
+            f"{metadata_path}: expected crate_name {EXPECTED_CRATE_NAME!r}; "
+            f"found {data['crate_name']!r}"
+        )
+    for field in ("unsupported_features", "contracted_functions"):
+        if not isinstance(data[field], list):
+            raise ValidationError(
+                f"{metadata_path}: metadata field {field!r} is not an array"
+            )
+    if data["autoharness_md"] is not None:
+        raise ValidationError(
+            f"{metadata_path}: canonical proof protocol forbids autoharness metadata"
+        )
+
+    proof_harnesses = data["proof_harnesses"]
+    if not isinstance(proof_harnesses, list):
+        raise ValidationError(
+            f"{metadata_path}: metadata field 'proof_harnesses' is not an array"
+        )
+    if not proof_harnesses:
+        raise ValidationError(f"{metadata_path}: metadata contains no proof harnesses")
+    test_harnesses = data["test_harnesses"]
+    if not isinstance(test_harnesses, list):
+        raise ValidationError(
+            f"{metadata_path}: metadata field 'test_harnesses' is not an array"
+        )
+    if test_harnesses:
+        raise ValidationError(
+            f"{metadata_path}: canonical proof protocol forbids test harnesses"
+        )
+    return proof_harnesses
+
+
+def _load_expected_harnesses(target_dir):
+    _require_real_directory(target_dir, "Kani target")
+    metadata_dir = target_dir / "kani"
+    _require_real_directory(metadata_dir, "Kani metadata root")
+    metadata_files = [
+        path
+        for path in _walk_real_files(metadata_dir, "Kani metadata tree")
+        if path.name.endswith(".kani-metadata.json")
+    ]
+    if len(metadata_files) != 1:
+        raise ValidationError(
+            "fresh Kani target must contain exactly one metadata inventory; "
+            f"found {len(metadata_files)}"
+        )
+    metadata_path = metadata_files[0]
+
+    def object_without_duplicate_keys(pairs):
+        value = {}
+        for key, member in pairs:
+            if key in value:
+                raise ValidationError(
+                    f"{metadata_path}: duplicate JSON object key {key!r}"
+                )
+            value[key] = member
+        return value
+
+    def reject_nonfinite_constant(token):
+        raise ValidationError(f"{metadata_path}: non-finite JSON constant {token!r}")
+
+    try:
+        data = json.loads(
+            metadata_path.read_text(encoding="utf-8"),
+            object_pairs_hook=object_without_duplicate_keys,
+            parse_constant=reject_nonfinite_constant,
+        )
+    except (OSError, UnicodeError, json.JSONDecodeError) as error:
+        raise ValidationError(f"cannot parse {metadata_path}: {error}") from error
+    proof_harnesses = _validate_metadata_root(data, metadata_path)
+
+    expected = {}
+    for index, harness in enumerate(proof_harnesses):
+        if not isinstance(harness, dict):
+            raise ValidationError(
+                f"{metadata_path}: proof_harnesses[{index}] is not an object"
+            )
+        if harness.get("crate_name") != EXPECTED_CRATE_NAME:
+            raise ValidationError(
+                f"{metadata_path}: proof_harnesses[{index}].crate_name must be "
+                f"{EXPECTED_CRATE_NAME!r}"
+            )
+        name = harness.get("pretty_name")
+        if not isinstance(name, str) or not name:
+            raise ValidationError(
+                f"{metadata_path}: proof_harnesses[{index}].pretty_name is not "
+                "a nonempty string"
+            )
+        if _contains_control_characters(name):
+            raise ValidationError(
+                f"{metadata_path}: proof_harnesses[{index}].pretty_name contains "
+                "a control character"
+            )
+        parsed_name = PurePosixPath(name)
+        if (
+            parsed_name.is_absolute()
+            or parsed_name.as_posix() != name
+            or any(part in ("", ".", "..") for part in parsed_name.parts)
+        ):
+            raise ValidationError(
+                f"{metadata_path}: unsafe harness result path in pretty_name {name!r}"
+            )
+        attributes = harness.get("attributes")
+        if not isinstance(attributes, dict) or not isinstance(
+            attributes.get("should_panic"), bool
+        ):
+            raise ValidationError(
+                f"{metadata_path}: proof_harnesses[{index}].attributes.should_panic "
+                "is not a boolean"
+            )
+        if name in expected:
+            raise ValidationError(f"{metadata_path}: duplicate harness pretty_name")
+        expected[name] = attributes["should_panic"]
+    return expected
+
+
+def _load_result_files(target_dir):
+    result_dir = target_dir / "result_output_dir"
+    _require_real_directory(result_dir, "Kani result root")
+    results = {}
+    for path in _walk_real_files(result_dir, "Kani result tree"):
+        name = path.relative_to(result_dir).as_posix()
+        if name in results:
+            raise ValidationError(f"duplicate Kani result path: {name!r}")
+        results[name] = path
+    if not results:
+        raise ValidationError(f"no per-harness result files below {result_dir}")
+    return results
+
+
+def validate(target_dir):
+    expected = _load_expected_harnesses(target_dir)
+    results = _load_result_files(target_dir)
+    actual = set(results)
+    expected_names = set(expected)
+    missing = expected_names - actual
+    unexpected = actual - expected_names
+    if missing or unexpected:
+        details = []
+        if missing:
+            details.append(f"missing: {_abbreviate(missing)}")
+        if unexpected:
+            details.append(f"unexpected: {_abbreviate(unexpected)}")
+        raise ValidationError(
+            "Kani result inventory mismatch (" + "; ".join(details) + ")"
+        )
+
+    cover_count = sum(
+        _parse_result(results[name], expected[name]) for name in sorted(expected)
+    )
+    if cover_count == 0:
+        raise ValidationError(
+            "unfiltered Kani result inventory contains no cover properties"
+        )
+    return len(expected), cover_count
+
+
+def main(argv):
+    if len(argv) != 2:
+        print(f"usage: {argv[0]} KANI_TARGET_DIR", file=sys.stderr)
+        return 2
+    target_dir = Path(argv[1])
+    try:
+        harness_count, cover_count = validate(target_dir)
+    except ValidationError as error:
+        print(f"{Path(argv[0]).name}: {error}", file=sys.stderr)
+        return 1
+    print(
+        f"validated {harness_count} Kani harness result files; "
+        f"all {cover_count} cover properties are SATISFIED"
+    )
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main(sys.argv))
diff --git a/ci/check_kani_cover_test.py b/ci/check_kani_cover_test.py
new file mode 100644
index 0000000000..ae0a719cbf
--- /dev/null
+++ b/ci/check_kani_cover_test.py
@@ -0,0 +1,1084 @@
+#!/usr/bin/env python3
+# Copyright 2026 The Fuchsia Authors
+#
+# Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+# <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+# license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+# This file may not be copied, modified, or distributed except according to
+# those terms.
+
+import json
+import os
+import subprocess
+import sys
+import tempfile
+import unittest
+from pathlib import Path
+
+CHECKER = Path(__file__).with_name("check_kani_cover.py")
+
+
+class CheckKaniCoverTest(unittest.TestCase):
+    def setUp(self):
+        self.temporary_directory = tempfile.TemporaryDirectory()
+        self.target = Path(self.temporary_directory.name)
+        self.metadata_dir = self.target / "kani" / "target" / "debug" / "deps"
+        self.metadata_dir.mkdir(parents=True)
+        self.result_dir = self.target / "result_output_dir"
+        self.result_dir.mkdir()
+
+    def tearDown(self):
+        self.temporary_directory.cleanup()
+
+    def metadata(self, names):
+        harnesses = []
+        for item in names:
+            name, should_panic = item if isinstance(item, tuple) else (item, False)
+            harnesses.append(
+                {
+                    "pretty_name": name,
+                    "crate_name": "zerocopy",
+                    "attributes": {"should_panic": should_panic},
+                }
+            )
+        return {
+            "crate_name": "zerocopy",
+            "proof_harnesses": harnesses,
+            "unsupported_features": [],
+            "test_harnesses": [],
+            "contracted_functions": [],
+            "autoharness_md": None,
+        }
+
+    def write_metadata(self, names, filename="fixture.kani-metadata.json"):
+        (self.metadata_dir / filename).write_text(
+            json.dumps(self.metadata(names)), encoding="utf-8"
+        )
+
+    def write_result(self, name, contents):
+        path = self.result_dir / name
+        path.parent.mkdir(parents=True, exist_ok=True)
+        path.write_text(contents, encoding="utf-8")
+        return path
+
+    def write_single_cover_result(self, name, status, thread=None, property_name=None):
+        satisfied = 1 if status == "SATISFIED" else 0
+        breakdown = {
+            "UNDETERMINED": " (1 undetermined)",
+            "UNREACHABLE": " (1 unreachable)",
+        }.get(status, "")
+        thread_header = f"Thread {thread}:\n" if thread is not None else ""
+        property_name = property_name or f"{name}.cover.1"
+        return self.write_result(
+            name,
+            f"""{thread_header}
+RESULTS:
+Check 1: {property_name}
+\t - Status: {status}
+\t - Description: "cover fixture"
+
+
+SUMMARY:
+ ** 0 of 0 failed
+
+ ** {satisfied} of 1 cover properties satisfied{breakdown}
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+    def write_expected_panic_result(
+        self, name, property_class="assertion", include_failure_location=True
+    ):
+        failure_location = (
+            ' File: "src/lib.rs", line 7, in fixture::panic\n'
+            if include_failure_location
+            else ""
+        )
+        return self.write_result(
+            name,
+            f"""
+RESULTS:
+Check 1: {name}.{property_class}.1
+\t - Status: FAILURE
+\t - Description: "expected panic"
+
+Check 2: {name}.cover.1
+\t - Status: SATISFIED
+\t - Description: "panic input is reachable"
+
+
+SUMMARY:
+ ** 1 of 1 failed
+
+ ** 1 of 1 cover properties satisfied
+
+Failed Checks: expected panic
+{failure_location}
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+Verification Time: 0.01s
+
+""",
+        )
+
+    def write_raw_metadata(self, contents, filename="fixture.kani-metadata.json"):
+        (self.metadata_dir / filename).write_text(contents, encoding="utf-8")
+
+    def run_checker(self, target=None):
+        return subprocess.run(
+            [sys.executable, str(CHECKER), str(target or self.target)],
+            check=False,
+            capture_output=True,
+            text=True,
+        )
+
+    def test_satisfied_cover_fixture_passes(self):
+        self.write_metadata(["fixture::satisfied"])
+        self.write_result(
+            "fixture::satisfied",
+            """
+RESULTS:
+Check 1: fixture::satisfied.assertion.1
+\t - Status: UNREACHABLE
+\t - Description: "assertion failed: true"
+
+Check 2: fixture::satisfied.cover.1
+\t - Status: SATISFIED
+\t - Description: "reachable cover"
+
+
+SUMMARY:
+ ** 0 of 1 failed (1 unreachable)
+
+ ** 1 of 1 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertIn("all 1 cover properties are SATISFIED", result.stdout)
+
+    def test_harness_without_cover_passes_when_another_harness_has_cover(self):
+        self.write_metadata(["fixture::no_cover", "fixture::covered"])
+        self.write_result(
+            "fixture::no_cover",
+            """
+RESULTS:
+Check 1: fixture::no_cover.assertion.1
+\t - Status: SUCCESS
+\t - Description: "assertion failed: true"
+
+
+SUMMARY:
+ ** 0 of 1 failed
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+        self.write_single_cover_result("fixture::covered", "SATISFIED")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertIn("all 1 cover properties are SATISFIED", result.stdout)
+
+    def test_all_harnesses_without_cover_fail(self):
+        self.write_metadata(["fixture::no_cover"])
+        self.write_result(
+            "fixture::no_cover",
+            """
+RESULTS:
+Check 1: fixture::no_cover.assertion.1
+\t - Status: SUCCESS
+\t - Description: "assertion failed: true"
+
+
+SUMMARY:
+ ** 0 of 1 failed
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("contains no cover properties", result.stderr)
+
+    def test_uncovered_fixture_fails(self):
+        self.write_metadata(["fixture::uncovered"])
+        self.write_single_cover_result("fixture::uncovered", "UNSATISFIABLE")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("is UNSATISFIABLE, not SATISFIED", result.stderr)
+
+    def test_unreachable_cover_fixture_fails(self):
+        self.write_metadata(["fixture::unreachable"])
+        self.write_single_cover_result("fixture::unreachable", "UNREACHABLE")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("is UNREACHABLE, not SATISFIED", result.stderr)
+
+    def test_undetermined_cover_fixture_fails(self):
+        self.write_metadata(["fixture::undetermined"])
+        self.write_single_cover_result("fixture::undetermined", "UNDETERMINED")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("is UNDETERMINED, not SATISFIED", result.stderr)
+
+    def test_missing_result_fixture_fails(self):
+        self.write_metadata(["fixture::missing"])
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("no per-harness result files", result.stderr)
+
+    def test_malformed_summary_fixture_fails(self):
+        self.write_metadata(["fixture::malformed"])
+        self.write_result(
+            "fixture::malformed",
+            """
+RESULTS:
+Check 1: fixture::malformed.cover.1
+\t - Status: SATISFIED
+\t - Description: "reachable cover"
+
+
+SUMMARY:
+ ** 0 of 0 failed
+
+ ** 1 of 2 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("canonical cover-property summary", result.stderr)
+
+    def test_malformed_status_breakdown_fixture_fails(self):
+        self.write_metadata(["fixture::malformed_breakdown"])
+        self.write_result(
+            "fixture::malformed_breakdown",
+            """
+RESULTS:
+Check 1: fixture::malformed_breakdown.assertion.1
+\t - Status: UNREACHABLE
+\t - Description: "assertion failed: true"
+
+
+SUMMARY:
+ ** 0 of 1 failed (1 undetermined)
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("canonical normal-property summary", result.stderr)
+
+    def test_cover_summary_after_footer_fixture_fails(self):
+        self.write_metadata(["fixture::late_cover_summary"])
+        self.write_result(
+            "fixture::late_cover_summary",
+            """
+RESULTS:
+Check 1: fixture::late_cover_summary.cover.1
+\t - Status: SATISFIED
+\t - Description: "reachable cover"
+
+
+SUMMARY:
+ ** 0 of 0 failed
+
+VERIFICATION:- SUCCESSFUL
+ ** 1 of 1 cover properties satisfied
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("canonical cover-property summary", result.stderr)
+
+    def test_nonempty_data_after_footer_fixture_fails(self):
+        self.write_metadata(["fixture::trailing"])
+        path = self.write_single_cover_result("fixture::trailing", "SATISFIED")
+        with path.open("a", encoding="utf-8") as result_file:
+            result_file.write("MALFORMED TRAILING RECORD\n")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("nonempty data follows", result.stderr)
+
+    def test_malformed_time_footer_fixture_fails(self):
+        self.write_metadata(["fixture::bad_time"])
+        path = self.write_single_cover_result("fixture::bad_time", "SATISFIED")
+        contents = path.read_text(encoding="utf-8")
+        path.write_text(
+            contents.replace("Verification Time: 0.01s", "Verification Time: +s"),
+            encoding="utf-8",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("verification-time footer", result.stderr)
+
+    def test_crlf_and_bare_cr_line_endings_fail(self):
+        self.write_metadata(["fixture::bad_line_endings"])
+        for line_ending in (b"\r\n", b"\r"):
+            with self.subTest(line_ending=line_ending):
+                path = self.write_single_cover_result(
+                    "fixture::bad_line_endings", "SATISFIED"
+                )
+                path.write_bytes(path.read_bytes().replace(b"\n", line_ending))
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("non-Kani control character", result.stderr)
+
+    def test_impossible_rendered_status_fixture_fails(self):
+        self.write_metadata(["fixture::covered_status"])
+        self.write_result(
+            "fixture::covered_status",
+            """
+RESULTS:
+Check 1: fixture::covered_status.assertion.1
+\t - Status: COVERED
+\t - Description: "impossible regular result status"
+
+
+SUMMARY:
+ ** 0 of 1 failed
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("unknown Kani status 'COVERED'", result.stderr)
+
+    def test_thread_header_fixture_passes(self):
+        self.write_metadata(["fixture::thread"])
+        self.write_single_cover_result("fixture::thread", "SATISFIED", thread=7)
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_expected_panic_assertion_failure_passes(self):
+        self.write_metadata([("fixture::panic", True)])
+        self.write_expected_panic_result("fixture::panic")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_expected_panic_without_failure_location_passes(self):
+        self.write_metadata([("fixture::panic", True)])
+        self.write_expected_panic_result(
+            "fixture::panic", include_failure_location=False
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_expected_panic_without_cover_passes_with_covered_peer(self):
+        self.write_metadata(
+            [("fixture::panic_no_cover", True), "fixture::covered_peer"]
+        )
+        self.write_result(
+            "fixture::panic_no_cover",
+            """
+RESULTS:
+Check 1: fixture::panic_no_cover.assertion.1
+\t - Status: FAILURE
+\t - Description: "expected panic"
+
+
+SUMMARY:
+ ** 1 of 1 failed
+Failed Checks: expected panic
+
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+Verification Time: 0.01s
+
+""",
+        )
+        self.write_single_cover_result("fixture::covered_peer", "SATISFIED")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_ordinary_success_banner_with_failure_fails(self):
+        self.write_metadata(["fixture::ordinary"])
+        path = self.write_expected_panic_result("fixture::ordinary")
+        contents = path.read_text(encoding="utf-8").replace(
+            "VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)",
+            "VERIFICATION:- SUCCESSFUL",
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("ordinary successful verification contains failed", result.stderr)
+
+    def test_expected_panic_nonassertion_failure_fails(self):
+        self.write_metadata([("fixture::panic", True)])
+        self.write_expected_panic_result(
+            "fixture::panic", property_class="array_bounds"
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("contains non-assertion failure", result.stderr)
+
+    def test_expected_panic_without_failure_fails(self):
+        self.write_metadata([("fixture::panic", True)])
+        path = self.write_single_cover_result("fixture::panic", "SATISFIED")
+        contents = path.read_text(encoding="utf-8").replace(
+            "VERIFICATION:- SUCCESSFUL",
+            "VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)",
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("contains no failed assertion", result.stderr)
+
+    def test_multiline_description_and_location_pass(self):
+        self.write_metadata(["fixture::multiline"])
+        self.write_result(
+            "fixture::multiline",
+            """
+RESULTS:
+Check 1: module.with.dot.cover.4294967295
+\t - Status: SATISFIED
+\t - Description: "first line
+middle line
+last line"
+\t - Location: src/lib.rs:7:9 in function fixture::multiline
+
+
+SUMMARY:
+ ** 0 of 0 failed
+
+ ** 1 of 1 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 1s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_cover_without_function_name_passes(self):
+        self.write_metadata(["fixture::bare_cover"])
+        self.write_single_cover_result(
+            "fixture::bare_cover", "SATISFIED", property_name="cover.0"
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_malformed_property_names_fail(self):
+        cases = (
+            ("fixture::bad.cover.1 ", "whitespace/control"),
+            ("fixture::bad.cover.01", "noncanonical Kani property id"),
+            ("fixture::bad.cover.4294967296", "exceeds 4294967295"),
+            ("fixture::bad.Cover.1", "malformed Kani property class"),
+            ("fixture::bad.cover.1.extra", "malformed Kani property class"),
+        )
+        self.write_metadata(["fixture::bad"])
+        for property_name, error in cases:
+            with self.subTest(property_name=property_name):
+                path = self.write_single_cover_result("fixture::bad", "SATISFIED")
+                contents = path.read_text(encoding="utf-8").replace(
+                    "fixture::bad.cover.1", property_name
+                )
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn(error, result.stderr)
+
+    def test_classes_outside_audited_corpus_fail(self):
+        name = "fixture::unknown_class"
+        self.write_metadata([name])
+        for property_class in (
+            "not_a_kani_class",
+            "NaN",
+            "finite_check",
+            "recursion",
+        ):
+            with self.subTest(property_class=property_class):
+                self.write_result(
+                    name,
+                    f"""
+RESULTS:
+Check 1: {name}.{property_class}.1
+\t - Status: SUCCESS
+\t - Description: "fabricated ordinary property"
+
+Check 2: {name}.cover.1
+\t - Status: SATISFIED
+\t - Description: "authentic cover class keeps the global obligation"
+
+
+SUMMARY:
+ ** 0 of 1 failed
+
+ ** 1 of 1 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+                )
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("outside the audited zerocopy vocabulary", result.stderr)
+
+    def test_duplicate_property_name_fails(self):
+        name = "fixture::duplicate_property"
+        self.write_metadata([name])
+        self.write_result(
+            name,
+            f"""
+RESULTS:
+Check 1: {name}.cover.1
+\t - Status: SATISFIED
+\t - Description: "first copy"
+
+Check 2: {name}.cover.1
+\t - Status: SATISFIED
+\t - Description: "second copy"
+
+
+SUMMARY:
+ ** 0 of 0 failed
+
+ ** 2 of 2 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+Verification Time: 0.01s
+
+""",
+        )
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("duplicate Kani property name", result.stderr)
+
+    def test_trailing_space_cannot_reclassify_cover_as_noncover(self):
+        self.write_metadata(["fixture::bad"])
+        path = self.write_single_cover_result("fixture::bad", "UNREACHABLE")
+        contents = path.read_text(encoding="utf-8").replace(
+            "fixture::bad.cover.1", "fixture::bad.cover.1 "
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("whitespace/control", result.stderr)
+
+    def test_malformed_check_and_thread_numbers_fail(self):
+        cases = (("Check 1:", "Check 01:"), ("Thread 7:", "Thread 07:"))
+        for old, new in cases:
+            with self.subTest(new=new):
+                self.write_metadata(["fixture::number"])
+                path = self.write_single_cover_result(
+                    "fixture::number", "SATISFIED", thread=7
+                )
+                contents = path.read_text(encoding="utf-8").replace(old, new)
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("malformed Kani", result.stderr)
+
+    def test_noncanonical_summary_counts_fail(self):
+        self.write_metadata(["fixture::summary"])
+        path = self.write_single_cover_result("fixture::summary", "SATISFIED")
+        contents = path.read_text(encoding="utf-8").replace(
+            " ** 0 of 0 failed", " ** 00 of 0 failed"
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("canonical normal-property summary", result.stderr)
+
+    def test_noncanonical_time_values_fail(self):
+        self.write_metadata(["fixture::time"])
+        for time_value in ("00.01", "0.010", "1e-2", "+0.01"):
+            with self.subTest(time_value=time_value):
+                path = self.write_single_cover_result("fixture::time", "SATISFIED")
+                contents = path.read_text(encoding="utf-8").replace(
+                    "Verification Time: 0.01s",
+                    f"Verification Time: {time_value}s",
+                )
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("verification-time footer", result.stderr)
+
+    def test_verification_time_numeric_envelope(self):
+        self.write_metadata(["fixture::time"])
+        cases = (
+            ("0", True, None),
+            ("0.000000001", True, None),
+            ("0.01", True, None),
+            ("1", True, None),
+            ("18446744000000000000", True, None),
+            ("0.0000000001", False, "one-nanosecond resolution"),
+            ("0.1234567891", False, "shortest-decimal precision"),
+            ("18446745000000000000", False, "rendered Duration range"),
+        )
+        for time_value, should_pass, error in cases:
+            with self.subTest(time_value=time_value):
+                path = self.write_single_cover_result("fixture::time", "SATISFIED")
+                contents = path.read_text(encoding="utf-8").replace(
+                    "Verification Time: 0.01s",
+                    f"Verification Time: {time_value}s",
+                )
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                if should_pass:
+                    self.assertEqual(result.returncode, 0, result.stderr)
+                else:
+                    self.assertEqual(result.returncode, 1)
+                    self.assertIn(error, result.stderr)
+
+    def test_unterminated_description_fails(self):
+        self.write_metadata(["fixture::description"])
+        path = self.write_single_cover_result("fixture::description", "SATISFIED")
+        contents = path.read_text(encoding="utf-8").replace(
+            'Description: "cover fixture"', 'Description: "cover fixture'
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("control record in unterminated description", result.stderr)
+
+    def test_control_record_inside_multiline_description_fails(self):
+        self.write_metadata(["fixture::description"])
+        path = self.write_single_cover_result("fixture::description", "SATISFIED")
+        contents = path.read_text(encoding="utf-8").replace(
+            'Description: "cover fixture"',
+            'Description: "first line\nCheck 2: fake.cover.1\nlast line"',
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("control record", result.stderr)
+
+    def test_reordered_or_duplicate_check_fields_fail(self):
+        cases = (
+            (
+                '\t - Status: SATISFIED\n\t - Description: "cover fixture"',
+                '\t - Description: "cover fixture"\n\t - Status: SATISFIED',
+            ),
+            (
+                "\t - Status: SATISFIED",
+                "\t - Status: SATISFIED\n\t - Status: SATISFIED",
+            ),
+            (
+                '\t - Description: "cover fixture"',
+                '\t - Description: "cover fixture"\n' '\t - Description: "duplicate"',
+            ),
+        )
+        self.write_metadata(["fixture::fields"])
+        for old, new in cases:
+            with self.subTest(new=new):
+                path = self.write_single_cover_result("fixture::fields", "SATISFIED")
+                contents = path.read_text(encoding="utf-8").replace(old, new)
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+
+    def test_malformed_optional_locations_fail(self):
+        self.write_metadata(["fixture::location"])
+        path = self.write_single_cover_result("fixture::location", "SATISFIED")
+        contents = path.read_text(encoding="utf-8").replace(
+            '\t - Description: "cover fixture"',
+            '\t - Description: "cover fixture"\n\t - Location: ',
+        )
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("malformed location", result.stderr)
+
+    def test_kani_location_display_variants_pass(self):
+        self.write_metadata(["fixture::location"])
+        locations = (
+            "src/lib.rs",
+            "src/lib.rs:7",
+            "src/lib.rs:7:9 in function fixture::location",
+            "Unknown file in function fixture::location",
+            "generated proof file.c",
+        )
+        for location in locations:
+            with self.subTest(location=location):
+                path = self.write_single_cover_result(
+                    "fixture::location", "SATISFIED"
+                )
+                contents = path.read_text(encoding="utf-8").replace(
+                    '\t - Description: "cover fixture"',
+                    '\t - Description: "cover fixture"\n'
+                    f"\t - Location: {location}",
+                )
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 0, result.stderr)
+
+    def test_c1_controls_in_result_records_fail(self):
+        self.write_metadata(["fixture::control"])
+        cases = (
+            (
+                "property name",
+                "fixture::control.cover.1",
+                "fixture::control.cover.\u0080",
+            ),
+            ("description", "cover fixture", "cover\u0085fixture"),
+            (
+                "location",
+                '\t - Description: "cover fixture"',
+                '\t - Description: "cover fixture"\n'
+                "\t - Location: src/\u009flib.rs",
+            ),
+        )
+        for description, old, new in cases:
+            with self.subTest(description=description):
+                path = self.write_single_cover_result(
+                    "fixture::control", "SATISFIED"
+                )
+                contents = path.read_text(encoding="utf-8").replace(old, new)
+                path.write_text(contents, encoding="utf-8")
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("non-Kani control character", result.stderr)
+
+    def test_noncanonical_failure_detail_line_number_fails(self):
+        self.write_metadata([("fixture::panic", True)])
+        path = self.write_expected_panic_result("fixture::panic")
+        contents = path.read_text(encoding="utf-8").replace("line 7", "line 07")
+        path.write_text(contents, encoding="utf-8")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("malformed failed-check location", result.stderr)
+
+    def test_stale_result_inventory_fixture_fails(self):
+        self.write_metadata(["fixture::expected"])
+        self.write_single_cover_result("fixture::stale", "SATISFIED")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("missing: 'fixture::expected'", result.stderr)
+        self.assertIn("unexpected: 'fixture::stale'", result.stderr)
+
+    def test_multiple_populated_metadata_inventories_fail(self):
+        self.write_metadata(["fixture::first"], "first.kani-metadata.json")
+        self.write_metadata(["fixture::second"], "second.kani-metadata.json")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("exactly one metadata inventory; found 2", result.stderr)
+
+    def test_second_empty_metadata_inventory_fails(self):
+        self.write_metadata(["fixture::selected"], "selected.kani-metadata.json")
+        self.write_metadata([], "stale-empty.kani-metadata.json")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("exactly one metadata inventory; found 2", result.stderr)
+
+    def test_metadata_root_must_match_pinned_schema_and_crate(self):
+        self.write_single_cover_result("fixture::covered", "SATISFIED")
+        cases = []
+
+        missing = self.metadata(["fixture::covered"])
+        del missing["contracted_functions"]
+        cases.append(("missing field", missing, "metadata root does not match"))
+
+        unexpected = self.metadata(["fixture::covered"])
+        unexpected["future_field"] = []
+        cases.append(("unexpected field", unexpected, "metadata root does not match"))
+
+        wrong_crate = self.metadata(["fixture::covered"])
+        wrong_crate["crate_name"] = "different_crate"
+        cases.append(("wrong crate", wrong_crate, "expected crate_name 'zerocopy'"))
+
+        wrong_unsupported = self.metadata(["fixture::covered"])
+        wrong_unsupported["unsupported_features"] = {}
+        cases.append(("unsupported type", wrong_unsupported, "is not an array"))
+
+        wrong_contracted = self.metadata(["fixture::covered"])
+        wrong_contracted["contracted_functions"] = None
+        cases.append(("contracts type", wrong_contracted, "is not an array"))
+
+        autoharness = self.metadata(["fixture::covered"])
+        autoharness["autoharness_md"] = {"chosen": [], "skipped": {}}
+        cases.append(("autoharness", autoharness, "forbids autoharness metadata"))
+
+        for description, metadata, error in cases:
+            with self.subTest(description=description):
+                self.write_raw_metadata(json.dumps(metadata))
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn(error, result.stderr)
+
+    def test_proof_and_test_harness_protocol_is_separate(self):
+        name = "fixture::covered"
+        proof = self.metadata([name])["proof_harnesses"][0]
+        self.write_single_cover_result(name, "SATISFIED")
+
+        test_only = self.metadata([])
+        test_only["test_harnesses"] = [proof]
+        self.write_raw_metadata(json.dumps(test_only))
+        result = self.run_checker()
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("metadata contains no proof harnesses", result.stderr)
+
+        mixed = self.metadata([name])
+        mixed["test_harnesses"] = [proof]
+        self.write_raw_metadata(json.dumps(mixed))
+        result = self.run_checker()
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("canonical proof protocol forbids test harnesses", result.stderr)
+
+    def test_nested_harness_crate_must_match_root(self):
+        metadata = self.metadata(["fixture::covered"])
+        metadata["proof_harnesses"][0]["crate_name"] = "different_crate"
+        self.write_raw_metadata(json.dumps(metadata))
+        self.write_single_cover_result("fixture::covered", "SATISFIED")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("proof_harnesses[0].crate_name must be 'zerocopy'", result.stderr)
+
+    def test_control_characters_in_harness_names_fail(self):
+        for control in ("\n", "\t", "\x7f", "\x80", "\x85", "\x9f"):
+            with self.subTest(control=repr(control)):
+                name = f"fixture::{control}bad"
+                self.write_metadata([name])
+                self.write_single_cover_result(
+                    name, "SATISFIED", property_name="cover.0"
+                )
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("pretty_name contains a control character", result.stderr)
+
+    def test_duplicate_root_metadata_key_fails(self):
+        self.write_raw_metadata("""{
+  "crate_name": "fixture",
+  "proof_harnesses": [],
+  "proof_harnesses": [
+    {"pretty_name": "fixture::duplicate", "attributes": {"should_panic": false}}
+  ],
+  "test_harnesses": []
+}""")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("duplicate JSON object key 'proof_harnesses'", result.stderr)
+
+    def test_duplicate_nested_metadata_key_fails(self):
+        self.write_raw_metadata("""{
+  "crate_name": "fixture",
+  "proof_harnesses": [
+    {
+      "pretty_name": "fixture::first",
+      "pretty_name": "fixture::second",
+      "attributes": {"should_panic": false}
+    }
+  ],
+  "test_harnesses": []
+}""")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("duplicate JSON object key 'pretty_name'", result.stderr)
+
+    def test_nonfinite_json_constants_fail(self):
+        for constant in ("NaN", "Infinity", "-Infinity"):
+            with self.subTest(constant=constant):
+                self.write_raw_metadata(
+                    "{"
+                    '"crate_name":"fixture",'
+                    '"proof_harnesses":[],"test_harnesses":[],'
+                    f'"unexpected":{constant}'
+                    "}"
+                )
+
+                result = self.run_checker()
+
+                self.assertEqual(result.returncode, 1)
+                self.assertIn("non-finite JSON constant", result.stderr)
+
+    def test_metadata_should_panic_must_be_boolean(self):
+        self.write_raw_metadata("""{
+  "crate_name": "zerocopy",
+  "proof_harnesses": [
+    {
+      "pretty_name": "fixture::bad",
+      "crate_name": "zerocopy",
+      "attributes": {"should_panic": 1}
+    }
+  ],
+  "unsupported_features": [],
+  "test_harnesses": [],
+  "contracted_functions": [],
+  "autoharness_md": null
+}""")
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("should_panic is not a boolean", result.stderr)
+
+    def test_noncanonical_metadata_result_path_fails(self):
+        self.write_metadata(["fixture//bad"])
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("unsafe harness result path", result.stderr)
+
+    def test_symlink_metadata_leaf_fails(self):
+        with tempfile.TemporaryDirectory() as external_directory:
+            metadata = {
+                "crate_name": "fixture",
+                "proof_harnesses": [],
+                "test_harnesses": [],
+            }
+            external_path = Path(external_directory) / "outside.kani-metadata.json"
+            external_path.write_text(json.dumps(metadata), encoding="utf-8")
+            (self.metadata_dir / "fixture.kani-metadata.json").symlink_to(external_path)
+
+            result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("symlink is forbidden in Kani metadata tree", result.stderr)
+
+    def test_symlink_result_root_fails(self):
+        self.write_metadata(["fixture::covered"])
+        self.result_dir.rmdir()
+        with tempfile.TemporaryDirectory() as external_directory:
+            self.result_dir.symlink_to(external_directory, target_is_directory=True)
+
+            result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("Kani result root is not a real directory", result.stderr)
+
+    def test_symlink_result_leaf_fails(self):
+        self.write_metadata(["fixture::covered"])
+        with tempfile.TemporaryDirectory() as external_directory:
+            external_path = Path(external_directory) / "outside-result"
+            external_path.write_text("not trusted\n", encoding="utf-8")
+            (self.result_dir / "fixture::covered").symlink_to(external_path)
+
+            result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("symlink is forbidden in Kani result tree", result.stderr)
+
+    def test_nonregular_result_leaf_fails(self):
+        self.write_metadata(["fixture::covered"])
+        fifo = self.result_dir / "fixture::covered"
+        os.mkfifo(fifo)
+
+        result = self.run_checker()
+
+        self.assertEqual(result.returncode, 1)
+        self.assertIn("non-regular path in Kani result tree", result.stderr)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/githooks/pre-push b/githooks/pre-push
index d5890e9fc3..1922af85bc 100755
--- a/githooks/pre-push
+++ b/githooks/pre-push
@@ -16,11 +16,10 @@ echo "Running pre-push git hook: $0"
 # Background all jobs and wait for them so they can run in parallel.
 ./ci/check_actions.sh                                  & ACTIONS_PID=$!
 ./ci/check_fmt.sh                                      & FMT_PID=$!
+python3 ./ci/check_kani_cover_test.py                  & KANI_COVER_TEST_PID=$!
 ./ci/check_job_dependencies.sh      >/dev/null         & JOB_DEPS_PID=$!
 ./zerocopy/ci/check_all_toolchains_tested.sh >/dev/null & TOOLCHAINS_PID=$!
 ./zerocopy/ci/check_readme.sh                >/dev/null & README_PID=$!
-./zerocopy/ci/run_kani.sh --self-test-cover-parser >/dev/null &
-KANI_RUNNER_PID=$!
 ./zerocopy/ci/check_stale_stderr.sh          >/dev/null & STALE_STDERR_PID=$!
 ./zerocopy/ci/check_versions.sh              >/dev/null & VERSIONS_PID=$!
 ./zerocopy/ci/check_msrv_is_minimal.sh       >/dev/null & MSRV_PID=$!
@@ -36,7 +35,7 @@ wait $FMT_PID
 wait $TOOLCHAINS_PID
 wait $JOB_DEPS_PID
 wait $README_PID
-wait $KANI_RUNNER_PID
+wait $KANI_COVER_TEST_PID
 wait $STALE_STDERR_PID
 wait $VERSIONS_PID
 wait $MSRV_PID
@@ -50,6 +49,9 @@ wait $MSRV_PID
 # This was added because, in #728, we added
 # `zerocopy/ci/check_all_toolchains_tested.sh` without calling it from this
 # script.
+# `./ci/check_kani_cover.py` is invoked against both passing and failing
+# fixtures by `./ci/check_kani_cover_test.py`; a real target is checked by
+# `./zerocopy/ci/run_kani.sh` after its single proof run.
 shopt -s extglob
 GLOBIGNORE="./*/@(release_crate_version|check_todo|release_anneal_version).sh" # We don't want to run these
 for f in ./ci/*; do
diff --git a/zerocopy/agent_docs/validation.md b/zerocopy/agent_docs/validation.md
index 124f8183ca..03b8815828 100644
--- a/zerocopy/agent_docs/validation.md
+++ b/zerocopy/agent_docs/validation.md
@@ -76,7 +76,27 @@ usually sufficient.
       and Kani's model of Rust.
     - **How to Write Proofs:**
         - **Harnesses:** Mark proof functions with `#[kani::proof]`.
-        - **Inputs:** Use `kani::any()` to generate arbitrary inputs.
+        - **Inputs:** Use `kani::any()` to generate arbitrary inputs. Kani
+          0.67's [tagged `any` contract] says that `any::<T>()` constructs an
+          arbitrary valid `T`, and that `Arbitrary` implementations are
+          expected to represent every possible value. Its tagged generic
+          [array dispatch] delegates `[T; N]` generation to `T::any_array`;
+          tagged [primitive implementations] override that method and obtain
+          primitive arrays, as well as scalar primitive integers, from raw
+          model hooks. The tagged [raw-any functions] carry the hooks which the
+          compiler's [raw-any lowering] and [raw-array lowering] replace with
+          destination-typed nondeterministic expressions. Kani's [dependency
+          pin] selects CBMC 6.8.0, whose [nondeterminism model] and
+          [separate-choice example] permit separately evaluated
+          nondeterministic expressions to choose differently. Treat
+          completeness, validity, and the premise that each
+          dynamic evaluation is a fresh, mutually unconstrained choice as
+          TOOL/TCB inputs, not properties proved by a harness. `kani::assume`
+          only
+          filters this generated domain; it does not establish its original
+          completeness. A custom or derived `Arbitrary` implementation needs
+          its own domain/image argument because the safe trait cannot enforce
+          the documented completeness expectation.
         - **Assumptions:** Use `kani::assume(condition)` to constrain inputs to
           valid states (e.g., `align.is_power_of_two()`).
         - **Assertions:** Use `assert!(condition)` to verify the properties you
@@ -103,23 +123,21 @@ usually sufficient.
           factored into a nearby family or module scope only when every covered
           harness refers to it unambiguously.
         - **Non-vacuity:** Use `kani::cover!` to check that important input and
-          result partitions are reachable. Every assumption must correspond to
-          a documented precondition or to the stated proof bound. Do not reject
-          inputs using an impossible assumption or a diverging loop. Kani 0.67
-          [treats cover properties as reporting-only][Kani cover renderer] and
-          has no
-          `--fail-on-cover` option: zero satisfied covers can accompany a
-          successful verification result. `ci/run_kani.sh` therefore checks
-          every emitted cover summary and fails unless all cover properties are
-          satisfied. Its parser is part of the pinned-version audit and must be
-          revalidated when Kani or its output format changes.
-        - **Bit validity:** `kani::any::<T>()` produces only valid instances of
-          `T`. To verify a byte validator, generate arbitrary bytes and decide
-          expected acceptance using an independent oracle before consulting the
-          target. Never materialize `T` merely because the validator under
-          proof accepts: that validator may be the bug. Construct `T` only
-          through an independently safe checked operation. If no such operation
-          exists, exercise only a non-materializing decision path for invalid
+          result partitions are reachable. The CI and local commands below use
+          a fresh explicit target and per-harness output, then fail unless every
+          emitted cover-class property is `SATISFIED`; Kani's successful
+          verification result alone is insufficient. Every assumption must
+          correspond to a documented precondition or to the stated proof bound.
+          Do not reject inputs using an impossible assumption or a diverging
+          loop.
+        - **Bit validity:** Under the TOOL/TCB premise recorded in **Inputs**,
+          `kani::any::<T>()` produces only valid instances of `T`. To verify a
+          byte validator, generate arbitrary bytes and decide expected
+          acceptance using an independent oracle before consulting the target.
+          Never materialize `T` merely because the validator under proof
+          accepts: that validator may be the bug. Construct `T` only through an
+          independently safe checked operation. If no such operation exists,
+          exercise only a non-materializing decision path for invalid
           candidates and document that limitation.
         - **Soundness boundary:** State which obligations Kani does not prove.
           In particular, Kani does not completely check reference aliasing,
@@ -148,7 +166,11 @@ usually sufficient.
       `x86_64-unknown-linux-gnu` (64-bit, little-endian) with
       `__internal_use_only_features_that_work_on_stable` (`alloc`, `derive`,
       `simd`, and `std`), `-Zfunction-contracts`, and one layout selected by
-      `--randomize-layout` per invocation. Source-level proof scopes should
+      `--randomize-layout` per invocation. The runner also supplies a fresh
+      explicit `--target-dir` with
+      `-Zunstable-options --output-into-files`, followed by
+      `ci/check_kani_cover.py`; this output/checking pair changes the acceptance
+      condition, not the modeled Rust program. Source-level proof scopes should
       refer to this common configuration and state any deviations.
     - **Compiler and documentation compatibility:** After installing the
       pinned Kani release, inspect the `kani-compiler` executable in that
@@ -170,6 +192,74 @@ usually sufficient.
       target, CBMC, and option-behavior record; recheck every versioned Rust
       contract against the new compiler snapshot; and rerun the complete Kani
       suite. Only then update the label to the new pin.
+    - **Fail-closed cover enforcement for Kani 0.67:** This release does not
+      expose `--fail-on-cover`; its [exact argument declaration] instead gates
+      `--output-into-files` behind `-Zunstable-options`. Its [exact result
+      renderer] explicitly excludes `kani::cover!` properties from overall
+      verification success, maps their results to `SATISFIED`,
+      `UNSATISFIABLE`, `UNREACHABLE`, or `UNDETERMINED`, and emits a separate
+      `N of M cover properties satisfied` summary only when cover properties
+      exist. The [Kani 0.67 result documentation] gives the same statuses and
+      syntax. Its [exact property-name formatter] renders the `cover` class as
+      `<function>.cover.<integer>` (or `cover.<integer>` without a function),
+      which is the only form the checker classifies as a cover. This is a
+      version-pinned audited output-format premise, not a general Kani format
+      contract. The [per-harness writer] renders the complete regular-format
+      result for each selected harness below the explicit target's
+      `result_output_dir`; [exact result assembly] appends the verification-time
+      footer; and the compiler's [exact metadata schema] calls its two inventory
+      fields the proof and test harnesses discovered in the compiled crate. The
+      canonical CI invocation supplies no harness filter and does not enable
+      test harnesses, so that discovery is the complete proof-harness set for
+      the selected zerocopy package/configuration. `ci/run_kani.sh` rejects
+      Kani's `--harness`, `--exact`, and `--tests` selection flags to preserve
+      that no-filter protocol.
+
+      `ci/check_kani_cover.py` therefore consumes the one Kani run rather than
+      rerunning it. On a fresh target it requires real, non-symlink directory
+      roots; exactly one regular metadata file with Kani 0.67's exact six-field
+      root; `zerocopy` as both root and proof-harness crate identity; a nonempty
+      proof-harness list; an empty test-harness list; null autoharness metadata;
+      and array-typed unsupported-feature and contracted-function metadata. It
+      decodes only the inventory-bearing nested fields rather than claiming to
+      validate every unused nested metadata field. It then requires an exact
+      one-to-one set of regular result files; a structurally complete successful
+      result for every harness; unique full property identifiers; only the 23
+      property classes found in the audited, complete zerocopy Kani 0.67
+      corpus; agreement between parsed properties and both summaries; at least
+      one cover across the run; and `SATISFIED` for every cover-class property.
+      A newly observed legitimate property class requires a deliberate
+      full-corpus re-audit before it is added to that allowlist.
+
+      The regular renderer's source-location components are independently
+      optional arbitrary strings: it can emit a file alone, file/line,
+      file/line/column, any of those followed by a function, or an unknown-file
+      function form. In particular, every nonempty control-free string is a
+      possible file-only payload, so the checker validates the location record's
+      position and envelope but makes no unsupported claim to authenticate its
+      internal fields. The verification-time footer is likewise ancillary to
+      the verdict. The checker requires the producer's plain decimal spelling,
+      one-nanosecond-to-binary32-`2^64` numeric envelope (plus zero), and at most
+      nine significant digits. Those are necessary producer bounds, not an
+      assertion that the Python checker recognizes the exact image of Rust's
+      binary32 shortest-decimal formatter.
+
+      For an individual harness with no covers, Kani omits the cover summary;
+      the checker accepts that case only after parsing the complete check
+      inventory and finding no cover-class checks. Missing, stale, duplicate,
+      symlinked, wrong-crate, test-only, control-bearing, unaudited-class, or
+      otherwise malformed inventory artifacts, and unsatisfiable, unreachable,
+      or undetermined cover evidence, all fail closed. A nonzero Kani exit still
+      fails directly before the checker runs.
+
+      This validates the integrity of Kani's emitted inventory, not source-level
+      proof coverage. It has no independent manifest of the harness and cover
+      declarations which ought to exist. Deleting a harness, or deleting one
+      cover while at least one other remains, can remove that obligation from
+      both Kani's metadata/results and the checker count. Review the documented
+      proof scopes and source diff for those coverage regressions; add an
+      independently maintained inventory if they must become mechanically
+      enforced.
     - **Recorded toolchain audit for `kani-version: 0.67.0`:** On 2026-09-08,
       `kani-compiler --version --verbose` reported `rustc 1.93.0-nightly`, commit
       `53732d5e076329a62f71d3c6901886ce8a71e812` dated 2025-11-20, LLVM 21.1.5,
@@ -178,25 +268,40 @@ usually sufficient.
       The bundled `cbmc --version` reported CBMC 6.8.0, and its `--help`
       reported `--no-malloc-may-fail  disable potential malloc failure` and
       `--malloc-may-fail  allow malloc calls to return a null pointer`. The
-      admitted compatibility proposition is that the versioned Rust 1.93.0
-      contracts cited by the current proofs describe the corresponding
-      behavior of this nightly snapshot. This was checked manually, not proved
-      by Kani. The audited terse output reports cover summaries as
-      `** N of M cover properties satisfied`, with canonical nonnegative `N`
-      and positive `M`. `ci/run_kani.sh` rejects malformed summary candidates,
-      requires `N == M` for every summary, and requires at least one recognized
-      summary. Pre-push exercises its parser against valid, unsatisfied,
-      absent, nonnumeric, zero-total, noncanonical, extra-token, numeric-
-      precision-edge, and mixed multiple-summary fixtures. Kani 0.67
-      [does not model stack unwinding][Kani panic strategies] even though
-      its bundled compiler's target cfg reports `panic="unwind"`; proofs may
-      use reachable panics as failed properties but may not infer cleanup or
-      post-panic behavior.
+      `cargo kani --help` output exposed no `--fail-on-cover`, and a direct
+      `cargo kani --fail-on-cover --version` probe rejected that argument. A
+      direct `-Zunstable-options --output-into-files` probe confirmed the exact
+      per-harness result and metadata syntax consumed by the checker above. The
+      exact Kani 0.67 [panic-strategy support record] says stack unwinding is
+      not modeled even though the bundled compiler reports `panic="unwind"`;
+      under its exact [panic-checking record] and [verification-result
+      semantics], proofs may use a reachable panic as a failed property, but
+      may not infer cleanup or post-panic behavior. The admitted compatibility
+      proposition is that the versioned Rust 1.93.0 contracts cited by the
+      current proofs describe the corresponding behavior of this nightly
+      snapshot. This was checked manually, not proved by Kani.
 
 [Rust feature support]: https://model-checking.github.io/kani/rust-feature-support.html
 [undefined-behaviour guide]: https://model-checking.github.io/kani/undefined-behaviour.html
-[Kani cover renderer]: https://github.com/model-checking/kani/blob/kani-0.67.0/kani-driver/src/cbmc_property_renderer.rs
-[Kani panic strategies]: https://github.com/model-checking/kani/blob/kani-0.67.0/docs/src/rust-feature-support.md#panic-strategies
+[tagged `any` contract]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L255-L279
+[array dispatch]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L125-L131
+[primitive implementations]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/arbitrary.rs#L22-L70
+[raw-any functions]: https://github.com/model-checking/kani/blob/kani-0.67.0/library/kani_core/src/lib.rs#L333-L367
+[raw-any lowering]: https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L334-L375
+[raw-array lowering]: https://github.com/model-checking/kani/blob/kani-0.67.0/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L1034-L1044
+[dependency pin]: https://github.com/model-checking/kani/blob/kani-0.67.0/kani-dependencies#L1-L3
+[nondeterminism model]: https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L7-L13
+[separate-choice example]: https://github.com/diffblue/cbmc/blob/cbmc-6.8.0/doc/cprover-manual/modeling-nondeterminism.md#L46-L59
+[exact argument declaration]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/args/mod.rs
+[exact result renderer]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/cbmc_property_renderer.rs
+[Kani 0.67 result documentation]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/docs/src/verification-results.md#cover-property-results
+[exact property-name formatter]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/cbmc_output_parser.rs
+[per-harness writer]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/harness_runner.rs
+[exact result assembly]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani-driver/src/call_cbmc.rs
+[exact metadata schema]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/kani_metadata/src/lib.rs
+[panic-strategy support record]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/docs/src/rust-feature-support.md#panic-strategies
+[panic-checking record]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/README.md
+[verification-result semantics]: https://github.com/model-checking/kani/blob/4feaaad1d6a2378a6ff6caa3b4fc5d6999c7bb5d/docs/src/verification-results.md
 
 Before running proofs locally, install the Kani version pinned in
 `.github/workflows/ci.yml`. Run the same proof configuration as CI with:
@@ -211,6 +316,10 @@ ci/run_kani.sh \
   --randomize-layout
 ```
 
+The runner's private fresh target is part of the checker protocol: reusing one
+can leave Kani metadata or result files from another invocation, which the
+checker rejects.
+
 ## Feature Gates
 
 When editing code gated by a feature, compile **with and without** that feature.
diff --git a/zerocopy/ci/run_kani.sh b/zerocopy/ci/run_kani.sh
index f81c6e1910..ac5f0667de 100755
--- a/zerocopy/ci/run_kani.sh
+++ b/zerocopy/ci/run_kani.sh
@@ -10,87 +10,39 @@
 
 set -eo pipefail
 
+# The metadata/result equality below establishes completeness only for the
+# harness set which this invocation asks Kani to compile. CI is intentionally a
+# no-filter run; reject the proof/test selection flags most likely to make a
+# local invocation look like the full-suite protocol while checking a subset.
+for argument in "$@"; do
+    case "${argument}" in
+        --harness | --harness=* | --exact | --tests)
+            echo "run_kani.sh does not support harness-selection argument: ${argument}" >&2
+            exit 2
+            ;;
+    esac
+done
+
 ZEROCOPY_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." && pwd)"
 readonly ZEROCOPY_DIR
-KANI_OUTPUT="$(mktemp)"
+REPO_DIR="$(dirname -- "${ZEROCOPY_DIR}")"
+readonly REPO_DIR
+KANI_SCRATCH="$(mktemp -d)"
+readonly KANI_SCRATCH
+KANI_OUTPUT="${KANI_SCRATCH}/combined-output.log"
 readonly KANI_OUTPUT
-trap 'rm -f "${KANI_OUTPUT}"' EXIT
-
-check_cover_summaries() {
-    awk '
-        /cover[[:space:]]+properties[[:space:]]+satisfied/ {
-            found_cover_candidate = 1
-            if (NF != 7 || $1 != "**" || $3 != "of" || $5 != "cover" ||
-                    $6 != "properties" || $7 != "satisfied" ||
-                    $2 !~ /^(0|[1-9][0-9]*)$/ || $4 !~ /^[1-9][0-9]*$/) {
-                print "Malformed Kani cover summary: " $0 > "/dev/stderr"
-                malformed_cover_summary = 1
-            } else {
-                found_cover_summary = 1
-                # Canonical decimal strings are numerically equal exactly when
-                # their strings are equal; this avoids AWK numeric precision
-                # limits for arbitrarily long counts.
-                if (("count:" $2) != ("count:" $4)) {
-                    print "Kani cover obligation failed: " $0 > "/dev/stderr"
-                    failed_cover = 1
-                }
-            }
-        }
-        END {
-            if (malformed_cover_summary) {
-                exit 2
-            }
-            if (!found_cover_candidate || !found_cover_summary) {
-                print "Kani emitted no recognized cover summary" > "/dev/stderr"
-                exit 2
-            }
-            if (failed_cover) {
-                exit 1
-            }
-        }
-    ' "$1"
-}
-
-expect_parser_result() {
-    local expected="$1"
-    local fixture="$2"
-    local actual
-    printf '%s\n' "${fixture}" > "${KANI_OUTPUT}"
-    if check_cover_summaries "${KANI_OUTPUT}" >/dev/null 2>&1; then
-        actual=success
-    else
-        actual=failure
-    fi
-    if [[ "${actual}" != "${expected}" ]]; then
-        echo "Kani cover parser self-test expected ${expected}: ${fixture}" >&2
-        exit 1
-    fi
-}
-
-if (( $# == 1 )) && [[ "$1" == "--self-test-cover-parser" ]]; then
-    readonly SELF_TEST_VALID_SUMMARY="** 1 of 1 cover properties satisfied"
-    expect_parser_result success "** 2 of 2 cover properties satisfied"
-    expect_parser_result failure "** 1 of 2 cover properties satisfied"
-    expect_parser_result failure "VERIFICATION:- SUCCESSFUL"
-    expect_parser_result failure "** x of x cover properties satisfied"
-    expect_parser_result failure "** 0 of 0 cover properties satisfied"
-    expect_parser_result failure "** 01 of 01 cover properties satisfied"
-    expect_parser_result failure "** 1 of 1 cover properties satisfied extra"
-    expect_parser_result success \
-        "** 9007199254740993 of 9007199254740993 cover properties satisfied"
-    expect_parser_result failure \
-        "** 9007199254740992 of 9007199254740993 cover properties satisfied"
-    expect_parser_result failure \
-        "${SELF_TEST_VALID_SUMMARY}"$'\n'"** 1 of 2 cover properties satisfied"
-    expect_parser_result failure \
-        "${SELF_TEST_VALID_SUMMARY}"$'\n'"* 1 of 1 cover properties satisfied"
-    exit 0
-fi
+KANI_TARGET="${KANI_SCRATCH}/target"
+readonly KANI_TARGET
+trap 'rm -rf -- "${KANI_SCRATCH}"' EXIT
 
 cd "${ZEROCOPY_DIR}"
 
 set +e
-"${ZEROCOPY_DIR}/cargo.sh" +stable kani "$@" 2>&1 | tee "${KANI_OUTPUT}"
+"${ZEROCOPY_DIR}/cargo.sh" +stable kani \
+    --target-dir "${KANI_TARGET}" \
+    -Zunstable-options \
+    --output-into-files \
+    "$@" 2>&1 | tee "${KANI_OUTPUT}"
 PIPELINE_STATUS=("${PIPESTATUS[@]}")
 readonly KANI_STATUS="${PIPELINE_STATUS[0]}"
 readonly TEE_STATUS="${PIPELINE_STATUS[1]}"
@@ -104,8 +56,8 @@ if (( TEE_STATUS != 0 )); then
 fi
 
 # Kani 0.67 reports unsatisfied `kani::cover!` properties but still exits
-# successfully. Its CLI has no `--fail-on-cover` option. Parse the exact output
-# format audited in `agent_docs/validation.md` so every emitted non-vacuity
-# summary fails closed, and total absence also fails. Re-audit this parser
+# successfully. Its CLI has no `--fail-on-cover` option. The combined output
+# above is retained for diagnostics, while the checker validates the complete
+# per-harness inventory emitted into the fresh target. Re-audit the checker
 # whenever the pinned Kani version changes.
-check_cover_summaries "${KANI_OUTPUT}"
+python3 "${REPO_DIR}/ci/check_kani_cover.py" "${KANI_TARGET}"