Welcome
ICME is the production implementation of two converging research breakthroughs in AI safety, formal verification and zero-knowledge machine learning, applied to AI agents that act in the real world.
The Research Foundation
Building on ARc
In 2025, researchers at Amazon Web Services published Automated Reasoning Checks (ARC) — a neurosymbolic framework that translates natural language policies into SMT-LIB formal logic and verifies agent actions using a mathematical solver. Their key result: 99%+ soundness on unseen adversarial datasets, a threshold unattainable by any LLM-based approach including ensemble methods and models with extended reasoning.
The core insight: use an LLM only to translate natural language to formal logic, a task it handles well, then hand the actual enforcement decision to a mathematical solver that has been proven correct. No confidence scores. No model judgment. A proof.
ICME's Novel Contribution
ARc solved enforcement. It did not solve verification at scale.
In our paper Succinctly Verifiable Agentic Guardrails With ZKP Over Automated Reasoning, we identify the missing layer: in a world of agentic commerce, where AI agents transact autonomously with each other at machine speed, you cannot require every participant to re-execute complex formal proofs to confirm that guardrails were followed. The verification cost becomes the bottleneck.
We solve this by wrapping the entire ARC enforcement pipeline in a zero-knowledge proof. The result is a single succinct cryptographic receipt that any machine can verify in under one second, without recomputing the underlying formal logic, without trusting the provider, and without revealing the policy itself. This is what makes trustless agentic commerce viable at scale.
What the two papers establish together
Natural language → formal logic
✓
✓
SMT solver enforcement
✓
✓
Soundness
99%+
99%+
Cryptographic proof of enforcement
✗
✓
Succinct verification (< 1 second)
✗
✓
Private policy
✗
✓
Trustless agent-to-agent verification
✗
✓
Designed for agentic commerce
✗
✓
How it works in practice
1. Write your policy in plain English No formal logic required. Write rules the way you would explain them to a colleague.
2. ICME compiles it to formal logic Your policy is formalized into SMT-LIB using the ARC approach. This happens once, offline.
3. Every agent action is checked against the solver When your agent attempts an action, it is translated into logical claims and verified against your policy model. SAT = allowed. UNSAT = blocked. Result in under one second.
4. Every decision is wrapped in a zero-knowledge proof A cryptographic receipt is generated for every enforcement decision — tamper-proof, independently verifiable by any machine, with your policy staying fully private.
5. Monitoring agents verify proofs autonomously No human in the loop, no re-execution of complex traces. Other agents verify the succinct proof instantly and respond automatically when a rule is broken.
bash
Response:
json
Jump right in
Last updated