Land v1.3.0-rc.1 adoption-surface program (OVK-PR1–PR9)

.github/workflows/ci.yml

@@ -49,6 +49,20 @@ jobs:
         run: python scripts/validate_templates.py
       - name: Validate adapter capabilities
         run: python scripts/validate_capabilities.py
+      - name: Validate adapter conformance
+        run: python scripts/validate_adapter_conformance.py
+      - name: Check capability tables are fresh
+        run: python scripts/render_capability_tables.py --check
+      - name: Check TCB document is fresh
+        run: python scripts/render_tcb_doc.py --check
+      - name: Verify RC DoD (in-repo)
+        run: python scripts/verify_rc_dod.py
+      - name: Verify RC install surface (Action SHA pins + metadata)
+        run: python scripts/verify_rc_install.py
+      - name: Check template claim registry is fresh
+        run: python scripts/build_template_registry.py --check
+      - name: Require SHA-pinned third-party actions in Action/release paths
+        run: python scripts/pin_action_shas.py
       - name: Score all benchmark cases
         run: python benchmarks/formal_pr_bench/score_all_lanes.py
       - name: Score expanded benchmark and publish leaderboard

.github/workflows/publish.yml

@@ -21,8 +21,8 @@ jobs:
     if: github.event_name == 'release'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-python@v5
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
         with:
           python-version: "3.12"
       - name: Install and verify release gates
@@ -58,7 +58,7 @@ jobs:
           /tmp/ovk-release-wheel/bin/ovk doctor
           /tmp/ovk-release-wheel/bin/python -c 'from ovk import mcp_server; from ovk.core.templates_cli import list_templates; assert len(list_templates()) >= 100; assert len(mcp_server.list_capabilities()["capabilities"]) >= 10'
       - name: Upload built distributions
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: ovk-dist
           path: dist/*
@@ -69,8 +69,8 @@ jobs:
     if: github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-python@v5
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
         with:
           python-version: "3.12"
       - name: Build package for Sigstore dry-run
@@ -83,7 +83,7 @@ jobs:
           python -m build
           twine check dist/*
       - name: Upload built distributions
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: ovk-dist
           path: dist/*
@@ -102,17 +102,17 @@ jobs:
       contents: write
       id-token: write
     steps:
-      - uses: actions/checkout@v4
-      - uses: actions/setup-python@v5
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0
         with:
           python-version: "3.12"
       - name: Download built distributions
-        uses: actions/download-artifact@v4
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
         with:
           name: ovk-dist
           path: dist
       - name: Install cosign
-        uses: sigstore/cosign-installer@v3.8.1
+        uses: sigstore/cosign-installer@d7d6bc7722e3daa8354c50bcb52f4837da5e9b6a # v3.8.1
       - name: Resolve certificate identity
         id: identity
         run: |
@@ -162,7 +162,7 @@ jobs:
               --git-ref "${GITHUB_REF}"
           fi
       - name: Retain cosign bundles
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: ovk-sigstore-bundles
           path: |
@@ -192,13 +192,13 @@ jobs:
       contents: read
       id-token: write
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
       - name: Download built distributions
-        uses: actions/download-artifact@v4
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
         with:
           name: ovk-dist
           path: dist
       - name: Publish to PyPI
-        uses: pypa/gh-action-pypi-publish@release/v1
+        uses: pypa/gh-action-pypi-publish@ba38be9e461d3875417946c167d0b5f3d385a247 # v1.14.1 (release/v1)
         with:
           password: ${{ secrets.PYPI_API_TOKEN }}

.github/workflows/repro-baseline.yml

@@ -0,0 +1,54 @@
+name: Repro baseline
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+jobs:
+  record:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+        python-version: ['3.10', '3.12']
+    runs-on: ${{ matrix.os }}
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python-version }}
+
+      - name: Sync package data and install
+        run: |
+          python -m pip install --upgrade pip
+          python scripts/sync_package_data.py
+          pip install --no-cache-dir -e '.[dev]'
+
+      - name: Record reproducible baseline
+        shell: bash
+        env:
+          PYTHONPATH: ${{ github.workspace }}
+        run: |
+          set +e
+          py_minor=$(python -c "import sys; print(f'{sys.version_info.major}.{sys.version_info.minor}')")
+          os_label=$(python -c "from scripts.record_repro_baseline import normalize_os_label; print(normalize_os_label())")
+          baseline="docs/baselines/repro-${os_label}-py${py_minor}.json"
+          python scripts/record_repro_baseline.py --skip-install --output "$baseline"
+          status=$?
+          set -e
+          python scripts/record_repro_baseline.py --validate-only "$baseline"
+          echo "recorder_exit=$status"
+          echo "baseline_path=$baseline" >> "$GITHUB_STEP_SUMMARY"
+          exit "$status"
+
+      - name: Upload baseline artifact
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: repro-baseline-${{ matrix.os }}-py${{ matrix.python-version }}
+          path: docs/baselines/repro-*.json
+          if-no-files-found: error

README.md

@@ -7,7 +7,7 @@
 [![License](https://img.shields.io/badge/license-Apache--2.0-blue.svg)](LICENSE)
 [![Python](https://img.shields.io/badge/python-3.10%2B-blue.svg)](pyproject.toml)
 [![FormalPR-Bench](https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/fraware/open-verification-kernel/main/docs/benchmarks/leaderboard-badge.json)](docs/benchmarks/latest-leaderboard-summary.json)
-[![Docs](https://img.shields.io/badge/docs-v1.2.1-green.svg)](docs/README.md)
+[![Docs](https://img.shields.io/badge/docs-v1.3.0--rc.1-green.svg)](docs/README.md)
 
 [Quick start](#quick-start) · [Add to CI](#github-actions) · [Contribute](#contribute) · [Documentation](docs/README.md)
 
@@ -30,6 +30,34 @@ flowchart LR
 
 ---
 
+## Public checkers
+
+<!-- BEGIN OVK_CAPABILITY_TABLE -->
+Public checkers from the normative capability registry (`adapters/*/capability.json`). Tables are generated by `scripts/render_capability_tables.py`.
+
+| Checker | release_status | claim_class | Native execution |
+|---|---|---|---|
+| `opa` | preview | policy_evaluation | yes |
+| `z3` | preview | smt_satisfiability | yes |
+| `cbmc` | preview | bounded_model_check | yes |
+| `cedar` | experimental | policy_evaluation | no |
+| `tla+` | experimental | bounded_model_check | no |
+| `kani` | experimental | bounded_model_check | no |
+| `dafny` | experimental | proof_obligation | no |
+| `verus` | experimental | proof_obligation | no |
+| `lean` | experimental | proof_obligation | no |
+| `alloy` | experimental | bounded_model_check | no |
+| `lane-authorization` | experimental | smt_refutation_search | no |
+| `lane-ci-secrets` | experimental | deterministic_witness | no |
+| `lane-deployment` | experimental | deterministic_witness | no |
+| `lane-infrastructure` | experimental | deterministic_witness | no |
+| `lane-self-protection` | experimental | policy_evaluation | no |
+
+Details and fallback rules: [docs/BACKENDS.md](docs/BACKENDS.md).
+<!-- END OVK_CAPABILITY_TABLE -->
+
+---
+
 ## Why this exists
 
 | Without OVK | With OVK |
@@ -119,14 +147,16 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: fraware/open-verification-kernel@v1.2.1
+      - uses: fraware/open-verification-kernel@v1.3.0-rc.1
         with:
           mode: advisory          # switch to strict when ready
           use-check: "true"       # analyze the PR diff automatically
           emit-check: "true"      # optional; requires checks: write
           post-comment: "true"    # requires pull-requests: write
 ```
 
