Skip to content

Commit 3d56bcc

Browse files
committed
Document adoption-surface RC status and CI hooks.
Update roadmap, schema index, and root docs for v1.3.0-rc.1, and extend CI so conformance and RC gates run with the rest of the suite.
1 parent 9b89752 commit 3d56bcc

5 files changed

Lines changed: 71 additions & 10 deletions

File tree

.github/workflows/ci.yml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,20 @@ jobs:
4949
run: python scripts/validate_templates.py
5050
- name: Validate adapter capabilities
5151
run: python scripts/validate_capabilities.py
52+
- name: Validate adapter conformance
53+
run: python scripts/validate_adapter_conformance.py
54+
- name: Check capability tables are fresh
55+
run: python scripts/render_capability_tables.py --check
56+
- name: Check TCB document is fresh
57+
run: python scripts/render_tcb_doc.py --check
58+
- name: Verify RC DoD (in-repo)
59+
run: python scripts/verify_rc_dod.py
60+
- name: Verify RC install surface (Action SHA pins + metadata)
61+
run: python scripts/verify_rc_install.py
62+
- name: Check template claim registry is fresh
63+
run: python scripts/build_template_registry.py --check
64+
- name: Require SHA-pinned third-party actions in Action/release paths
65+
run: python scripts/pin_action_shas.py
5266
- name: Score all benchmark cases
5367
run: python benchmarks/formal_pr_bench/score_all_lanes.py
5468
- name: Score expanded benchmark and publish leaderboard

README.md

