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, which is why placement matters. 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.

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.

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 and the protocols are peer reviewed.

Signing the log does not change that. Signed or transparency-logged records (the approach behind products like Traefik's Sovereign Trust Plane) prove the record was not altered after the fact, and some of these products also block before the action runs. But a signature proves who vouched for the decision, not that the check was computed correctly, and the verifier has to read the record to check it. A receipt proves the check ran correctly on that action against that policy, and the verifier learns the verdict and the policy hash without the record, the policy, or the data.

Products like EQTY Lab run the guardrail inside secure hardware and publish an attestation that it ran. That is a real improvement over a log. But the verifier has to trust the chip vendor's attestation keys, and in October 2025 researchers extracted or bypassed them in Intel, AMD, and NVIDIA confidential computing (WireTap, Battering RAM, TEE.fail). A PreFlight receipt has no hardware root to steal. The two approaches can be combined: hardware can vouch that the action description came from the real system, and the receipt proves the check on it was correct.

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.