CAIN-42 CAIN Studio

CAIN-42 · Authority Notary v3

The layer between an AI agent
and the real world.

CAIN-42 is a Byzantine trust fabric. The Authority Notary is its independent verification surface: six checkable layers that answer who authorized this, may it proceed, is the agent's world still true, did the effect match the authorization, and can a stranger prove it without trusting us. A quorum co-signing is never an authorization.

Notary, not firewallAn enforcer cannot credibly certify itself. This one only refuses.
Offline verifiableOne signed record, one zero-dependency verifier, one browser tab.
Bounded proofL2's decision algebra is proved with Z3. The Lean 4 theorem is pending and labelled so.

Six layers, six refusals

Each layer can only say no. The stack is AUTHORIZED only when every layer is, and a missing layer is named rather than assumed to pass.

loading the live layer descriptors…

Try it against the live engine

These buttons call the real routes on this host. Both outcomes are shown on purpose: a notary that only ever says yes is a rubber stamp.

L2 · Admission — the same call, once with history and once with a forbid.

not run yet

L4 · Intent ↔ effect — the authorized transfer, then the same transfer with the payee and the amount widened past the mandate.

not run yet

L1 · Delegation — the committed two-hop chain, then the same chain with the leaf's capability widened to admin:*.

not run yet

L3 · Co-signed state — the committed three-checkpoint chain, then the same chain with one verified fact rewritten.

not run yet

Verify it yourself, offline

The bundle ships its own verifier. It imports no CAIN code and re-derives every verdict instead of reading our ok flags.

pip install cryptography
curl -O https://cainstudio.online/notary/v3/evidence/bundle
curl -O https://cainstudio.online/notary/v3/evidence/verifier.py
python3 verifier.py bundle --pinned-pub <the key you pinned>

The capability matrix — what is real, and what is not

Every subsystem in the published architecture, graded from the tree rather than from a document. A row is REAL only when production code exists and a test exercises it. This is the page that makes the marketing copy auditable.

loading the matrix…

What is proved, and what is not

ClaimStatusBasis
L2 decision algebra is correct and fail-closedPROVED (bounded)Z3, five theorems, UNSAT of every counterexample
L2 evaluator ↔ independent Lean semanticsPENDINGLean 4 is not installed on the build host; not claimed
L1 chain only narrows, offlineTESTEDPEDIGREE/APS/AIP/WIMSE invariants, adversarial tests
L3 state is tamper-evident and divergence is localisedTESTEDper-tenant SHA-256 chain, rewrite and gap tests
L4 effect stays inside the mandateTESTEDwidening, budget, replay, expiry and settlement tests
L0 quorum is equivocation-resistantTESTEDN=4, Q=3, Sybil and equivocation tests
Third-party audit / SOC 2 / customer runNOT METsame-operator evidence only
Honest limits. L0 is a verifiable local quorum with the production arithmetic, not a claim that the production cluster is fault-free. L4 is a conformant local profile of AP2's open-mandate idea, not AP2 certification. The Lean 4 equivalence proof is pending. Nothing here grants authority, and a quorum co-signing is not an authorization. Same-operator evidence; no third-party audit.