certior 0.1.0a1

Verified safety layer for AI agent tool calls - capability, content, and budget gates with signed certificates and a Lean-checked policy model

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 against a Lean-proven 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.

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 -> signed receipt in guard.audit_log
                                   # capability escalation -> raises CertiorBlocked

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:

Gate	Checks
Capability	child agent's capabilities ⊆ parent's; tool requires only what's granted
Content	HIPAA / SOX / attorney-client / custom detectors on prompts and outputs
Budget	per-agent hard ceiling; every step debits the parent

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

Framework	Module	Guide
OpenAI tool use	certior.adapters.tool_use	docs.certior.io/guides/openai
Anthropic tool_use	certior.adapters.tool_use	same recipe, native shape
LangChain	certior.adapters.langchain	docs.certior.io/guides/langchain
CrewAI	certior.adapters.crewai	docs.certior.io/guides/crewai
OpenClaw	certior.adapters.openclaw	docs.certior.io/guides/openclaw
MCP / custom	@guard.wrap(...)	docs.certior.io/guides/custom-loop

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: [e-mail]