Verification infrastructure for agentic AI
AI agents now approve payments, change permissions, and touch production systems. Onyx stands between an agent and the systems it reaches: every high‑stakes action is checked against your policies by a deterministic proof engine — and every decision ships with a certificate your auditors can re‑check without trusting the engine, the vendor, or the model.
The gap
Every agent stack can tell you what the model said. Almost none can prove that what the system did was allowed. When a regulator, a customer, or your own board asks “who checked that?” — a transcript of tokens is not evidence. Onyx is the missing evidence layer, in three verbs:
Gate
Each consequential action — a tool call, a transaction, a permission change — is decided against your policies: Cedar, Rego, XACML, or custody-style transaction rules. The verdict isn’t a rules-engine evaluation; it’s a theorem, proved fresh every time. Drops into agent stacks as an MCP server.
Verify
Onyx answers questions over all requests, not one: can any request matching X ever be permitted? Can a single signer ever move funds? Do these two policy sets agree? A violation returns a concrete counterexample; a pass returns a certificate.
Attest
Every decision lands in a hash-chained audit trail. Edit, delete, or reorder a record and the chain breaks — loudly. One command re-checks every certificate in the trail, offline, months later, using nothing but the standalone checker.
Under the hood
Onyx’s architecture is the old, hard discipline of proof engineering applied to a new problem. The searching machinery can be arbitrarily clever, because none of it has to be trusted — only the checker does.
Policies, claims, and requests compile to one precise graph structure — the same structure your auditors later see drawn as a picture, not a wall of symbols.
A deterministic engine derives the decision with a fixed set of sound rewrite rules, plus certificate-producing procedures for arithmetic, arrays, bitvectors, and equality.
Premise, every rewrite, conclusion — packaged as one self-contained artifact. Nothing about the certificate requires our software’s goodwill to interpret.
Replay, no search. The trusted base is the checker, not the solver — so you don’t trust Onyx’s cleverness, ours, or the model’s. Anyone can re-run it, any time.
Every inference rule Onyx uses is proved sound in two independent, industry-standard proof assistants, and Onyx derivations re-check move-for-move inside both. Not our test suite — kernels we don’t control.
Where it fits
Onyx ships as an MCP server: agents call the gate before consequential tool calls, decisions come back proved and fail-closed, and the compliance team gets a tamper-evident trail they can re-verify without asking engineering.
Onyx speaks custody transaction-policy JSON — ordered rules, first match, quorum approvals — and proves properties like “no single signer can ever move funds,” with a certificate per covered case and a concrete witness transaction when the property fails.
For Cedar, Rego, and XACML estates: safety assertions over all requests, equivalence between an old and a refactored policy set, dead-rule detection — each answer carrying a counterexample or a certificate, never a shrug.
Onyx independently re-derives proofs from cvc5, veriT, E, and Vampire step by step — including the steps the solver itself marked “trust” — so a formal-methods pipeline doesn’t rest on any single tool’s say-so.
Measured, not marketed
Onyx is a verification and audit reasoner for the decidable, policy-scale fragment — it is not a general-purpose theorem prover, and we say so. A public capability ledger records what it proves, what it declines, and the measured limits. When Onyx can’t decide, it says undetermined — it never guesses.
A private demo suite runs the real engine in your browser: live policy gating, certified verification, a real audit trail with a tamper caught on screen, and a solver proof re-checked end to end. Ask us for access — it takes ten minutes and no installation.
Charter program
We’re selecting design partners: teams with a real audit, verification, or governance problem, who want to shape what gets built and can speak to it when it works.