Certior

Provable boundaries for multi-agent AI. A capability boundary for OpenClaw, LangChain, CrewAI, and your own delegation chains - every agent-to-agent call is checked by Z3 against a Lean-audited policy before it runs. Allowed calls return a signed receipt. Blocked calls raise CertiorBlocked with a precise reason.

Homepage: certior.io · Docs: docs.certior.io · Source: github.com/paulinebourigault/certior

Install

pip install certior

Requires Python 3.11 or later. Pulls in z3-solver, httpx, pydantic, jsonschema, and PyYAML.

Every tool call is enforced by Z3 against a policy model proven sound in Lean 4 offline. For live lattice-proven flow verification on every call, fetch the Lean binary on demand (not bundled in the wheel; ~90 MB, Linux x86_64 / macOS arm64):

pip install "certior[lean]"
certior-install-lean   # downloads + SHA-256-verifies the binary, fails closed on mismatch

Without it the runtime stays on the always-on Z3 path.

Quickstart

from certior import Guard, CertiorBlocked

guard = Guard(permissions=["network:http:read"])           # an agent's capability boundary

@guard.wrap(required_capabilities=["network:http:read"])   # tool calls + child agents must fit inside
def web_fetch(url): ...

web_fetch("https://example.com")  # allowed -> call runs, recorded in guard.audit_log
                                   # capability escalation -> raises CertiorBlocked
                                   # signed certificate of the decision: guard.verify(...).certificate

One decorator. Wraps any function. The rest of your code is unchanged.

Full 5-minute walkthrough: docs.certior.io/quickstart.

What it does

Three gates run before every tool call:

Allowed calls return a signed certificate bound to a Lean-checked policy fingerprint. Blocked calls raise CertiorBlocked with a precise reason. An auditor reproduces the audit with a single lake build.

See how it works and certificates for the runtime model.

Adapters

What is proven

Three formal tools, three jobs:

• Z3 runs on every tool call and proves the action satisfies capability, budget, and flow constraints.
• Lean 4 machine-checks the policy model (155 theorems and lemmas, 0 sorry, 0 axioms beyond Lean's standard three: propext, Classical.choice, Quot.sound). CI fails the build if any of the four headline guarantees - delegationSafety, ifcSoundness, compositionSoundness, SecurityLevel.isValidBoundedLattice - stops depending only on standard axioms.
• Dafny statically verifies kernel properties (path-safety, seccomp).

Certior does not verify the LLM's behaviour. It verifies the boundary the LLM operates inside.

Full assurance model: docs.certior.io/reference/trust-package.

Server, Studio, examples

The pip package is the SDK. The GitHub repository ships the FastAPI server, the Certior Studio UI, the Lean kernel, the GitHub Action, the certior-skill-audit CLI, and runnable examples:

• github.com/paulinebourigault/certior
• Server + Studio
• GitHub Action
• Skill audit CLI

Status

Alpha release, in active development under Apache-2.0. Public API may change between minor versions during the 0.x line; pin to certior==0.1.* for compatible updates.

Looking for design partners in healthcare, finance, legal, and regulated AI teams who need real audit trails on agent workflows.

Contact: hello@certior.io