+Pin target is `v1.3.0-rc.1` after the attributable tag exists. Until then, signed `@v1.2.1` remains the live production pin; see [docs/CURRENT_RELEASE_STATUS.md](docs/CURRENT_RELEASE_STATUS.md).
+
 Copy a full consumer example: [`examples/github_workflows/external_consumer.yml`](examples/github_workflows/external_consumer.yml)
 
 ---

action.yml

@@ -67,11 +67,14 @@ inputs:
     default: ovk-release-bundle
 
 outputs:
+  decision_state:
+    description: Normative DecisionState lattice member (allow, block, needs_review, unknown, error, skipped)
+    value: ${{ steps.set-outputs.outputs.decision_state }}
   recommendation:
-    description: Merge recommendation from the evidence bundle (allow, block, require_human_review, etc.)
+    description: Deprecated merge_recommendation alias (allow, block, require_human_review, etc.)
     value: ${{ steps.set-outputs.outputs.recommendation }}
   exit_code:
-    description: Process exit code implied by the recommendation (0 allow, 1 block, 2 require_human_review)
+    description: Process exit code implied by decision_state (0 allow, 1 block, 2 needs_review/unknown/error/skipped)
     value: ${{ steps.set-outputs.outputs.exit_code }}
   check_emitted:
     description: Whether a GitHub check run was successfully emitted
@@ -81,7 +84,7 @@ runs:
   using: composite
   steps:
     - name: Cache pip packages
-      uses: actions/cache@v4
+      uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
       with:
         path: ~/.cache/pip
         key: ovk-pip-${{ runner.os }}-${{ hashFiles('**/pyproject.toml') }}
@@ -365,22 +368,53 @@ runs:
             evidence_path = configured if configured.exists() else Path("ovk-evidence.json")
 
         recommendation = ""
+        decision_state = ""
         exit_code = "2"
         if evidence_path.exists():
             bundle = json.loads(evidence_path.read_text(encoding="utf-8"))
