1
Semantics foundation
Publish the first open Lean 4 control-spec library and the three-tier control classification model for the SOC 2 Security plus ISO 27001 technical overlap corridor.
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.
2
Evidence and interchange
Define the typed evidence-claim schema, actor ontology, and OSCAL-native ingest path for catalogs, profiles, mappings, and assessment-style artifacts.
3
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.
4
Trust hardening
Add canonical artifact envelopes, signatures, transparency logging, reproducible replay bundles, and witness receipts for exact-match reruns.
5
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.
6
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.
Current Focus
First corridor first
The first milestone is intentionally narrow. Seed public corridors now exist for blocked and certificate-eligible ExampleCo runs, and the public lifecycle pack now shows what happens after drift. 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.
- 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.