Roadmap

Build the narrow corridor first, then harden it in public.

The sequence matters. OpenCompliance is strongest if it goes from formal semantics to deterministic verification, then to tamper-evident artifact handling, and only after that to broader publication and continuous operation.

1

Semantics foundation

Publish the first open Lean 4 control-spec library, the three-tier control classification model, and a first exact-anchor review pilot for the SOC 2 Security plus ISO 27001 technical overlap corridor, then widen the public review layer to GDPR, IRAP, Cyber Essentials, NCSC CAF, NIST, and the first AI-governance frameworks without faking implementation that does not exist yet. That public review layer now reaches into the UK ICO AI guidance, NIST AI 600-1, NIST AI 100-4, NIST AI 700-2, and the first ETSI AI-security entries as well, while keeping the newer ISO AI standards honest as candidate layers instead of reviewed facts.

2

Typed legal semantics

Adopt LegalLean as the shared boundary vocabulary so proof, defeat, and judgment become typed values instead of prose only. The current corridor already has `FormalisationBoundary`-typed identity and logging results, a concrete risk-acceptance defeat path, a small `Vague` inventory, a first minimal-corpus solver, a public runtime layer whose decisions now drive every current public fixture, and a first versioned public verifier bundle that reruns the synthetic corridors outside the private monorepo. The remaining work is no longer basic runtime parity or bundle packaging; it is widening that typed path into a live-evidence verifier.

3

Evidence and interchange

Define the typed evidence-claim schema, actor ontology, and OSCAL-native ingest path for catalogs, profiles, mappings, and assessment-style artifacts.

4

Deterministic verification

Ship the Lean proof runner, trust-surface report, and single Verify flow that returns a certificate or typed punch-list for the same evidence every time.

5

Trust hardening

Add canonical artifact envelopes, signatures, transparency logging, reproducible replay bundles, and witness receipts for exact-match reruns.

6

Live evidence and lifecycle

Connect real evidence sources, track freshness, detect compliance drift, and handle certificate revocation or re-verification when state changes. The current synthetic lifecycle pack already demonstrates the fail-closed shape and the delta-recheck plan.

7

Public proof commons

Split docs, open specs, and public example fixtures into separate public bundles so the semantic layer can be inspected and reused in the open. The first stitched verifier bundle now exists inside the public examples surface, the current release line is rebuilt and smoke-checked through one scripted private release path before publication, and the public control library now also carries planned continuity, risk-governance, retention/deletion, facilities, supplier-commitment, ISMS-context, project-security, issue-resolution, outsourced-development, stakeholder-management, continual-improvement, compliance-inventory, intellectual-property, and remote-working branches while the live-evidence path matures.

Current Focus

First corridor first

The first milestone is intentionally narrow. Seed public corridors now exist for blocked, stale, certificate-eligible, cyber-baseline, and AI-governance ExampleCo runs, the public lifecycle pack now shows what happens after drift, the specs now include an exact-anchor review pilot that reaches across 56 public controls and 30 frameworks with 257 review entries, the Lean corridor now carries a LegalLean-backed typed boundary layer with runtime-consumed verdicts live across every current public fixture, and the Verify surface now includes a deterministic local HTTP/JSON API as well as the local CLI. The medium, issued, and cyber-baseline packs now also include the promoted access-review-export, password-policy, managed-WAF, centralized-monitoring, network-boundary, plaintext-transport, encryption-at-rest, unique-infrastructure-identity, segmentation, key-hygiene, locality, secure-baseline, update-hygiene, malware-protection, incident, repository-integrity, retention/deletion, supplier-commitment, reported-security-concern, and outsourced-development proof, attestation, or judgment wave, while the public ontology now also carries planned continuity, risk-governance, facilities, ISMS-context, project-security, stakeholder-management, continual-improvement, compliance-inventory, intellectual-property, remote-working, conduct, audit, support, intelligence, facility-workspace, and richer AI provenance/evaluation/data-quality branches with matching typed claim schemas. The new mapping-program files now make the remaining exact-anchor, claim, Lean, and fixture rollout work explicit instead of burying it in prose. That is the right shape: formalize a few defensible controls well before claiming broad framework coverage loosely.

Target Public Outputs

What others should be able to inspect

  • The open Lean 4 control-spec library and proof-boundary metadata.
  • The LegalLean-backed typed boundary layer for proof, defeat, and judgment.
  • The exact-anchor review pilot with public reviewed anchors, crosswalk-derived candidate anchors, and explicit blocker records.
  • Typed evidence-claim schemas and actor ontology documents.
  • Replayable proof bundles and example witness receipts.
  • The docs site that states the limits as clearly as the ambitions.

Longer-term goals

Goal 1

Open spec library

Make the standards-to-formal-language mapping reviewable and extendable in the open.

Goal 2

Deterministic verify loop

Ensure the same evidence package yields the same verdict and trust-surface output every time.

Goal 3

Continuous compliance

Move from one-shot runs to delta-triggered rechecks and revocable certificate lifecycles. The public next step is a live event stream and scheduled rerun path, not just static drift examples.