Open Proof Layer

Compliance should say what it proves.

OpenCompliance is an OSCAL-native, Lean 4 proof-carrying compliance engine. It treats technical controls as theorems when they really are theorems, treats human attestations as signed claims when they are not, and keeps judgment-heavy controls explicit instead of hiding them behind green checks.

Kernel Lean 4 proofs for the narrow technical corridor.
Wire Format OSCAL packages and mappings as the external contract.
Evidence Typed claims with signer, scope, freshness, and provenance.
Outcome Deterministic certificates, punch-lists, and a trust-surface report.
Product Pitch

The short version

OpenCompliance is a proof-carrying compliance engine, not a checklist dashboard. It ingests controls and evidence, routes each obligation into proof, attestation, or human review, then returns either a certificate or a typed punch-list together with a trust-surface report that states exactly what was proved, assumed, attested, excluded, or deferred to judgment.

The point is not maximal automation. The point is epistemic honesty with better artifacts.

Why This Matters

The industry problem

Most compliance tooling collapses very different kinds of reasoning into one dashboard status. A runtime proof, a stale screenshot, a manually uploaded PDF, and a partner attestation often end up looking identical in the UI.

OpenCompliance tries to break that habit by making the boundary between proof and assertion visible and machine-readable.

What happens when a company presses Verify?

Step 1
Ingest the corridor

OpenCompliance imports the target control profile and the matching OSCAL mappings for the in-scope corridor.

Step 2
Collect typed evidence

Machine evidence, human attestations, and exclusions are stored as typed claims with signer, scope, source, freshness, and control mappings.

Step 3
Classify each obligation

Every control is routed into one of four buckets: decidable, attestation, judgment, or mixed.

Step 4
Run Lean 4 on the technical slice

Only the decidable corridor enters the proof kernel. The system extracts unresolved axioms rather than hiding them.

Step 5
Bind the output to artifacts

Proof bundles, certificates, and revocations become signed artifacts with canonical digests that can be logged and replayed later.

Step 6
Return a clear verdict

The output is a certificate or typed punch-list plus a trust-surface report saying what is proved, attested, judgment-dependent, or out of scope.

Trust Surface

Proof is only one layer

The product’s signature artifact is the trust-surface report. It is a machine-generated summary of what the compliance result rests on.

Tamper Evidence

Shortcut-proof by construction

The system should make it difficult to jump from messy internal state to a public certificate without leaving a signed, append-only, replayable trail.

Open Commons

Build the semantic layer in public

The public value is not just the UI. It is the open mapping corpus, typed evidence model, proof boundaries, and replayable examples others can inspect and improve.

Explicit limitations

Boundary

OpenCompliance does not replace licensed CPA firms, ISO certification bodies, or internal human judgment. It improves the quality, structure, and inspectability of evidence that those parties review.

Physical controls, policy adequacy, board oversight, and other normative questions remain partly or wholly attestation-driven or judgment-driven.

MVP Corridor

The initial scope is deliberately narrow: the technical overlap corridor between SOC 2 Security and ISO 27001. Access-control invariants, MFA enforcement, repository protections, CI policy guarantees, cryptographic settings, and similar inspectable controls come first.

Read by angle

Architecture

The runtime pipeline, components, and how proofs, attestations, and publication-safe artifacts fit together.

Open architecture
Trust Model

How signed artifacts, transparency logs, witness reruns, and fail-closed issuance make the system tamper-evident without blockchain.

Open trust model
Essay

Why an open, limitation-aware proof layer would move the compliance industry forward even before it solves every control.

Read the essay
Landscape

Where OpenCompliance overlaps with Ceel, Vanta, and Drata, and why the open-source proof layer still matters.

Open landscape
Examples

The public repos now carry blocked, stale-evidence, and successful synthetic ExampleCo corridors, persisted classification artifacts, raw source-export inputs, checked-in repo and CI verification claims inside the medium corridor, public transparency logs, a lifecycle drift pack, typed claims, signature manifests, scoped certificates or punch-lists, OSCAL-shaped projections, and replayable witness receipts.

Open examples
Lifecycle

See how a source change maps to impacted controls, triggers fail-closed revocation or re-verification, and blocks higher-level composition until trust is restored.

Open lifecycle
Foundation

Why the shared semantic layer should live in a neutral home, how sponsors fit in, and how the documents should be peer reviewed.

Open foundation