OC OpenCompliance
Technical Walkthrough

The architecture is a narrow verification pipeline.

OSCAL packages and typed evidence claims enter through deterministic ingestion. The classifier decides what may be proved, what must be attested, and what remains a human question. Lean 4 produces proof artifacts, not marketing prose.

10 core components in the current architecture slice
3 epistemic routes: proof, attestation, judgment
1 deterministic Verify surface for the user
0 room for hidden narrative overrides after the kernel
Core Principle

OSCAL outside, Lean inside

The external contract stays machine-readable and standards-aligned. OSCAL packages, profiles, mappings, and assessment-result style artifacts form the interchange layer. Lean 4 is the internal proof kernel for the decidable technical corridor.

This split matters. It avoids locking the product into an ad hoc private schema while still keeping the trusted core small and explicit.

Epistemic Model

Not every control is the same kind of thing

  • Decidable: controls expressible as propositions over inspectable system state.
  • Attestation: controls supported by signed human or institutional statements.
  • Judgment: controls whose adequacy depends on interpretation, governance, or review.
  • Mixed: controls decomposed into sub-obligations that take different routes.

Runtime components

1

Control Spec Library

Versioned Lean 4 modules encode the in-scope control corridor together with proof boundaries and source mappings.

2

OSCAL Bridge

Normalizes catalogs, profiles, mappings, and assessment-result style packages into the internal representation while rejecting unresolved references.

3

Evidence Claim Registry

Stores typed claims with actor identity, actor type, scope, timestamp, source system, signature state, and control mappings.

4

Control Classifier

Routes controls into proof, attestation, or judgment queues. It is the anti-magic layer that prevents ambiguous obligations from being mislabeled as machine-proven.

5

Proof Kernel Runner

Executes Lean proof batches, extracts unresolved axioms, and emits the trust-surface artifact for the verification session.

6

Verification Session

Presents one Verify API that returns either a deterministic certificate or a typed punch-list. No prose layer is allowed to overrule the kernel verdict.

7

Transparency Ledger

Appends canonical digests for evidence claims, proof bundles, certificates, witness receipts, and revocations so later mutation is publicly detectable.

8

Reproducible Witness Verifier

Reruns published bundles under pinned environments and only issues a witness receipt when the resulting digests match exactly.

9

Certificate Lifecycle Manager

Tracks drift, revokes stale certificates, and composes child certificates into larger trust artifacts when scope boundaries allow it.

10

Public Docs and Artifact Publishing

Explains the system honestly, exposes limitations, and exports allow-listed public bundles for docs, open specs, and example fixtures.

Plain-English Example

A single verification run

A company requests verification for a scoped profile. OpenCompliance ingests the relevant OSCAL profile, imports typed evidence from systems and attestations, classifies the resulting obligations, sends only the decidable corridor to Lean, then packages the result into a certificate or punch-list with a trust-surface report.

From there, the output can be signed, logged, replayed by witnesses, and revoked later if drift is detected.

LLM Boundary

Where language models are allowed

LLMs may help with bounded normalization of messy attachments into candidate claims. They do not get to decide verdicts, proof status, or publication safety. Any LLM-assisted step still terminates in deterministic schema checks and rule validation.

Architecture summary in one artifact chain

OSCAL profile
  -> normalized obligations
  -> typed evidence claims
  -> control classification
  -> Lean 4 proof batch
  -> trust-surface report
  -> certificate or punch-list
  -> canonical digest
  -> transparency entry
  -> witness replay receipt
  -> lifecycle drift and revocation