Enforcement you can prove.
Privacy you keep.

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.

Signed execution logs prove what ran and that the record was not altered. That is integrity of the log: it shows the record was not edited afterward, and shows nothing about whether it was honest in the first place. It also does not prove the agent action satisfied your policy, and the verifier still sees the log.

PreFlight proves compliance, not just execution: this action was checked against these rules and satisfied them. And the verifier learns only that, never the policy, the action, or which rule fired.

No, and the distinction is the whole product. An audit trail is a record the operator keeps about its own conduct. When your reviewer asks how they know the log is honest, an audit trail has no answer beyond "trust the operator." The receipt is different in kind: it is a piece of math an outside party can check, and if anyone tampered with the result, the check fails.

You are not being asked to take a vendor's word. Every decision comes with a receipt an independent party can verify, the same way your browser checks a bank's certificate millions of times a day: verification by proof rather than by promise. The math doing the checking is public and has been studied for years.

The framing we use internally: a record you produce about your own system is testimony. A receipt checkable against neutral math is evidence. Legal buyers tend to get that distinction faster than technical ones.

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.

Keep them if they are working. A policy engine can stop the action, but it cannot hand your auditor a proof that it did. The receipt is the part nobody else ships, and the proof is what unsticks the deal. We are the evidence layer, not a rip-and-replace.

Platform governance controls what gets built and who can deploy it: permissions, lifecycle, admin dashboards. PreFlight answers a different question: what did a deployed agent actually do, checked against your rules, provable to someone outside the platform. Your auditor, your client, and your regulator have no login to your platform, and the platform's own report about its own agents is self-attested by construction.

There is also a practical reason: no enterprise runs agents on one platform. PreFlight is a single enforcement layer that spans every stack your agents live on, which is something no platform's built-in governance can be by definition. Keep the platform. Put the proof in front of it.

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.

Scope is not a setting configured somewhere. It is declared on every check: each compiled rule set gets its own policy ID, and every check names which one to check against.

Say you have an NDA playbook, an MSA playbook, and a vendor-agreement playbook. Each compiles into its own ID. The NDA agent's checks pass the NDA policy, the MSA workflow step passes the MSA policy, and a renewal agent touching vendor paper passes the vendor policy. Scope follows whichever ID each agent or step is wired to. An account-wide baseline is the simple version of the same thing: compile one policy and have everything pass that ID. Most teams end up running both, a firm-wide baseline on every action plus a lane-specific policy on top.

The IDs carry versioning for free. When the legal team tightens a playbook, the new compile returns a new ID, and rollout or rollback is changing which ID an agent passes. No redeployment, no migration, and every receipt binds to the exact policy version in force when the action was checked.

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.

A receipt carries the proof itself, the policy hash that commits to the exact ruleset checked, the SAT or UNSAT outcome it attests to, and verification metadata. Verification time is independent of policy size, and the proof stays roughly constant-sized no matter how complex the rules are.

What it does not contain: no rule text, no documents, no agreement data. A counterparty can confirm the check happened and the rules were followed without ever seeing what the rules say. That absence is what makes a receipt shareable across a trust boundary in the first place.

One current limit, stated plainly: each hosted proof supports one public verification or one download, an anti-spam control, so the pattern is to verify or download shortly after generation. The authenticated status endpoint stays read-only and repeatable while the proof is hosted, and durable receipt archives are on the near-term roadmap.

Deterministic describes the decision: a rule decides instead of a model, and a gateway can stop the action before it runs. That is the right foundation, and several platforms now offer it.

Provable usually describes a record: the system logs that the rule fired, and that log is generated, held, and presented by the operator, inside the operator's own infrastructure. It answers the operator's question, not the reviewer's.

The question a regulated buyer actually asks is who can verify it without trusting the operator. Gateways can enforce and log. The receipt is the part a third party checks without access to the gateway, the operator, or the cloud it runs on: no API key, no account, on any stack, and without ever seeing your policy or your data.

Out of the checking, not out of the judgment. Verifying that an agent action satisfies a rule was never judgment work; it is the part a person does slowly, inconsistently, and, at agent volume, only by sampling. The solver does that part on every action, at the speed the agent works.

Humans keep the two jobs that were always theirs: writing the rules, and judging the exceptions. And exception routing is itself a rule you can write and enforce: agent actions above a threshold, off a playbook, or in a defined category are held for a person, and the hold is checked and receipted like everything else. You decide where the human sits. PreFlight makes that decision enforceable instead of aspirational.

PreFlight is an API. There is no infrastructure to stand up and no server to run. 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.

Yes. The PreFlight MCP server is live at api.icme.io/mcp with 14 documented tools covering checking, verification, and rule compilation. But enforcement is different from checking, because a tool an agent can call is a tool an agent can skip.

The block itself belongs in the execution path, at a hook where the action cannot proceed without a verdict. The MCP server makes PreFlight easy to adopt. The hook makes it impossible to bypass.

No. Every check runs three independent verifications: a local extraction model that evaluates extracted values against the compiled policy, an automated reasoning pass that independently translates the raw action text to formal logic, and a Z3 solver that formally checks the extracted values against the constraints. To approve, the paths have to agree. To block, one proof of a violation from any path is enough.

The rule is "proof of violation blocks," not "one engine wins." No path, including the LLM, can talk the system out of a proven violation. One documented nuance: an uncertain translation is not a proven violation, so if the extractor and the solver both confirm the action is allowed, the check can still clear.

Z3 came out of Microsoft Research and has been an industry-standard formal verification engine for close to twenty years. The translation methodology is adopted from AWS Automated Reasoning Checks (arXiv:2511.09008). Our contribution is wiring these in front of agent actions and adding the cryptographic receipt.

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

A vague term does not get silently interpreted. It gets flagged in testing so you can define it, or it produces an uncertain result and the action is treated cautiously. The solver enforces what the policy says; the tooling exists to make the policy say what you mean.

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 at runtime.

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

So there are two kinds of transparency. As the customer, you can open the hood any time and read the compiled logic and the values the system extracted. For outsiders, 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.

Scope is not a setting somewhere. It is declared on every check. Each compiled rule set gets its own policy ID, and every check names which one to check against. An NDA playbook, an MSA playbook, and a vendor playbook each compile to their own ID, and each agent or workflow step passes the one for its lane. A firm-wide baseline is just one more policy checked on every agent action alongside the lane-specific one.

Versioning comes free. Tighten the MSA playbook and the new compile returns a new version; rollout or rollback is changing which ID an agent passes. No redeployment, no migration. And every receipt binds to the exact policy version in force when the action was checked, which is what lets an auditor answer "which rules applied that day" precisely.

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.