icme-agt

ICME PreFlight as an external policy backend for the Microsoft Agent Governance Toolkit (AGT).

Made with ❤️ by ICME Labs. Not affiliated with or endorsed by Microsoft.

AGT's BackendDecision reserves two fields — proof_artefact and verification_pointers — for "high-assurance backends (SMT-verified gates, mechanised-proof PDPs, TEE-attested PDPs)". This package fills that slot: every decision is verified by ICME PreFlight's SMT solver against a plain-English policy and returns with a zero-knowledge proof that flows verbatim into AGT's tamper-evident audit trail.

• Tiered by design. AGT's evaluator consults external backends only when no YAML rule matches. Your deterministic rules stay the free, microsecond fast path; ICME is the semantic escalation tier at $0.01 per check.
• Semantic policies YAML can't express. AGT conditions compare a field to a constant. ICME catches role violations ("only the client agent can release payment"), field-vs-field comparisons ("no withdrawal exceeding the original payment"), and cross-fact conjunctions — reasoning formally over plain-English rules.
• Framework-authored action descriptions. The action string sent to ICME is serialized deterministically from AGT's execution context (real tool name, validated arguments) — never from the agent's self-report. A prompt-injected agent cannot launder its own description.
• Fail-closed, twice. In enforce mode this backend denies on any ICME outage — and it also sets BackendDecision.error, so AGT's own evaluator independently fail-closes (per AGT's #2992 semantics and ADR-0013).
• Zero runtime dependencies. Stdlib-only HTTP; agent-os is a peer, not a dependency.

Install

pip install "git+https://github.com/ICME-Lab/icme-agt.git@v0.1.0"

Quickstart

import os
from agent_os.policies import PolicyEvaluator
from icme_agt import ICMEBackend

evaluator = PolicyEvaluator()
evaluator.load_policies("policies/")            # Tier 1: deterministic YAML

evaluator.add_backend(ICMEBackend(              # Tier 2: proven semantics
    policy_id=os.environ["ICME_POLICY_ID"],     # from POST /v1/makeRules
    api_key=os.environ["ICME_API_KEY"],
    triggers={"release_payment", "file_dispute", "withdraw"},
))

decision = evaluator.evaluate({
    "agent_id": "freelancer-agent",
    "tool_name": "release_payment",
    "arguments": {
        "acting_role": "freelancer agent",
        "amount": 500,
        "original_payment": 500,
        "recipient": "the freelancer themselves",
        "dispute_active": False,
        "days_since_deposit": 3,
    },
})

print(decision.allowed, decision.reason)
print(decision.audit_entry["proof_artefact"])          # proof id
print(decision.audit_entry["verification_pointers"])   # publicly verifiable

Compile your policy once, in plain English (300 credits, one time):

curl -s -N -X POST https://api.icme.io/v1/makeRules \
  -H 'Content-Type: application/json' -H 'X-API-Key: YOUR_KEY' \
  -d '{"policy": "1. Only the client agent can release payment to the freelancer.\n2. Only the client agent can file a dispute.\n3. Only the freelancer agent can submit completed work.\n4. If a dispute is active, no agent can release payment.\n5. If more than 14 days have passed since the payment was deposited, no agent can file a dispute.\n6. No agent can release payment to any address other than the designated freelancer.\n7. No agent can withdraw more than the original payment amount."}'

Field-tested: a live five-act run

Output of examples/tiered_governance_demo.py against the live API, governing two escrow agents (a client agent and a freelancer agent) under the seven-rule policy above. Every proof ID below is real and independently verifiable — no ICME account required.

Escrow governance: AGT YAML (deterministic) + ICME PreFlight (proven)
ICME mode: LIVE (api.icme.io) | assurance: dual

Act 1 — routine escrow status check (outside `triggers` scope: no API call, no credit)
  -> ALLOWED: Tool 'get_escrow_status' is outside the ICME escalation scope; deterministic tier governs it.

