fraware · fraware · Jul 24, 2026 · Jul 24, 2026 · Jul 24, 2026 · Jul 24, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -265,4 +265,43 @@ jobs:
         uses: actions/upload-artifact@v4
         with:
           name: template-conformance
-          path: docs/benchmarks/template-conformance.json
+          path: docs/benchmarks/template-conformance.json
+
+  assurance:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Checkout pcs-core pin
+        uses: actions/checkout@v4
+        with:
+          repository: SentinelOps-CI/pcs-core
+          ref: fb588a41a7eab68064429e3c4dfb26c328b9863d
+          path: pcs-core
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.11'
+      - name: Install OVK with assurance pin
+        env:
+          OVK_PCS_CORE_PATH: ${{ github.workspace }}/pcs-core
+        run: |
+          python -m pip install --upgrade pip
+          python scripts/sync_package_data.py
+          pip install --no-cache-dir -e '.[dev]'
+          pip install --no-cache-dir -e './pcs-core/python'
+      - name: Verify PCS pin digests
+        env:
+          OVK_PCS_CORE_PATH: ${{ github.workspace }}/pcs-core
+        run: |
+          python -c "from ovk.assurance.pin import require_pcs_pin, verify_pin_digests, PCS_PIN_COMMIT; print(require_pcs_pin()); print(PCS_PIN_COMMIT); print(verify_pin_digests())"
+      - name: Assurance pytest
+        env:
+          OVK_PCS_CORE_PATH: ${{ github.workspace }}/pcs-core
+        run: pytest tests/assurance -q --tb=short
+      - name: PCS conformance suite
+        working-directory: pcs-core
+        run: pcs conformance run --suite verifier-assurance
+      - name: Ordinary surfaces still pass
+        run: |
+          python scripts/check_command_surface.py
+          python scripts/validate_capabilities.py
+          ovk check --changed-files examples/multi_surface/pr_combined.diff --output-dir .ovk-assurance-ordinary --advisory
diff --git a/.gitignore b/.gitignore
@@ -45,3 +45,21 @@ ovk/package_data/
 .vscode/
 *.swp
 *~
