AI agent verification with cryptographic proof.
Checked before the action runs.

Not by anything written in a document or a prompt. The solver has no context window and reads no instructions; it evaluates the proposed action against compiled logic and returns SAT or UNSAT. There is nothing in it to inject. Skipping the check is a separate question, and it is why placement matters: a tool an agent can call is a tool an agent can skip. As a pre-execution hook, the platform runs the check and the agent never chooses whether to be checked.

The LLM does one job: translating your policy into formal logic, once, at compile time. That output is inspected, checked for contradictions, and battle-tested against generated scenarios before anything goes live. At decision time a solver decides, and a solver cannot be talked around or fed a trick instruction. The probabilistic component never makes the allow-or-block call.

A locked workflow makes the steps repeatable, then hands your auditor a trace of what ran. That trace is a log. To trust it, the auditor has to trust that it was not edited, that nothing was omitted, and that your system produced it honestly.

PreFlight returns a proof instead of a trace. A third party verifies it without trusting you, and without seeing your policy or your data. Repeatable is good. Provable, and provable without disclosure, is the part a locked workflow does not give you.

Keep them; your buyers require them. But certifications verify the operator's controls, at the organization level, on an annual cycle. They say nothing about whether a specific agent action complied with a specific rule today. A certificate vouches for the company. The receipt vouches for the agent action.

There is also an evidentiary hierarchy here. The audit profession's own evidence standards rank independent external evidence above anything produced by the entity under review. A receipt verified by outside math sits in that top tier. A control report produced inside the system it vouches for does not.

It depends on how you deploy, and in two of the three models the question does not arise.

Pilot. A pilot uses your published policy and test actions. No client data is involved, so no vendor security review is needed to start.

Production in your own cloud account. The checkpoint runs inside your AWS account. Actions are checked and proofs are generated within your environment, and only the proof and verdict metadata reach ICME. ICME verifies your receipts and never holds client data, so SOC 2 is not applicable to us. Your cloud provider's certifications cover the infrastructure and your own controls cover the data.

ICME-hosted. SOC 2 becomes relevant only if you prefer that we host. In that case we run a single-tenant environment with private connectivity and encryption keys you hold and can revoke, and we meet your vendor security requirements before any client data moves.

The same receipt answers the underwriter. Carriers writing affirmative AI coverage now condition it on evidence that controls were enforced, and 2026 renewals are where the question lands; a receipt per action is that evidence, without opening your logs to the carrier.

Policies are built on facts present in the action itself: amount, recipient, destination. Text slipped into an email the agent read (a prompt injection) cannot change what the proposed action actually says. When PreFlight gates at the point of execution, the checked action is the executed action. The agent cannot move $10,000 while describing a $100 transfer, because the description is the transfer.

Correct, and we lead with it. SAT means the action satisfied your policy. It does not mean the policy was wise, or that the facts the action asserted are true. The receipt proves the rule fired against what the action claimed, which is accountability, not a safety guarantee.

What stalls a deployment is almost never "the agent might be suboptimal." It is "we cannot prove controls to risk and the regulator." Receipts solve that one, and that is the problem with a budget attached.

Then they still get the enforcement. The blocking decision comes from the solver consensus, not from the proof layer. So the worst case for a skeptic is "the guardrail still blocked the bad action, and the receipt is evidence I am choosing not to rely on yet."

The receipt adds verifiability on top of the safety. It does not carry the safety; that is the solver's job. A reviewer can adopt the evidence on their own timeline without the protection ever depending on it.

For the attorney or compliance owner who uses it day to day, there is nothing technical about it: they write plain-English if-then rules the way they would brief a new hire, and that is the entire authoring experience. Compilation and battle-testing run behind it. There is no separate interface to learn, so rules can be authored wherever your team manages policy today.

Two timings. Rules an attorney writes in their own words take minutes to compile, because the solver checks the whole set for contradictions and edge cases before anything governs a live action. Rules that range over fixed, known fields auto-generate in about two seconds. The first buys a version an attorney signed off on; the second is why per-customer setup at platform scale does not wait on a compile.

