> For the complete documentation index, see [llms.txt](https://docs.icme.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.icme.io/documentation/our-products.md).
# Our Products
ICME builds one thing: trust in AI systems that you can check instead of believe. Three products deliver it at three different points in an agent's life, and they answer three different questions.
**Verbatim Deterministic Gateway** answers: *can my agent say or do something my policy forbids?* It is a gateway wrapped around your own agent that makes hallucination and rule-breaking impossible by construction. The model picks the words; it never gets to invent the facts.
**PreFlight** answers: *was this action actually checked against the policy, and can a stranger verify that?* It translates natural-language policies into formal logic and verifies agent actions with an SMT solver. In production, the solve runs inside our zkVM, so every verdict carries a zero-knowledge receipt a counterparty can check in milliseconds, without re-running anything, without trusting the operator, and without seeing the policy.
**PreFlight Instruments** answers: *did anyone check the model for prompt injection before it sends output, and can they prove it?* A layered detection ensemble (an activation probe, a guard SLM, and a sparse autoencoder) works at the model level, reading the forward pass itself, and every scan ships with a zkML proof that the agreed detector ran on that exact input. Detection is probabilistic. The receipt is not.
***
#### Blocked is good. Unrepresentable is better.
Every agent-security product on the market intercepts actions the model already proposed. A checkpoint sits between the agent and the world, catches the bad proposal, and blocks it. That is the right instinct, and it is still one step too late.
**Grammar-constrained decoding enforces at proposal time: forbidden actions aren't blocked, they're unrepresentable.** Behind the Verbatim gateway, the model's output space is compiled from your policy before generation begins. An action the current session does not permit is not a string the model can produce, so there is nothing to intercept. The gate still runs behind it, as a second wall, but the first wall is the language itself.
This distinction is why the industry's most embarrassing failures cannot happen here. Agents delete files after acknowledging a "do not run" instruction. Agents refuse in text while executing the forbidden call in the same turn. Safety constraints silently vanish when a long context gets compacted. All three failures share one root: the constraint lived in the model's context, where the model can read it, lose it, or ignore it. Verbatim's constraints live in the grammar and the executor. There is nothing in context to compact away, "acknowledged but did it anyway" is impossible when the words and the actions are one validated program, and an instruction the attacker injects can influence which permitted option gets picked but cannot add a single word to the vocabulary of the possible.
***
#### The layer every framework is missing
The agent-security industry is converging on a four-layer architecture: observe your agent, enforce on your agent, evaluate your agent's trajectories, govern your agent's policies. Look at where all four layers live. Inside one operator's trust perimeter.
Every guarantee that architecture produces is a claim the operator makes about itself. The monitors are the operator's monitors. The enforcement logs are the operator's logs. When two agents from different companies transact, when a regulator asks for evidence, when a customer disputes an action, the strongest artifact the four layers can produce is "trust me, our guardrails ran." Reputation systems and audit trails paper over the gap, and both stop working at machine speed.
ICME builds the fifth layer: **prove**. Every product in this stack emits a receipt that verifies *outside* the operator's perimeter, with nothing but math. Verbatim's provenance and gate verdicts make the enforcement layer inspectable and, with its receipt layer, provable. PreFlight makes the policy check itself a zero-knowledge proof a stranger verifies in milliseconds, without seeing the policy. Instruments makes "the injection scan ran" a cryptographic fact instead of an operator's assertion. Observe, enforce, evaluate, govern, and then prove it to someone who has no reason to believe you.
***
#### At a glance
| | **Verbatim Deterministic Gateway** | **PreFlight** | **PreFlight Instruments** |
| ---------------------------- | ---------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------ |
| **What it is** | A deterministic gateway around your agent: grammar-constrained decoding, runtime gates, per-character provenance | Formal policy verification: natural language compiles to SMT logic, a solver renders the verdict, proven in ZK | Prompt-injection detection at the model level: the forward pass itself is read, and every scan carries a ZK proof it ran |
| **Core question** | Can the agent misbehave at all? | Did this action comply with the policy, provably? | Was the model checked before it acted, provably? |
| **When it acts** | At proposal time: forbidden output is unrepresentable, not intercepted | At action time, before a consequential action executes | Inside the model, before output leaves: activations and features are read wherever untrusted content enters context |
| **Guarantee type** | Correctness by construction: no path for an unverified fact or ungated action | Formal verdict: SAT/UNSAT against the policy model, cryptographically bound to the input | Process integrity: the agreed classifier ran, untampered, unskipped, on this exact input |
| **What stays probabilistic** | Which permitted option the model selects | Faithfulness of the natural-language-to-logic translation (mitigated by a redundant ensemble, 99%+ soundness) | The verdict itself: a 0.99 AUROC ensemble is strong, not certain |
| **Whose agent** | Yours: an appliance you deploy and own | Anyone's, including a counterparty's: wraps any agent's actions | Any self-hosted model; closed APIs expose no forward pass, so they get the text classifier only |
| **Granularity** | Every turn, every character of output | Consequential actions: purchases, transfers, commitments | One verdict and one proof per scan, at every untrusted boundary |
| **Proving cost** | Microseconds per token for enforcement; receipts prove a small deterministic core | About a second per action: production proves the SMT solve in ZK | 66 ms to prove, 10 ms to verify, on one CPU core |
| **Privacy** | Spec stays inside your perimeter; nothing leaves the box | Policy hiding: prove compliance without revealing limits, thresholds, or exception rules | Verdict travels, weights and inputs do not |
***
#### How to choose
Pick by where your risk lives. If the risk is *your own agent's mouth and hands* (a hallucinated fee, an over-limit transfer, an invented policy), that is Verbatim: prevention, not detection, on every turn. If the risk is *a consequential action crossing a trust boundary* (your agent buys from a stranger's agent, a regulator wants evidence, a counterparty wants assurance without seeing your policy), that is PreFlight: a formal verdict with a receipt that travels. If the risk is *poisoned content steering your model* (a hidden instruction in a webpage, a wallet-drain line in a tool response), that is Instruments: scan every boundary, keep the receipts.
#### Better together
The three compose into one trust chain, and they share one proving stack (Jolt for deterministic and solver execution, Jolt Atlas for model inference), so receipts from all three verify the same way.
An agent behind the Verbatim gateway cannot misspeak or act outside its spec. Content entering that agent's context arrives pre-scanned by Instruments, with proof the scan ran. And when the agent takes an action that touches money or another party, PreFlight renders a formal compliance verdict with a receipt the counterparty checks in milliseconds. Constrained inside, scanned at the borders, proven at the boundary where trust runs out. At no point in that chain does anyone have to take anyone's word for anything.
***
#### Get access
All three products are onboarding design partners now. If you are deploying agents where a wrong word, an unchecked action, or an unverified guardrail is unacceptable, reach out.
[Request access on X](https://x.com/wyatt_benno)
or
Email us at