Act 2 — emergency withdrawal attempt (Tier 1 YAML denies; ICME never consulted)
  -> BLOCKED: Deterministic tier: emergency_withdraw is always denied.
     decided by: escrow-tier1

Act 3 — client releases payment: no dispute, day 3, designated freelancer (SAT)
  -> ALLOWED: ICME PreFlight AR unavailable: Satisfiable [allowed under 'dual' assurance:
     result was 'AR unavailable' but llm and z3 each returned SAT] [verifiers: llm=SAT, z3=SAT]
     proof:  308ff908-32bd-47f1-acc7-4888abd41ed7

Act 4 — ROLE VIOLATION: freelancer agent releases the payment to themselves
  -> BLOCKED: ICME PreFlight UNSAT: Unsatisfiable
     (extracted: agentReleasingPayment=1; ...; originalPaymentAmount=500.0; withdrawalAmount=500.0)
     proof:  b8bdb869-dfd2-473c-8c0a-432289355ae5

Act 5 — FIELD-VS-FIELD: client withdraws $750 of an original $500 payment
  -> BLOCKED: ICME PreFlight UNSAT: Unsatisfiable
     (extracted: ...; originalPaymentAmount=500.0; withdrawalAmount=750.0)
     proof:  90c671fb-1a79-4d73-b887-b4a5002f6c67
     verify: https://api.icme.io/v1/proof/90c671fb-1a79-4d73-b887-b4a5002f6c67

Act 4 is a role violation: same tool, valid-looking arguments, wrong actor. Act 5 compares two fields (withdraw amount vs. original payment), which AGT YAML conditions — field / operator / CONSTANT — cannot express at all. Both were caught by formal reasoning, each with a verifiable proof in the AGT audit entry.

Run the same walkthrough yourself, fully offline (no API key, no credits, recorded responses):

python examples/tiered_governance_demo.py

Zero-risk on-ramp: shadow mode

Nothing blocks; verdicts, reasons, and proofs still land in the audit entry, and would-have-blocked actions are logged. Flip one argument to enforce.

ICMEBackend(policy_id=..., api_key=..., mode="shadow")

Offline demos and CI: ReplayTransport

Like AGT's own scripted MAF demos, everything here runs with no API key, no network, and no credits via recorded responses:

from icme_agt import ICMEBackend, ReplayTransport

transport = ReplayTransport(cassette="recorded.jsonl")   # or .stub(...)
backend = ICMEBackend("demo-policy", transport=transport)

Record a cassette from a live session with HTTPTransport(api_key=..., recorder="recorded.jsonl").

How a check flows

PolicyEvaluator.evaluate(context)
  ├─ YAML rule matches ──────────────────────────► decision (ICME never called)
  └─ no rule matched → ICMEBackend.evaluate(context)
       ├─ tool outside `triggers` ────────────────► allow (no API call, no credit)
       ├─ deny-cache hit (recent UNSAT retried) ──► deny (no API call)
       ├─ POST /v1/checkRelevance  (free)
       │    └─ zero policy variables matched ─────► allow (no paid call)
       └─ POST /v1/checkIt         (1 credit, SSE → final event)
            ├─ result SAT ────────────────────────► allow + proof_artefact + pointers
            ├─ result UNSAT ──────────────────────► deny  + proof_artefact + pointers
            ├─ uncertain (e.g. "AR uncertain",
            │  "AR unavailable") ─────────────────► per `assurance` (strict: deny)
            └─ error / outage ────────────────────► deny (fail closed; AGT's
                                                    evaluator fail-closes too)

ICME endpoint	Used for	Cost
POST /v1/checkIt	The verdict (SSE stream; transport returns the final event). Default.	1 credit ($0.01)
POST /v1/checkItProd	Plain-JSON variant — opt in via check_endpoint="checkItProd"	1 credit ($0.01)
POST /v1/checkRelevance	Free pre-screen; skips irrelevant actions	free
POST /v1/verifyProof	Third-party proof verification (public)	free

