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.
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.
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.
OpenCompliance imports the target control profile and the matching OSCAL mappings for the in-scope corridor.
Machine evidence, human attestations, and exclusions are stored as typed claims with signer, scope, source, freshness, and control mappings.
Every control is routed into one of four buckets: decidable, attestation, judgment, or mixed.
Only the decidable corridor enters the proof kernel. The proof bundle now records which proved claims actually entered the public Lean batch and which still sit outside that public proof boundary.
Proof bundles, certificates, and revocations become signed artifacts with canonical digests that can be logged and replayed later.
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.
The product’s signature artifact is the trust-surface report. It is a machine-generated summary of what the compliance result rests on.
The system should make it difficult to jump from messy internal state to a public certificate without leaving a signed, append-only, replayable trail.
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.
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.
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. The public fixture set now also includes dedicated synthetic cyber-baseline and AI-governance corridors, while the reviewed mapping pilot remains broader than the implemented proofs, covering public exact anchors across GDPR, IRAP, Cyber Essentials, NCSC CAF, NIST CSF 2.0, NIST SP 800-53, the EU AI Act, the EU GPAI Code of Practice, and NIST AI RMF, and keeping ISO AI standards at candidate status until licensed review exists.
The runtime pipeline, components, and how proofs, attestations, and publication-safe artifacts fit together.
Open architectureHow signed artifacts, transparency logs, witness reruns, and fail-closed issuance make the system tamper-evident without blockchain.
Open trust modelWhy an open, limitation-aware proof layer would move the compliance industry forward even before it solves every control.
Read the essayWhere OpenCompliance overlaps with Ceel, Vanta, and Drata, and why the open-source proof layer still matters.
Open landscapeThe public repos now carry blocked, stale-evidence, cyber-baseline, AI-governance, and successful synthetic ExampleCo corridors, persisted classification artifacts, a first mixed-control decomposition in the medium corridor, raw source-export inputs, boundary-aware proof-runner metadata, signed governance evidence, public transparency logs, a lifecycle drift pack, typed claims, signature manifests, scoped certificates or punch-lists, OSCAL-shaped projections, and replayable witness receipts.
Open examplesA company-level ExampleCo walkthrough now shows how a hypothetical team can aggregate four corridor results into one honest buyer-facing assurance story without overstating full-framework compliance.
Open showcaseSee 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 lifecycleWhy the shared semantic layer should live in a neutral home, how sponsors fit in, and how the documents should be peer reviewed.
Open foundationThe published project surface is organized under a single GitHub organization so people can inspect the site, specs, examples, schemas, validators, and Lean corridor directly.
Open GitHub orgIf you only read one page before diving into GitHub, read the repository map. It tells you which repo is normative, which repo is executable, and which repo is only explanatory.
Open repository mapThe public docs bundle, including the trust model, roadmap, publication plan, and repository map, lives in its own repo.
Open site repoArtifact contracts, mapping methodology, control-boundary metadata, exact-anchor review pilots, and versioning rules belong in the public specs repo.
Open specs repoThe ExampleCo corridors, lifecycle packs, witness receipts, transparency logs, and OSCAL-shaped projections are published as synthetic public examples.
Open examples repoThe public validator and conformance vectors are published separately so the examples and schemas can be checked rather than trusted by prose.
Open conformance repoThe public evidence envelope and claim-type payload schemas are published on their own so others can integrate or critique them independently.
Open schema repoThe public Lean package shows exactly what the current proof slice covers and, just as importantly, where the proof boundary stops.
Open Lean repo