PreFlight is an API. By default there is no infrastructure to stand up and no server to run. For production in a regulated firm, the checkpoint can instead run inside your own cloud account so no client data leaves it. Either way it is cloud-neutral, and the receipt verifies on any stack, not just the one that produced it. A third party checks a decision against a single public endpoint, with no API key and no account.

No. Every check runs two independent verifications and reconciles them before returning a result: a custom LLM check that evaluates the action against the compiled SMT model of your policy, and a cloud reasoning engine that independently evaluates the same action against the same policy. A SAT result requires both to agree. If either returns UNSAT, the action is blocked.

So a single extraction error or a single reasoning gap cannot produce a false clearance, and no path, including the LLM, can talk the system out of a proven violation. The solver underneath is Z3, which came out of Microsoft Research and has been a standard formal verification engine for close to twenty years; the translation method is adopted from AWS Automated Reasoning checks (arXiv:2511.09008). Policies are also checked for internal contradictions at compile time, before they are saved.

The system surfaces ambiguity rather than quietly resolving it. At compile time, battle testing generates scenarios that expose a vague or wrong rule first. Before production, you can pull every extracted variable, its type, and its rule, and tighten a loose phrase. At runtime, an ambiguous term returns an uncertain result instead of a clean verdict, and the check resolves conservatively.

The runtime uncertain result is a backstop, not a workflow. If it appears in production, treat it as a signal to return to the policy, define the term, and re-run battle testing. A well-tested policy produces clean SAT and UNSAT verdicts.

Fully, as the customer. You can retrieve the original policy text, the compiled SMT-LIB, and the parsed rules at no charge, and export the SMT-LIB for your own tooling or an independent reviewer. Every check also returns the extracted variable bindings and the per-path results alongside the proof.

Outsiders get the other kind of transparency: the zero-knowledge receipt lets anyone confirm the decision was made correctly without seeing your rules and without trusting us. Your clients' reviewers verify the check ran; your policy stays private.

An audit trail is a record the operator keeps about its own conduct; when a reviewer asks how they know the log is honest, the only answer is to trust the operator. The receipt is a piece of math an outside party checks, and if anyone tampered with the result, the check fails. The verifier code is public, the protocols are peer reviewed, and a dishonest verifier would be caught by the first cryptographer who looked, which is the same reason banks trust TLS without reading its source.

A record you produce about your own system is testimony. A receipt checkable against neutral math is evidence.

Signing the log does not change that. A signed or transparency-logged record (the approach behind products like Traefik's Sovereign Trust Plane) proves the record was not altered after the fact, and the verifier has to read the record to check it. A receipt proves the rule was checked before the action ran, and the verifier learns the verdict and the policy hash without the record, the policy, or the data.

JOLT is a16z Crypto's open-source zkVM, and its README says it is in alpha and not yet audited. We disclose that plainly. The audit question is narrower than it looks, though. In a zero-knowledge system the property that protects you is verifier correctness, not whole-codebase perfection. A correctly implemented verifier rejects a cheating prover, so a bug or bad actor on the proving side produces a rejected proof, not a false one.

The verifier is the small, inspectable, open-source component, and it implements peer-reviewed protocols (JOLT, IACR ePrint 2023/1217, with our zkML layer in JOLT Atlas, arXiv:2602.17452). You do not need to inspect it personally; the assurance comes from the fact that anyone can. A dishonest verifier would be caught by the first cryptographer who looked, and cryptographers do look, which is the same reason banks trust TLS without reading its source. Compare that to a proprietary log format, where nobody outside the vendor can check anything.

Two scoping points: enforcement does not depend on JOLT at all, since the fail-closed blocking comes from the solver consensus above, and the upstream verification work is public and trackable at github.com/a16z/jolt rather than promised, including its Z3 verifier component. We hold ourselves to the same disclosure discipline we recommend to buyers: verify the small thing that matters, disclose the maturity of the rest. If a16z publishes audit results, we will surface them.