Anyone holding the proof_id from an audit entry can verify the decision independently — no ICME account required. Note: the JOLT proving pipeline has not yet completed a formal security audit; treat proofs as transparency artifacts, not yet as a sole trust boundary.

Assurance levels: handling non-binary verdicts

/v1/checkIt runs three verifiers — an LLM check (llm_result), the Z3 SMT solver (z3_result), and an automated-reasoning engine (ar_result) — and the top-level result can be non-binary: e.g. "AR uncertain" (the AR engine wants unanimous confirmation) or "AR unavailable" (the AR engine is degraded). The assurance parameter decides what happens then:

Level	Uncertain result is allowed when...	Posture
strict (default)	never — only top-level result == "SAT" allows	strictest; recommended
unanimous	llm, z3, AND ar each returned SAT	high
dual	llm and z3 returned SAT (AR advisory)	moderate

No level ever overrides an explicit top-level UNSAT. When a level clears an uncertain verdict, the decision reason records exactly why (allowed under 'dual' assurance: ...) plus the per-verifier summary, so the audit entry stays self-explanatory — and a log search for allowed under shows precisely how much assurance was traded, and when. Recommended posture: strict in steady state; dual as a documented, temporary fallback during AR degradation.

ICMEBackend(policy_id=..., api_key=..., assurance="unanimous")

Field notes

Behaviors we hit while battle-testing this integration against the live API, and how the backend handles them:

• result is an open set, not a SAT/UNSAT boolean. Live runs returned "AR uncertain" and "AR unavailable" alongside SAT/UNSAT. The backend therefore gates on result == "SAT" and nothing else; any unrecognized state is handled by the assurance policy (strict: deny). Integrations that check result != "UNSAT" fail open through states they have never seen.
• Wrong-policy misconfiguration fails safe under strict. Checking actions against an unrelated policy_id produced extractions with no overlap with the action's facts — and sub-verifiers still reported SAT. The strict default (plus the extracted: echo in every deny reason, which makes the mismatch obvious at a glance) contained it.
• Extraction can error on irrelevant input. Actions that mention none of a policy's variables can fail extraction outright. Scope consequential tools with triggers so routine calls never reach the paid check, and the fail-closed path covers the rest.

Notes

• Latency & cost scoping. Use triggers (tool-name set or a predicate over the context) so only consequential actions pay the ~sub-second network check; everything else stays on AGT's free tier.
• Denied means denied. UNSAT action fingerprints are re-denied from a local cache (default 5 minutes) so an agent cannot cheaply retry a blocked action verbatim until something slips through.
• AGT package consolidation. AGT is migrating agent-os-kernel → agent-governance-toolkit-core; this package imports BackendDecision opportunistically and falls back to a field-compatible local type, so it tracks either layout.

Testing

pip install pytest
python -m pytest tests -q                    # unit tests, no network
AGT_REPO=/path/to/agent-governance-toolkit \
python -m pytest tests -q                    # + conformance vs real AGT PolicyEvaluator

The conformance suite asserts isinstance(ICMEBackend(...), ExternalPolicyBackend) against AGT's runtime-checkable protocol (ADR-0015) and that proofs propagate into PolicyDecision.audit_entry through Microsoft's actual evaluator. CI re-runs it against a fresh clone of upstream main on every push.

Roadmap

• MAF FunctionMiddleware wrapper (direct, evaluator-less path)
• .NET twin for Microsoft.AgentGovernance / Microsoft.Agents.AI
• POST /v1/explain integration for opaque inputs (shell commands, encoded tool calls)
• "Act 5: semantic bypass" fork of AGT's 01-loan-processing MAF example — see examples/maf-loan-act5/
• Upstream: contribute the backend + the Act 5 scenario to AGT's examples/maf-integration

License

MIT