-            recommendation = str(bundle.get("decision", {}).get("merge_recommendation", ""))
+            decision = bundle.get("decision", {}) or {}
+            decision_state = str(decision.get("decision_state", "") or "")
+            recommendation = str(decision.get("merge_recommendation", "") or "")
+            if not decision_state and recommendation:
+                alias = {
+                    "allow": "allow",
+                    "block": "block",
+                    "require_human_review": "needs_review",
+                    "allow_with_warning": "needs_review",
+                    "require_stronger_check": "needs_review",
+                    "needs_review": "needs_review",
+                    "unknown": "unknown",
+                    "error": "error",
+                    "skipped": "skipped",
+                }
+                decision_state = alias.get(recommendation, "needs_review")
+            if not recommendation and decision_state:
+                alias = {
+                    "allow": "allow",
+                    "block": "block",
+                    "needs_review": "require_human_review",
+                    "unknown": "require_human_review",
+                    "error": "require_human_review",
+                    "skipped": "require_human_review",
+                }
+                recommendation = alias.get(decision_state, "require_human_review")
             exit_codes = {
                 "allow": 0,
-                "allow_with_warning": 0,
                 "block": 1,
+                "needs_review": 2,
+                "unknown": 2,
+                "error": 2,
+                "skipped": 2,
+                "allow_with_warning": 0,
                 "require_human_review": 2,
                 "require_stronger_check": 2,
             }
-            exit_code = str(exit_codes.get(recommendation, 2))
+            exit_code = str(exit_codes.get(decision_state or recommendation, 2))
 
         check_emitted = "true" if Path(".ovk-check-emitted").exists() else "false"
         github_output = os.environ["GITHUB_OUTPUT"]
         with open(github_output, "a", encoding="utf-8") as handle:
+            handle.write(f"decision_state={decision_state}\n")
             handle.write(f"recommendation={recommendation}\n")
             handle.write(f"exit_code={exit_code}\n")
             handle.write(f"check_emitted={check_emitted}\n")
@@ -405,7 +439,7 @@ runs:
         exit 2
     - name: Upload OVK artifacts
       if: always()
-      uses: actions/upload-artifact@v4
+      uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
       with:
         name: ovk-evidence-artifacts-${{ github.job }}
         path: |

adapters/alloy/capability.json

@@ -1,19 +1,56 @@
 {
   "capability_id": "alloy-relational-v1",
-  "tool": {"name": "alloy", "adapter": "ovk-adapter-alloy", "adapter_version": "0.1.0"},
+  "checker_id": "alloy",
+  "version": "0.1.0",
+  "implementation": "ovk-adapter-alloy",
+  "input_contract": "Alloy relational-model contract payload for authorization, infrastructure, or deployment topology.",
+  "output_contract": "ovk.result.v1 with instance counterexamples (deterministic evaluator today)",
+  "claim_class": "bounded_model_check",
+  "tool": {
+    "name": "alloy",
+    "adapter": "ovk-adapter-alloy",
+    "adapter_version": "0.1.0"
+  },
   "backend_class": "model_checker",
-  "input_languages": ["alloy"],
-  "supported_domains": ["authorization", "infrastructure", "deployment"],
-  "supported_property_kinds": ["invariant", "access_control", "forbidden_configuration"],
+  "input_languages": [
+    "alloy"
+  ],
+  "supported_domains": [
+    "authorization",
+    "infrastructure",
+    "deployment"
+  ],
+  "supported_property_kinds": [
+    "invariant",
+    "access_control",
+    "forbidden_configuration"
+  ],
   "guarantee": {
     "type": "bounded_model_check",
     "meaning_of_pass": "Alloy found no counterexample within scope.",
     "meaning_of_fail": "Alloy found a violating instance.",
     "meaning_of_unknown": "Alloy unavailable or model incomplete."
   },
-  "assumptions": ["Relational model captures relevant configuration."],
-  "limits": ["Finite scope analysis only."],
+  "assumptions": [
+    "Relational model captures relevant configuration."
+  ],
+  "trusted_components": [
+    "deterministic relational-model contract evaluator"
+  ],
+  "limits": [
+    "Finite scope analysis only."
+  ],
+  "failure_semantics": "Unavailable Alloy or incomplete model maps to unknown; evaluator errors map to error.",
+  "timeout_semantics": "unknown",
+  "timeout_behavior": "unknown",
+  "unsupported_semantics": "Native Alloy analysis is not implemented; finite scope analysis only under the deterministic evaluator.",
+  "determinism_status": "deterministic",
+  "release_status": "experimental",
+  "owner": "ovk-maintainers",
+  "native_execution": false,
   "result_format": "ovk.result.v1",
   "counterexample_format": "instance",
-  "timeout_behavior": "unknown"
+  "conformance": {
+    "suite": "conformance/manifest.json"
+  }
 }

adapters/alloy/conformance/CLAIMS.md

@@ -0,0 +1,9 @@
+# Adapter conformance claims
+
+## Pass establishes
+
+The deterministic Alloy model oracle reported no counterexample instances for the supplied fixture.
+
+## Outside the claim
+
+Native Alloy analysis is not implemented; does not prove properties outside the fixture model scope.