+
+# Local verifier-assurance / baseline scratch (never ship)
+.ovk-va00-*/
+.ovk-va00-*.txt
+.ovk-assurance-*/
+.ovk-va-*/
+.ovk-check-*/
+evidence-pack-*/
+tmp-assurance-*/
+**/evidence-pack-*/
+**/tmp-assurance-*/
+
+# Editor / local backup debris
+*.bak
+*.bak_*
+*.bak_check
+docs/**/*.bak*
+
diff --git a/README.md b/README.md
@@ -140,6 +140,9 @@ Copy a full consumer example: [`examples/github_workflows/external_consumer.yml`
 | **Agent server** (`ovk-mcp`) | Let coding agents run checks from their tool loop (`pip install '.[mcp]'`) |
 | **Templates** ([`templates/`](templates/)) | Reusable rules for common risks (100 included) |
 | **Benchmark** (`ovk bench`) | Measure regression on agent-style PR diffs |
+| **Assurance** (`ovk verifier …`) | Opt-in reproducible verifier runs with PCS-bound evidence packs ([docs/assurance/GUIDE.md](docs/assurance/GUIDE.md)) |
+
+Ordinary PR checks (`ovk check` / Action / MCP) stay the default. Assurance mode does not replace them and requires a resolved [pcs-core pin](docs/PCS_PIN.md).
 
 Agent repair walkthrough: [docs/AGENT_REPAIR_LOOP.md](docs/AGENT_REPAIR_LOOP.md)
 
@@ -184,6 +187,8 @@ Questions, ideas, or a first PR — you are welcome. See [docs/ARCHITECTURE.md](
 | Install locally or wire up CI | [INTEGRATION.md](docs/INTEGRATION.md) |
 | Tune strictness and checker selection | [POLICY.md](docs/POLICY.md) |
 | Understand checkers and fallbacks | [BACKENDS.md](docs/BACKENDS.md) |
+| Use opt-in verifier-assurance mode | [assurance/GUIDE.md](docs/assurance/GUIDE.md) |
+| See the PCS pin / merge gate | [PCS_PIN.md](docs/PCS_PIN.md) |
 | Run or extend the benchmark | [BENCHMARK.md](docs/BENCHMARK.md) |
 | Roll out on an external OSS repo | [EXTERNAL_PILOT_PLAYBOOK.md](docs/EXTERNAL_PILOT_PLAYBOOK.md) |
 | See current capabilities | [STATUS.md](docs/STATUS.md) |
@@ -197,12 +202,12 @@ Full index: [docs/README.md](docs/README.md)
 ## Repository layout
 
 ```
-schemas/      Shared JSON schemas for configs and evidence
-ovk/          Python package — CLI, routing, adapters
+schemas/      Shared JSON schemas for configs and evidence (OVK-owned; no PCS VA forks)
+ovk/          Python package — CLI, routing, adapters, optional assurance/
 templates/    100 ready-made property templates
-examples/     Passing and failing scenarios you can run today
+examples/     Passing and failing scenarios; examples/assurance/ for PCS packs
 benchmarks/   FormalPR-Bench cases and real PR diff corpus
-docs/         Guides, specs, and release notes
+docs/         Guides, specs, ADRs, and release notes
 ```
 
 ---

diff --git a/docs/ADAPTER_CONTRACT.md b/docs/ADAPTER_CONTRACT.md
@@ -122,3 +122,17 @@ Adapters must not:
 - generate evidence not bound to input digests;
 - allow an agent-authored PR to alter adapter trust settings without human review;
 - execute arbitrary untrusted commands outside the adapter sandbox.
+
+## Ordinary vs assurance adapters
+
+Ordinary adapters participate in `ovk check` / MCP / Action routing and emit OVK evidence bundles. Assurance-capable adapters are opt-in (`ovk verifier …`), advertise validated assurance sections in their capability manifests, and export PCS-bound profiles/results via a pinned `pcs-core` revision.
+
+Assurance-capable adapters must additionally:
+
+- fail closed on missing checkers (typed indeterminate, never a fabricated native pass);
+- refuse to upgrade guarantee class during normalization;
+- redact secrets before configuration snapshot / profile export;
+- keep mutation from overwriting production profiles;
+- never label ordinary `ovk.cache.v3` hits as assurance replay.
+
+Cedar and ordinary Lean `deterministic_fallback` are not assurance-capable. See [assurance/GUIDE.md](assurance/GUIDE.md), [assurance/ADAPTER_INVENTORY.md](assurance/ADAPTER_INVENTORY.md), and [PCS_PIN.md](PCS_PIN.md).
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
@@ -164,3 +164,20 @@ This directory becomes machine-readable memory for future agents.
 OVK is backend-neutral, but it is not semantics-neutral.
 
 A policy evaluation, bounded model check, SMT satisfiability query, TLA+ trace, Dafny proof, Verus proof, Lean theorem, and runtime monitor are different guarantee classes. OVK records those distinctions in every capability manifest and evidence object.
+
+## Verifier-assurance mode (opt-in)
+
+Distinct from ordinary `ovk check` / MCP / Action. Requires a resolved [PCS pin](PCS_PIN.md); missing pin or unknown schema versions fail closed for assurance paths only.
+
+```text
+ovk verifier describe | snapshot-config | run | replay | mutate | validate-evidence
+        ↓
+ConfigurationSnapshot → VerifierProfile.v1 (PCS)
+        ↓
+run_assurance → VerifierInvocationRecord.v1 + VerificationResult.v1 + evidence/
+        ↓
+replay → VerifierReplayReport.v1 (immutable; no production overwrite)
+mutate → VerifierMutationManifest.v1 (production_prohibition always true)
+```
+
+Assurance-capable backends live under `ovk/adapters/assurance/` and register only for the verifier registry (not ordinary lane routing). Ordinary `ovk.cache.v3` hits are never labeled as assurance replay. See [assurance/GUIDE.md](assurance/GUIDE.md) and [adr/0001-verifier-assurance-architecture.md](adr/0001-verifier-assurance-architecture.md).
diff --git a/docs/BACKENDS.md b/docs/BACKENDS.md
@@ -1,6 +1,6 @@
 # Backend Execution Guide
 
-OVK exposes a common evidence contract across ten formal-methods backends. Their execution depth is not uniform. This document is the authoritative statement of what each backend actually executes in v1.2.0 RC.
+OVK exposes a common evidence contract across ten formal-methods backends. Their execution depth is not uniform. This document is the authoritative statement of what each backend actually executes in the current `1.2.1` package line (ordinary mode). Assurance-capable backends are listed separately below and are opt-in via `ovk verifier`.
 
 ## Execution maturity
 
@@ -14,11 +14,26 @@ OVK exposes a common evidence contract across ten formal-methods backends. Their
 | `kani` | Deterministic Rust-harness contract evaluator | No | Native Kani execution is not implemented |
 | `dafny` | Deterministic proof-obligation contract evaluator | No | Native Dafny verification is not implemented |
 | `verus` | Deterministic verified-Rust contract evaluator | No | Native Verus verification is not implemented |
-| `lean` | Deterministic theorem-obligation contract evaluator | No | Native Lean checking is not implemented |
+| `lean` | Deterministic theorem-obligation contract evaluator | No | Native Lean checking is not implemented; ordinary adapter is **not** assurance_capable |
 | `alloy` | Deterministic relational-model contract evaluator | No | Native Alloy analysis is not implemented |
 
 A binary-presence or version probe is never labeled as native verification. Evidence artifacts record `used_native_binary`, the guarantee type, assumptions, and limits.
 
+### Assurance-capable backends (opt-in `ovk verifier`)
+
+These are separate from ordinary lane routing. See [assurance/GUIDE.md](assurance/GUIDE.md).
+
+| `backend_id` | Real checker | Guarantee class | Notes |
+|---|---|---|---|
+| `auth-state-predicate` | Exact predicate engine over declared state | observational | VA-06 |
+| `pytest-suite` | `python -m pytest` + junit | runtime_observed | VA-07 |
+| `opa-policy` | `opa eval` | certificate_checked | VA-08; missing opa → indeterminate |
+| `lean-pfcore` | `lean` / optional lake | formally_checked | VA-09; ordinary Lean fallback stays non-assurance |
+| `sql-state-diff` | SQLite digest diff | observational | VA-10 |
+| `model-judge` | Judge client (CI contract fake) | empirically_measured | VA-11; stochastic; no guarantee upgrade |
+
+Cedar is never assurance_capable in this programme.
+
 ## CI tiers
 
 ### Native execution required
@@ -51,7 +66,7 @@ TLA+, Kani, Dafny, Verus, Lean, and Alloy remain non-blocking integration surfac
 
 Capability manifests live under `adapters/*/capability.json` and are packaged with the wheel. They support intent/backend ranking and MCP capability discovery.
 
-In v1.2.0 RC, router output is advisory metadata. Core lane obligations still execute their lane evaluator, and the selected generic backend does not yet control compilation or execution. Evidence records `routing_enforced: false` until the backend-selection control plane is implemented.
+Lane routing may be **enforced** when `.verification/config.yml` enables it for a lane (`routing_enforced: true` on evidence). The default product path remains shadow/legacy-authoritative until adopters opt into enforced lane policy — see [CURRENT_RELEASE_STATUS.md](CURRENT_RELEASE_STATUS.md) and [POLICY.md](POLICY.md). Router metadata alone is never a substitute for recorded guarantee type, assumptions, and limits.
 
 ## Entry points
 

diff --git a/docs/CHANGELOG_VERIFIER_ASSURANCE.md b/docs/CHANGELOG_VERIFIER_ASSURANCE.md
@@ -0,0 +1,29 @@
+# Verifier-assurance changelog (OVK-VA-00…14)
+
+## Unreleased — verifier-assurance programme
+
+### Added
+
+- **VA-00:** ADR, baseline, adapter inventory, ordinary-vs-assurance freeze, PCS development pin.
+- **VA-01…05:** Optional assurance capability manifests, configuration snapshots, invocation/evidence packs, replay, typed mutations, `ovk verifier` CLI.
+- **VA-06:** `auth-state-predicate` — exact predicates over declared authoritative state materials.
+- **VA-07:** `pytest-suite` — real pytest runner; `runtime_observed` only.
+- **VA-08:** `opa-policy` — assurance-capable real `opa eval` (missing opa → indeterminate). Cedar excluded.
+- **VA-09:** `lean-pfcore` — real Lean/PF-Core surface; ordinary Lean `deterministic_fallback` remains non-assurance.
+- **VA-10:** `sql-state-diff` — SQLite offline before/after digests.
+- **VA-11:** `model-judge` — stochastic empirical judge with CI contract fake; cannot upgrade guarantee class.
+- **VA-12:** Cross-adapter 14-test conformance harness + `examples/assurance/` packs.
+- **VA-13:** Post-freeze adjudication importer with label isolation and audit events.
+- **VA-14:** Assurance guide, non-claims, threat-model / BACKENDS / ARCHITECTURE / adapter-contract notes, schema-index PCS pointer.
+- Aligned pin/docs/exporters with pcs-core OVK pin surface: `VerifierProfile.v1`, `VerificationResult.v1`, `VerifierInvocationRecord.v1`, `VerifierReplayReport.v1`, `VerifierMutationManifest.v1` at commit `fb588a41a7eab68064429e3c4dfb26c328b9863d`.
+- Assurance CI job (`tests/assurance` + PCS conformance + pin digest verify).
+- Adversarial secret redaction (value patterns, list recursion) and fail-closed timeout/missing-checker split in VA-12.
+
+### Compatibility
+
+- Ordinary `ovk check`, MCP, and GitHub Action contracts unchanged.
+- Pin identity for merge-to-main is **satisfied** at the documented pcs-core SHA ([PCS_PIN.md](PCS_PIN.md)). PyPI publish of pcs-core remains pending.
+
+### Non-claims
+
+See [assurance/GUIDE.md](assurance/GUIDE.md#non-claims).
diff --git a/docs/PCS_PIN.md b/docs/PCS_PIN.md
@@ -0,0 +1,140 @@
+# PCS pin for OVK verifier-assurance
+
+OVK pins portable verifier-assurance schemas from `pcs-core`. OVK never forks those schemas under `schemas/` or invents parallel `VerifierProfile` / `VerificationResult` types.
+
+## Gate status
+
+| Gate | Status |
+|---|---|
+| Development against this pin | **OPEN** |
+| Pin identity (merge-to-main for pin purposes) | **SATISFIED** — OVK pins committed pcs-core revision below |
+| PyPI / registry publish of pcs-core | **Pending** — optional extra still uses git/path until a versioned release ships |
+
+See [ADR 0001](adr/0001-verifier-assurance-architecture.md) for ownership and ordinary-vs-assurance doctrine.
+
+## Authoritative pin
+
+| Field | Value |
+|---|---|
+| Repository | `https://github.com/SentinelOps-CI/pcs-core` |
+| Commit SHA | `fb588a41a7eab68064429e3c4dfb26c328b9863d` |
+
+**Pinned commit:** `fb588a41a7eab68064429e3c4dfb26c328b9863d`
+
+This SHA is the merge commit of PR #26 on pcs-core (VA schemas + OVK pin-surface + conformance). Prefer the full SHA in CI and install URLs. Pin by SHA, not branch name. PyPI publish is still pending.
+
+**Important:** a sibling `../pcs-core` checkout on a newer `main` tip is **not** automatically valid for OVK. After pcs-core changes that remove or rename pin-surface schemas, `verify_pin_digests()` fails closed. Always install or check out the SHA above (or set `OVK_PCS_CORE_PATH` to that revision). Do not assume “latest pcs-core main” equals this pin.
+
+Install from the pin (until PyPI):
+
+```bash
+pip install "pcs-core @ git+https://github.com/SentinelOps-CI/pcs-core@fb588a41a7eab68064429e3c4dfb26c328b9863d#subdirectory=python"
+# or sibling editable:
+pip install -e "../pcs-core/python"
+```
+
+## Pin resolution order
+
+OVK resolves the PCS checkout root in this order:
+
+1. Environment variable `OVK_PCS_CORE_PATH` (preferred for CI)
+2. Environment variable `PCS_CORE_PATH`
+3. Sibling directory `../pcs-core` relative to the OVK repository root
+4. Installed `pcs-core` package (when a published wheel is available)
+
+If no pin root is found, assurance validation and PCS export integrity sealing fail closed.
+
+## Install options
+
+### Path / editable (local development)
+
+```bash
+# from open-verification-kernel
+pip install -e ".[assurance]"
+# or explicitly:
+pip install -e "../pcs-core/python"
+```
+
+Optional extra `assurance` in `pyproject.toml` documents the git commit pin. Sibling path remains the local fallback.
+
+### Future published pin
+
+When pcs-core releases a version that includes the VA schemas:
+
+```toml
+assurance = ["pcs-core==<published-version>"]
+```
+
+Update this document with the exact version and schema digests from that release, then record the pin in CI.
+
+## Artifact types (pinned names)
+
+| Artifact type | Schema path under pcs-core |
+|---|---|
+| `VerifierProfile.v1` | `schemas/VerifierProfile.v1.schema.json` |
+| `VerificationResult.v1` | `schemas/VerificationResult.v1.schema.json` |
+| `VerifierInvocationRecord.v1` | `schemas/VerifierInvocationRecord.v1.schema.json` |
+| `VerifierReplayReport.v1` | `schemas/VerifierReplayReport.v1.schema.json` |
+| `VerifierMutationManifest.v1` | `schemas/VerifierMutationManifest.v1.schema.json` |
+
+Shared definitions: `schemas/verifier_assurance.defs.json`.
+
+`VerificationResult.v1` is distinct from `VerificationResult.v0`. Do not auto-upgrade.
+
+Field-shape notes (do not invent local forks):
+
+- Profiles use `verifier_profile_id` and nested `configuration.*_digest`, plus `integrity.{canonicalization_version,artifact_digest}`.
+- Results use `decision` (`accept` / `reject` / `indeterminate_*`) and `execution_status`.
+- Digests are `sha256:` + 64 lowercase hex. Integrity is nested; top-level `signature_or_digest` is forbidden on VA roots.
+
+## Schema digests at pinned commit
+
+Recorded against pcs-core commit `fb588a41a7eab68064429e3c4dfb26c328b9863d` (2026-07-24). Schema file digests (SHA-256 of file bytes):
+
+| Schema file | Digest |
+|---|---|
+| `VerifierProfile.v1.schema.json` | `sha256:a657a63eee47a00419f31008f0adee5559e37fdba2544831e8b297c0a2dbe9bd` |
+| `VerificationResult.v1.schema.json` | `sha256:146534a7ebf8ee8cdaecaa57258c0ce11224f50aed1a71196bc7b72d2c5b6d17` |
+| `VerifierInvocationRecord.v1.schema.json` | `sha256:3ee1384cd5fae5e08b87870100609a9a9b8cf2502b2c4d92de9dedc1f9ffbc3d` |
+| `VerifierReplayReport.v1.schema.json` | `sha256:06660ef51c89385869306c2f1c7f1364bec129b783007cc7a8caa4322582bd3b` |
+| `VerifierMutationManifest.v1.schema.json` | `sha256:b82952c1d41ddd151cd71440a5a38f7e768c468c3ff4ae11f3a80325d4cb4819` |
+| `verifier_assurance.defs.json` | `sha256:c417accb1b4bc08d6e6f0f98e71ee6e7c87a923d19c5054a18841e7e04eadabb` |
+
+Recompute digests after any pcs-core schema change:
+
+```bash
+python -c "from pathlib import Path; from hashlib import sha256; root=Path(r'../pcs-core/schemas');
+files=['VerifierProfile.v1.schema.json','VerificationResult.v1.schema.json','VerifierInvocationRecord.v1.schema.json','VerifierReplayReport.v1.schema.json','VerifierMutationManifest.v1.schema.json','verifier_assurance.defs.json'];
+[print(f, 'sha256:'+sha256((root/f).read_bytes()).hexdigest()) for f in files]"
+```
+
+Unknown schema versions and missing pin roots fail closed. Digests are enforced by `ovk.assurance.pin.verify_pin_digests()`.
+
+## Validation commands
+
+From a pcs-core checkout (or installed package with bundled schemas):
+
+```bash
+pcs schema check
+pcs validate examples/verifier_assurance/VerifierProfile.v1.valid.json
+pcs validate examples/verifier_assurance/VerificationResult.v1.valid.json
+pcs validate examples/verifier_assurance/VerifierInvocationRecord.v1.valid.json
+pcs validate examples/verifier_assurance/VerifierReplayReport.v1.valid.json
+pcs validate examples/verifier_assurance/VerifierMutationManifest.v1.valid.json
+pcs conformance run --suite verifier-assurance
+```
+
+From OVK (after pin resolution):
+
+```bash
+ovk verifier validate-evidence path/to/evidence/
+python -c "from ovk.assurance.pin import require_pcs_pin, verify_pin_digests; print(require_pcs_pin()); verify_pin_digests()"
+```
+
+## Dependency for assurance
+
+Assurance CLI (`ovk verifier …`) and PCS export/validation require a resolved pin. Ordinary `ovk check` / MCP / Action paths do not require pcs-core.
+
+## Non-claims
+
+Pinning PCS schemas does not assert checker correctness. Profiles and results bind digests and decisions only. See pcs-core `docs/verifier-assurance/non-claims.md` and ADR 0001 exclusions. PyPI publish of pcs-core remains a separate release step and is not implied by this pin.