Lines changed: 32 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
[![License](https://img.shields.io/badge/license-Apache--2.0-blue.svg)](LICENSE)
88
[![Python](https://img.shields.io/badge/python-3.10%2B-blue.svg)](pyproject.toml)
99
[![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)
10-
[![Docs](https://img.shields.io/badge/docs-v1.2.1-green.svg)](docs/README.md)
10+
[![Docs](https://img.shields.io/badge/docs-v1.3.0--rc.1-green.svg)](docs/README.md)
1111

1212
[Quick start](#quick-start) · [Add to CI](#github-actions) · [Contribute](#contribute) · [Documentation](docs/README.md)
1313

@@ -30,6 +30,34 @@ flowchart LR
3030

3131
---
3232

33+
## Public checkers
34+
35+
<!-- BEGIN OVK_CAPABILITY_TABLE -->
36+
Public checkers from the normative capability registry (`adapters/*/capability.json`). Tables are generated by `scripts/render_capability_tables.py`.
37+
38+
| Checker | release_status | claim_class | Native execution |
39+
|---|---|---|---|
40+
| `opa` | preview | policy_evaluation | yes |
41+
| `z3` | preview | smt_satisfiability | yes |
42+
| `cbmc` | preview | bounded_model_check | yes |
43+
| `cedar` | experimental | policy_evaluation | no |
44+
| `tla+` | experimental | bounded_model_check | no |
45+
| `kani` | experimental | bounded_model_check | no |
46+
| `dafny` | experimental | proof_obligation | no |
47+
| `verus` | experimental | proof_obligation | no |
48+
| `lean` | experimental | proof_obligation | no |
49+
| `alloy` | experimental | bounded_model_check | no |
50+
| `lane-authorization` | experimental | smt_refutation_search | no |
51+
| `lane-ci-secrets` | experimental | deterministic_witness | no |
52+
| `lane-deployment` | experimental | deterministic_witness | no |
53+
| `lane-infrastructure` | experimental | deterministic_witness | no |
54+
| `lane-self-protection` | experimental | policy_evaluation | no |
55+
56+
Details and fallback rules: [docs/BACKENDS.md](docs/BACKENDS.md).
57+
<!-- END OVK_CAPABILITY_TABLE -->
58+
59+
---
60+
3361
## Why this exists
3462

3563
| Without OVK | With OVK |
@@ -119,14 +147,16 @@ jobs:
119147
runs-on: ubuntu-latest
120148
steps:
121149
- uses: actions/checkout@v4
122-
- uses: fraware/open-verification-kernel@v1.2.1
150+
- uses: fraware/open-verification-kernel@v1.3.0-rc.1
123151
with:
124152
mode: advisory # switch to strict when ready
125153
use-check: "true" # analyze the PR diff automatically
126154
emit-check: "true" # optional; requires checks: write
127155
post-comment: "true" # requires pull-requests: write
128156
```
129157
158+
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).
159+
130160
Copy a full consumer example: [`examples/github_workflows/external_consumer.yml`](examples/github_workflows/external_consumer.yml)
131161

132162
---

docs/README.md

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# OVK Documentation
22

3-
Documentation for Open Verification Kernel (**v1.3.0-rc.1 candidate**; signed tag remains `v1.2.1`).
3+
Documentation for Open Verification Kernel (**v1.3.0-rc.1** in-repo RC; signed tag remains `v1.2.1` until attributable publication).
44

55
Use this index as the canonical entry point. Each guide covers one topic; cross-links replace duplicated content across files.
66

@@ -40,8 +40,10 @@ Use this index as the canonical entry point. Each guide covers one topic; cross-
4040
| [HOLDOUT_LABEL_SEPARATION.md](HOLDOUT_LABEL_SEPARATION.md) | Sprint 8 label-separated prediction/eval checklist |
4141
| [SOURCE_PROFILE_HARDENING.md](SOURCE_PROFILE_HARDENING.md) | Sprint 6 source-profile hardening scaffolding |
4242
| [ATTRIBUTABLE_PUBLICATION.md](ATTRIBUTABLE_PUBLICATION.md) | Sprint 10 rc.1 / v1.3.0 publication gate |
43+
| [TRUSTED_COMPUTING_BASE.md](TRUSTED_COMPUTING_BASE.md) | Reviewer TCB inventory (registry + Action/App) |
4344
| [EXTERNAL_PILOT_PLAYBOOK.md](EXTERNAL_PILOT_PLAYBOOK.md) | Advisory→strict rollout on external OSS repos |
4445
| [PILOT_CASE_STUDIES.md](PILOT_CASE_STUDIES.md) | In-repo pilot metrics and external pilot reporting |
46+
| [pilots/README.md](pilots/README.md) | Published advisory pilot reports (Python, JS/TS, infra) |
4547
| [AGENT_REPAIR_LOOP.md](AGENT_REPAIR_LOOP.md) | Counterexample-to-repair workflow for MCP agents |
4648
| [benchmarks/adoption-summary.json](benchmarks/adoption-summary.json) | Machine-readable adoption metrics (see [BENCHMARK.md](BENCHMARK.md) for field-name notes) |
4749

@@ -69,6 +71,7 @@ Use this index as the canonical entry point. Each guide covers one topic; cross-
6971

7072
| Document | Purpose |
7173
|---|---|
74+
| [RELEASE_NOTES_v1.3.0-rc.1.md](RELEASE_NOTES_v1.3.0-rc.1.md) | v1.3.0-rc.1 candidate changelog |
7275
| [RELEASE_NOTES_v1.2.0.md](RELEASE_NOTES_v1.2.0.md) | v1.2.0 changelog |
7376
| [RELEASE_NOTES_v1.1.0.md](RELEASE_NOTES_v1.1.0.md) | v1.1.0 changelog |
7477
| [RELEASE_NOTES_v1.0.0.md](RELEASE_NOTES_v1.0.0.md) | v1.0.0 changelog |
@@ -79,12 +82,14 @@ Use this index as the canonical entry point. Each guide covers one topic; cross-
7982
docs/
8083
README.md # this index
8184
CURRENT_RELEASE_STATUS.md # living adoption dashboard
85+
TRUSTED_COMPUTING_BASE.md # reviewer TCB inventory (OVK-PR9)
8286
STATUS.md # stable capability inventory
8387
RELEASE.md # maintainer guide + known limitations
8488
RELEASE_NOTES_v*.md # immutable per-version changelogs
8589
INTEGRATION.md # install and GitHub Actions
8690
LANES.md, BACKENDS.md, … # reference and operations guides
8791
ARCHITECTURE.md, … # design and specification
92+
pilots/ # published advisory pilot reports (OVK-PR8)
8893
benchmarks/ # committed leaderboard and adoption JSON
8994
templates/ # external pilot manifest template
9095
```

docs/ROADMAP.md

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,34 @@
11
# OVK Roadmap
22

3-
Current product positioning: **`v1.3.0-rc.1` candidate** (typed control plane post-dates signed `v1.2.1`). What OVK can do today: [STATUS.md](STATUS.md). Adoption status: [CURRENT_RELEASE_STATUS.md](CURRENT_RELEASE_STATUS.md). Authoritative program: [ENGINEERING_PROGRAM_2026-07-23_R2.md](ENGINEERING_PROGRAM_2026-07-23_R2.md).
3+
Current product positioning: **`v1.3.0-rc.1` in-repo release candidate** (package `1.3.0-rc.1`; typed control plane + adoption-surface program post-date signed `v1.2.1`). What OVK can do today: [STATUS.md](STATUS.md). Adoption status: [CURRENT_RELEASE_STATUS.md](CURRENT_RELEASE_STATUS.md). TCB: [TRUSTED_COMPUTING_BASE.md](TRUSTED_COMPUTING_BASE.md). Authoritative program: [ENGINEERING_PROGRAM_2026-07-23_R2.md](ENGINEERING_PROGRAM_2026-07-23_R2.md).
44

55
## Release history
66

77
| Version | Summary | Changelog |
88
|---|---|---|
9-
| v1.3.0-rc.1 (candidate) | Typed backend control plane; P0 trust PRs 1–9 in working tree; publication gates open | [DEEP_AUDIT_2026-07-23_R2.md](DEEP_AUDIT_2026-07-23_R2.md) |
9+
| v1.3.0-rc.1 (in-repo RC) | Adoption surface PR1–PR9: registry, lattice, evidence integrity, conformance, bench provenance, Action SHA pins, App alpha, pilots, TCB; live attributable tag pending | [RELEASE_NOTES_v1.3.0-rc.1.md](RELEASE_NOTES_v1.3.0-rc.1.md) |
1010
| v1.2.1 | Signed release on pre-control-plane commit; consumer pin baseline | [RELEASE_NOTES_v1.2.1.md](RELEASE_NOTES_v1.2.1.md) |
1111
| v1.2.0 | All five check types validated end-to-end; clearer GitHub Action outputs; example rollout workflows | [RELEASE_NOTES_v1.2.0.md](RELEASE_NOTES_v1.2.0.md) |
1212
| v1.1.0 | Realistic PR diff benchmark set; required native checker CI for OPA, Z3, CBMC, Cedar; external rollout guide | [RELEASE_NOTES_v1.1.0.md](RELEASE_NOTES_v1.1.0.md) |
1313
| v1.0.0 | Unified `ovk check`, five check types, ten backends, GitHub Action, benchmark suite | [RELEASE_NOTES_v1.0.0.md](RELEASE_NOTES_v1.0.0.md) |
1414

15+
## Completed in this working tree (OVK-PR1–PR9)
16+
17+
1. Normative capability registry + multi-OS repro baseline harness.
18+
2. DecisionState lattice with strict fail-closed truth tables.
19+
3. Evidence integrity envelope (digests / controlling findings).
20+
4. Seven-item adapter conformance; stable ⊆ conformant.
21+
5. FormalPR-Bench provenance, partitions, contamination guards, version manifest.
22+
6. Action hardening suite + immutable SHA pins for release-path third parties.
23+
7. GitHub App private alpha with required security controls.
24+
8. Three advisory pilot reports under `docs/pilots/`.
25+
9. RC metadata (`1.3.0-rc.1`), TCB doc, DoD + install verification scripts.
26+
1527
## What we are working on next
1628

17-
1. **Sprint 0 / attributable gates** — live CI, wheel smoke, Action dogfood, and workflow IDs on a non-`[skip ci]` SHA (P0 code PRs 1–9 already in working tree; see [ENGINEERING_PROGRAM_2026-07-23_R2.md](ENGINEERING_PROGRAM_2026-07-23_R2.md)).
18-
2. **Semantic template conformance v2** and source-profile hardening (Sprints 6–7).
19-
3. **Consumer validation on rc.1** and label-separated holdout (Sprints 8–9).
20-
4. **Attributable publication** of `v1.3.0-rc.1` then `v1.3.0` after the 18-condition gate (Sprint 10).
29+
1. **Attributable publication of `v1.3.0-rc.1`** — non-`[skip ci]` workflow IDs, signed tag, Publish/Sigstore, consumer remotes on the immutable pin ([ATTRIBUTABLE_PUBLICATION.md](ATTRIBUTABLE_PUBLICATION.md)).
30+
2. **Promotion path to `v1.3.0`** — after the 18-condition gate, consumer validation, and attributable holdout aggregates.
31+
3. Ongoing calibration of strict lanes on real diffs (advisory remains the default recommendation until attributable RC evidence exists).
2132

2233
## Not planned as product promises
2334

docs/SCHEMA_INDEX.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,8 @@ JSON schemas for OVK objects. See also [ARTIFACTS.md](ARTIFACTS.md).
3232
| [infrastructure.policy.schema.json](../schemas/infrastructure.policy.schema.json) | ovk.infrastructure.policy.v1 | policy configuration files |
3333
| [verification.config.schema.json](../schemas/verification.config.schema.json) | ovk.config.v1 | `.verification/config.yml` policy routing config |
3434
| [formal_pr_bench.leaderboard.schema.json](../schemas/formal_pr_bench.leaderboard.schema.json) | formal_pr_bench.leaderboard.v1 | `ovk bench --leaderboard` |
35-
| [pilot.report.schema.json](../schemas/pilot.report.schema.json) | ovk.pilot_report.v1 | `ovk pilot --output report.json` |
35+
| [formal_pr_bench.manifest.schema.json](../schemas/formal_pr_bench.manifest.schema.json) | formal_pr_bench.manifest.v1 | `benchmarks/formal_pr_bench/manifest.v1.json` |
36+
| [pilot.report.schema.json](../schemas/pilot.report.schema.json) | ovk.pilot_report.v1 | `ovk pilot --output report.json`; published under `docs/pilots/*/pilot-report.json` |
3637
| [pilot.metrics.schema.json](../schemas/pilot.metrics.schema.json) | ovk.pilot_metrics.v1 | `scripts/collect_pilot_metrics.py --output pilot-metrics.json` |
3738
| [holdout.aggregate_metrics.schema.json](../schemas/holdout.aggregate_metrics.schema.json) | ovk.holdout_aggregate_metrics.v1 | FormalPR holdout aggregate metrics (labels never committed) |
3839
| [pilot.ledger.schema.json](../schemas/pilot.ledger.schema.json) | ovk.pilot_ledger.v1 | `docs/templates/pilot_ledger.example.json` (scaffolding) |

0 commit comments

Comments
 (0)