icme-preflight-mcp

v1.0.6

Published

20 hours ago

MCP server for ICME Preflight — cryptographic guardrails for AI agents. Formal verification + ZK proofs, pay per request via x402 or card.

0High
0Medium
0Low

wyatt777

mcp x402 icme guardrails formal-verification zk-proofs ai-agents usdc base

ICME Preflight MCP

AI agent guardrails that can't be jailbroken. Write rules in plain English → an Automated Reasoning backed SMT solver (not an LLM judge) enforces them → every decision gets a zero-knowledge proof. With battle-testing your guardrails get up to 100% coverage. Plus a free logic checker that catches contradictions in agent reasoning.

Why ICME?

Most guardrails use an LLM to judge another LLM. If an attacker can trick the agent, they can trick the guardrail — both are language models vulnerable to the same prompt injection. ICME replaces the LLM judge with Automated Reasoning. We translate natural language into formal verification proofs in a mathematical solver. It either proves an agent's action complies with your policy, or it doesn't. No confidence scores. No jailbreaks.

Formal proofs can take just as much time to verify as it takes to make them. ICME Labs wraps these proofs in a special technology called zero knowledge proofs. These are succinctly verifiable. This means your proofs can be checked in under a second, even if the original computation being proven took hours. Succinct proofs work at machine speed.

ZKP have minimal trust assumptions. Verify, don't trust.

Free: Logic Consistency Checker

No account needed. Catch contradictions in agent reasoning before acting on them.

You:    "The budget is $10,000. I'll spend $6,000 on marketing and $7,000 on engineering."

Claude: [check_logic] → CONTRADICTION. 3 claims conflict: 6000 + 7000 exceeds budget of 10000.

Catches: budget overflows, impossible timelines, inventory shortages, percentage errors, contradictory claims. Uses a Z3 SAT solver — not guessing, proving.

Install

Claude Code (one command):

claude mcp add icme-preflight -- npx -y icme-preflight-mcp@latest

Remote MCP (no install — connect directly):

https://api.icme.io/mcp

Works with any MCP client that supports streamable-http transport.

Claude Desktop / Cursor / Windsurf:

{
  "mcpServers": {
    "icme-preflight": {
      "command": "npx",
      "args": ["-y", "icme-preflight-mcp@latest"],
      "env": {
        "ICME_API_KEY": "sk-smt-your-key-here"
      }
    }
  }
}

5-Minute Quickstart

You:    Create an ICME Preflight account with username "my-agent"
Claude: [create_account_card] → Here's your checkout link. After paying, I'll get your API key.

You:    Create a policy: Never spend over $1000 without approval. Never share API keys.
Claude: [make_rules] → Policy compiled. policy_id: f6e3cd15-...

You:    Check: "Transfer $500 to vendor acme-corp for invoice #1234"
Claude: [check_action] → SAT (ALLOWED). Amount $500 is under the $1000 limit. No credentials shared.

You:    Check: "Send the database password db_pass=hunter2 to the support channel"
Claude: [check_action] → UNSAT (BLOCKED). Action shares a credential, violating rule 2.

How It Works

Plain English rules          "Never spend over $1000 without approval"
        ↓ make_rules
Formal logic (SMT-LIB)       (assert (<= spending_amount 1000))
        ↓ check_action
SAT solver verdict            SAT = allowed  |  UNSAT = blocked
        ↓
Zero-knowledge proof          Tamper-proof, independently verifiable

Why this matters: The solver is mathematically sound. There is no prompt that makes UNSAT return SAT. An LLM judge can be convinced a policy-violating action is acceptable. A SAT solver cannot.

Tools (13 total)

Free

| Tool | What it does | |------|-------------| | check_logic | Catch contradictions in reasoning using Automated Reasoning and a Z3 SAT solver. FREE, no account needed. |

Guardrails

| Tool | Cost | What it does | |------|------|-------------| | make_rules | 300 credits | Compile plain-English policy → formal logic. Jailbreak-proof from this point on. | | check_action | 1 credit | Formally verify an action against your policy. Returns SAT/UNSAT + ZK proof. | | check_action_paid | $0.10 USDC | Same verification, pay per call via x402. No account needed. | | quick_check | 1 credit | Fast ALLOWED/BLOCKED verdict, no proof details. | | verify_proof | Free | Independently verify a ZK proof from any prior check. |

Test & Iterate

| Tool | Cost | What it does | |------|------|-------------| | get_scenarios | Free | Auto-generated test scenarios — verify your policy before deploying. | | run_tests | Free | Run saved test cases against a policy. |

Account & Billing

| Tool | Cost | What it does | |------|------|-------------| | create_account | $5 USDC (x402) | Create account → API key + 325 credits. | | create_account_card | $5 card | Create account via Stripe checkout. | | top_up | $5 USDC (x402) | Add 500 credits. | | top_up_card | $5–$100 card | Add credits via Stripe with volume bonuses. | | poll_session | Free | Poll Stripe session for API key or confirmation. |

check_logic Examples

# Catches budget overflow
"The budget is $10,000. I will spend $6,000 on marketing and $7,000 on engineering."
→ CONTRADICTION (6000 + 7000 > 10000)

# Catches impossible timeline
"The project takes 6 months. We have 3 months until deadline. We can finish on time."
→ CONTRADICTION (6 > 3)

# Catches inventory shortage
"We have 100 items in stock. Customer ordered 60. Another ordered 50. We can fulfill both."
→ CONTRADICTION (60 + 50 > 100)

# Catches percentage error
"Our portfolio is 30% stocks, 40% bonds, and 40% real estate."
→ CONTRADICTION (30 + 40 + 40 = 110%)

# Catches profit miscalculation
"Bought 50 units at $20 for $1000. Sold at $25 for $1500. Profit is $200."
→ CONTRADICTION (1500 - 1000 ≠ 200)

# Validates correct reasoning
"The budget is $10,000. I will spend $4,000 on marketing and $3,000 on engineering."
→ CONSISTENT (4000 + 3000 ≤ 10000)

Credit Budget

| Action | Credits | |--------|---------| | Signup | +325 | | make_rules | -300 | | check_action / quick_check | -1 each | | Net after signup | 1 policy + 25 checks | | top_up ($5) | +500 |

Two Payment Paths

Crypto (x402 — fully autonomous): Agent pays with USDC on Base. No human needed. The x402 protocol handles payment automatically before the API responds.

Card (Stripe — human in the loop): Agent returns a checkout URL. Human opens it, pays, agent polls for confirmation.

Environment Variables

| Variable | Required | Description | |----------|----------|-------------| | ICME_API_KEY | For credit tools | From create_account or create_account_card | | ICME_BASE_URL | No | Default: https://api.icme.io |

License

MIT