tau-x402-cage 0.25.0

Formal policy-semantics cage for HTTP 402 agentic payments (x402 + MPP)

[!IMPORTANT] Dual-licensed. GPLv3 for OSS + royalty-free patent grant. Commercial license for closed-source integrations. Contact [e-mail].

---

What this is

tau-x402-cage is a policy and governance layer for safer agent payments and sits in front of your existing x402 stack.

Designed for AI agents and autonomous systems that can initiate payments via x402. Every intent the agent submits runs through a declarative policy, gets a signed decision, and lands in an audit bundle a regulator can verify offline.

flowchart LR
    A[AI agent] --> B[tau-x402-cage<br/>policy · limits · approvals · audit]
    B -->|approved| C[x402 stack] --> E[Vendor / paid API]
    B -->|denied or flagged| D[Block · review · shadow log]

Who this is for

• AI agents that can spend money without a human in the loop
• Autonomous workflows with API budgets, retry logic, and no standing oversight
• LLM-driven systems that hit paid endpoints during planning or tool-use
• Teams running x402 in production who need audit trails their compliance team will accept

When to use this

• Use it when your agent spends autonomously and you need budgets, merchant controls, approvals, or an audit trail
• Use it when policy consistency matters and you cannot rely on every rule author writing non-contradictory YAML
• Use standard x402 on its own when you only need basic payment handling and no governance layer

---

Why this exists

Two HTTP-402 standards shipped within 16 days in early 2026 (Coinbase's x402 in the Linux Foundation; Stripe+Tempo's MPP with Visa). Both are governed by neutral foundations. Neither specifies what "a policy" actually means.

Daily x402 volume sits around $3.4M across 88k transactions with an average size of ~$39 (Artemis, 2026-04-18). That average puts agent payments in the regime where a compromised or prompt-injected agent doing a handful of wrong calls is no longer a rounding error. But every policy-guardrails write-up published in Q1 2026 stops at "spending caps + merchant category + time-bound permissions" — the level OPA and Cedar already ship.

Static contradiction detection over simple allow/deny rules is solved — AWS Cedar's Zelkova uses z3, OPA has linting, Rego has policy-as-code tooling. What production agent payments actually need is narrower and none of those ship it.

The cage rests on three load-bearing capabilities. Everything else — adaptive tightening, revision branching, natural-language authoring, integrations — is supporting cast.

1. Decidable contradiction on fragment-v1; bounded model-checking on fragment-v2. Limits like "no more than $X spent in the last hour", "wait 60 seconds after a reject before retrying", or "at most N calls to this provider in a rolling 24-hour window" are past-temporal. Cedar Zelkova is propositional + linear integer arithmetic and does not reason about these operators in a single proof call. Fragment-v1 of the cage closes the decidable subset in Tau with a full decision procedure; fragment-v2 covers the windowed residue in z3 with bounded unrolling (N=10 default). Every envelope carries proof_strength so callers can distinguish the two; Guaranteed Mode restricts to fragment-v1 only.

2. Strengthening-only mutation enforced by a transition invariant. NoWeakening + OverridesMustExpire are themselves proof obligations every policy change must satisfy before it activates. A raised spending cap, a lengthened retry window, or a dropped provider from the allowlist is rejected at admission — the active revision does not change. Scope: single-parameter comparison per rule type today; multi-dimensional trade-offs (tighten one knob, loosen another) are caught only when the composite policy produces a separate contradiction. Cedar and OPA have no equivalent; limit relaxation there is an authoring-side convention, not a decidable one.

3. Per-verdict signed provenance. Every decision envelope cryptographically binds (intent_hash, policy_revision_id, proof_backend, proof_strength, prover_mode, compile_hash) so an auditor can reconstruct the exact rulebook state that signed off on any given decision and tamper-detect single-byte mutation. Two signing backends: HMAC-SHA256 (default — authenticates the facilitator ↔ cage trust boundary; the operator holds the key) and Ed25519 (the signing-ed25519 extra — required for external-auditor non-repudiation, since verifiers only need the published public key). Regulated pilots should run Ed25519.

In plain English: before a new rule goes live, the cage tells you — with a decision procedure, not a heuristic — whether it silently contradicts an existing backwards-looking time rule. It blocks anyone from quietly raising a spending cap without re-proving the whole rulebook is still safe. And every verdict carries a cryptographic receipt tying it to the exact rulebook version in force at the moment it fired, so "what rules were live last Tuesday at 3pm" is a verifiable question.

Full market context, competitive landscape, and pilot shape: docs/why_this_exists.md. Real-world incidents that inform the runtime design: docs/why_this_matters.md.

---

Example demo — what a retry loop looks like with the cage

python3 demos/hero_retry_loop.py --quiet

An agent enters a retry loop at $50 per call. The baseline SpendingCap blocks the fourth call. Adaptive tightening ramps on every reject, shrinks the limits further, and surfaces what the loop would have cost:

{
  "blocked": true,
  "reason": "adaptive_tightening_triggered",
  "without_system_estimate": {"projected_spend": 2400},
  "with_system":             {"actual_spend":   150},
  "prevented_loss": 2250
}

---

Install

60-second install — compat + verified modes

pip install tau-x402-cage
tau-x402 run

tau-x402 run boots the daemon with a deny-by-default safe policy, adaptive tightening enabled, advisory signals on, and offline-verifiable audit logs. Zero config. Compat mode (pattern prover) by default; verified mode works if a tau binary is on PATH.

Use the wheel extras when you need them:

pip install tau-x402-cage[saas]             # FastAPI + web UI
pip install tau-x402-cage[fragment-v2]      # z3 for windowed constraints
pip install tau-x402-cage[signing-ed25519]  # Ed25519 instead of HMAC
pip install tau-x402-cage[metrics]          # Prometheus /metrics
pip install tau-x402-cage-client            # thin httpx-only caller for agents

Agents written in TypeScript, LangChain, LlamaIndex, OpenAI function-calling, or anything speaking MCP have bindings already: see integrations/ and ts/.

Guaranteed Mode — reproducible via Docker

Guaranteed Mode routes every admission through a pure-Tau decision procedure and requires the patched IDNI Tau Language CLI (incorporating the three pending fixes filed upstream: IDNI/tau-lang#64, #65, #66). The published image bundles that binary so no local Tau build is needed:

docker run --rm -v /tmp:/tmp \
  ghcr.io/jme-tau/tau-x402-cage:v0.24.0-guaranteed \
  --prover-mode guaranteed

Full install walkthrough, verification, and local-build instructions: docs/guaranteed_mode_install.md.

Distribution matrix — what works where

Artifact	Compat mode	Verified mode	Guaranteed mode
pip install tau-x402-cage	✅	✅ (if tau on PATH)	❌
docker run ghcr.io/jme-tau/tau-x402-cage:<ver>	✅	❌	❌
docker run ghcr.io/jme-tau/tau-x402-cage:<ver>-guaranteed	✅	✅	✅
Local build from source + patched Tau	✅	✅	✅

The :-guaranteed tag carries the patched Tau CLI bundled into python:3.12-slim; total image ~310 MB. Once IDNI merges #64/#65/#66 upstream, a platform-wheel release will vendor Tau into the [tau] extra and Guaranteed Mode becomes reachable via pip install tau-x402-cage[tau].

---

Corporate card demo — bank-grade walkthrough

python3 demos/corporate_card_demo.py

ProcureBot-7 is a fictional agent with an 8-invariant policy covering per-tx caps, daily caps, per-vendor caps, retry cadence, rolling counts, and burst velocity. The demo walks 7 scenarios:

#	Scenario	Result
1	Policy admission under Guaranteed Mode	admitted with evidence record
2	Routine $35 AWS invoice	allowed
3	Knight Capital-style retry loop	blocked at retry #3 by adaptive tightening
4	Milkie Way-style runaway $30 × many	composed violation, prevented $1800/60s
5	Weakening mutation (cap raised without approval)	rejected by NoWeakening, active revision unchanged
6	Lookalike spoof st-ripe.com	rejected, not in allowlist
7	Signed audit bundle exported + verified offline	HMAC verifies, single-byte tamper breaks it

Each scenario prints the decision, the rule that fired, and a real-world incident citation (Knight Capital 2012 SEC filing, Milkie Way Cloud Run 2020 HN #25372336, FinCEN BEC advisory FIN-2019-A005).

---

How it works

Admission and request-time run on different paths. Decision procedures live in admission; the request hot path is a lookup against the already-admitted ruleset.

Declare time (admission)

An operator op (declare_x402, add_invariant, update_invariant, remove_invariant, plus every mutation op) is routed through the pattern prover first, then Tau on the fragment-v1 subset, then z3 on the fragment-v2 subset, then a cross-fragment composer. The registry is swapped only when a decisive proof token comes back. Guaranteed Mode further requires the pure-Tau path to close decisively.

sequenceDiagram
    participant Operator
    participant Daemon
    participant Pattern as Pattern prover
    participant Tau as Tau (fragment v1)
    participant Z3 as z3 (fragment v2)
    participant Hybrid as HybridProver
    participant Log as Revision log

    Operator->>Daemon: declare_x402 / add_invariant / update_invariant / remove_invariant
    Daemon->>Daemon: classify delta by fragment
    Daemon->>Pattern: prove(full candidate set)
    alt pattern Contradiction
        Pattern-->>Daemon: Contradiction(left, right, reason)
        Daemon-->>Operator: reject, registry unchanged
    else pattern clean
        Pattern-->>Daemon: ProofToken (strength=pattern)
        Daemon->>Tau: prove(v1 subset)
        Daemon->>Z3: prove_delta(added, removed, v2 current)
        Daemon->>Hybrid: prove_delta(added, removed, full current)
        alt any Contradiction, or InconclusiveProof under strict mode
            Daemon-->>Operator: reject, registry unchanged
        else decisive
            Daemon->>Log: append PolicyRevision (mint policy_revision_id)
            Daemon-->>Operator: admitted, new revision_id
        end
    end

Request time (enforcement)

X402Registry.check_payment walks the admitted invariants and returns the first violation. The verdict is signed, recorded, and emitted. The prover chain is not on the hot path.

sequenceDiagram
    participant Agent
    participant Fac as Facilitator
    participant Cage as mediate() + daemon
    participant Reg as X402Registry
    participant Hist as History store

    Agent->>Fac: POST /pay (HTTP 402 + X-PAYMENT)
    Fac->>Cage: mediate(headers, body, secret)
    Cage->>Cage: parse + schema-validate intent
    Cage->>Reg: check_payment(intent, history, rejects)
    Reg-->>Cage: Violation | None (pure Python, no prover)
    Cage->>Hist: append(intent, kind=permit|reject) + verdict record
    Cage->>Cage: sign envelope (HMAC-SHA256 or Ed25519)
    Note over Cage: envelope MAC-binds policy_revision_id, proof_backend,<br/>proof_strength, prover_mode, compile_hash, intent_hash, ttl
    Cage-->>Fac: signed envelope
    Fac->>Fac: verify MAC + intent_hash + TTL
    alt permit
        Fac->>Agent: 200 OK + X-Policy-Verdict: permit
    else reject
        Fac->>Agent: 403 + X-Policy-Verdict: reject + X-Policy-Rule-Id + reason
    end

What else is in here

Supporting capabilities layered on the three load-bearing guarantees. Each exists because a specific deployment scenario needed it; none of them is the differentiator.

• Runtime layers. Adaptive tightening (deterministic, policy-aware, decays over 900s), composed-violation reporting, cross-revision awareness, kernel-verified peer authentication, forward-projected prevented-loss with Tau-proven upper bound.
• Policy management. Pointwise revision with proof provenance, branching with 3-way merge, BranchRespectsCore transition invariant, natural-language authoring loop, meta-policy tier.
• Distribution. Python SDK, TypeScript SDK, MCP server, LangChain / LlamaIndex / OpenAI bindings, gRPC, webhook sink, Prometheus /metrics, Helm chart, offline-verifiable audit bundle.

Full per-capability feature matrix + vendor-by-vendor comparison across the x402 ecosystem: docs/competitive_landscape.md.

Flexible vs Guaranteed mode

Mode	When to pick	Prover
Flexible (default)	Broader rule surface, easier to author, start here	Tau + z3 + pattern fallback
Guaranteed (opt-in via Docker today)	Bank-grade deployment; every admitted rule closes under pure-Tau proof	Pure Tau, 9 rule types + 2 meta-policies

Guaranteed Mode refuses anything outside its supported rule set with UNSUPPORTED_FOR_GUARANTEED_MODE — no downgrade, no z3 fallback, no nlang smuggling. Install: docker pull ghcr.io/jme-tau/tau-x402-cage:v0.24.0-guaranteed. Full details: docs/guaranteed_mode_install.md, docs/guarantees.md, docs/threat-model.md, docs/regulatory-mapping.md.

---

Security properties

Four attacks, four defences, four passing property tests:

Attack	Defence	Test
Attacker flips permit ↔ reject header	HMAC-SHA256 over canonical payload	tests/test_verdict_signer.py::test_tampered_outcome_fails_verify
Attacker replays $10 permit against $10,000 intent	intent_hash binding checked before MAC	tests/test_verdict_signer.py::test_replay_against_different_intent_fails
Attacker replays expired permit	TTL + issued_at enforced	tests/test_verdict_signer.py::test_expired_verdict_rejected
Hostile payment intent injects Tau syntax	Safe-token regex on every field	tests/test_payment_intent_matcher.py::test_provider_injection_attempt_rejected

Plus v0.22.0 additions:

Attack	Defence	Test
Non-privileged process submits a mutation op over the UDS	Kernel peer-cred check against admitted PeerAuthenticationPolicy	tests/test_daemon_peer_auth.py
Rogue operator adds themselves to the allowed-peer set	Adding a UID is weakening; rejected by NoWeakening without an approval token	tests/test_meta_policy.py
Feature branch mutates a rule tagged "core"	BranchRespectsCore rejects at admission; active revision unchanged	tests/test_branch_respects_core_wired.py
Audit bundle tampered post-export	HMAC-SHA256 over canonical JSON-lines payload; single-byte flip breaks verify	tests/test_guaranteed_audit.py::test_tamper_breaks_verification

What we're NOT claiming

[!CAUTION] No software-only policy engine can defend against the four attacks below. We shift the attack surface from "silent runtime drift" (breached for months without knowing) to "spec review" (humans can catch mistakes). That is the trade on offer.

Out-of-scope attack	Your responsibility
Rule authorship errors ($10,000 when you meant $1,000)	Review processes, spec testing, change management
Trusted Computing Base compromise	Process isolation, binary attestation, runtime monitoring
Side channels not modeled by the rules	Expand the spec to cover the channel
Info-leak via attributed verdict rule_id	Redact or generalise for external-facing contexts

Full threat model (trust boundaries, 8 attacker models, residual risks, red-team stress-test steps): docs/threat-model.md.

---

CLI

tau-x402 run                            # authorise payments for your agent (safe defaults)
tau-x402 quickstart                     # scaffold policy.yaml + .env for first-run
tau-x402 init                           # create an editable starter policy
tau-x402 lint <policy.yaml>             # check a policy file for contradictions before declaring
tau-x402 suggest                        # natural-language → YAML authoring loop
tau-x402 narrate <policy.yaml>          # YAML → plain English
tau-x402 inspect                        # inspect the active policy and prover mode
tau-x402 explain                        # explain why a policy is admitted or rejected
tau-x402 explain-decision <id>          # explain why a payment was allowed or denied
tau-x402 compare                        # show prevented spend vs running without the cage
tau-x402 risk-prevented                 # show runtime risk counters
tau-x402 bundle --out <path>            # export a signed decision bundle
tau-x402 bundle-verify <path>           # verify a signed bundle offline
tau-x402 audit-export --out <path>      # export a signed audit bundle
tau-x402 guaranteed export-audit-bundle # guaranteed-mode audit trail
tau-x402 guaranteed inspect-policy      # admission evidence for a revision
tau-x402 guaranteed replay-decision     # deterministic decision replay

tau-x402-cage remains wired as an alias for existing scripts, docs, and CI.

---

Calling the cage from an agent

Over the Unix socket:

import json, socket
s = socket.socket(socket.AF_UNIX); s.connect("/tmp/tau-x402-cage.sock")
s.sendall(json.dumps({
    "op": "check_payment",
    "intent": {
        "amount": "35", "currency": "USDC", "provider": "aws.amazon.com",
        "counterparty": "aws.amazon.com:primary", "rail": "x402",
        "timestamp_unix": 1713000000, "request_id": None,
    }
}).encode() + b"\n")
print(s.makefile().readline())

Over the Python client SDK (pip install tau-x402-cage-client):

from tau_x402_cage_client import CageClient
client = CageClient(socket_path="/tmp/tau-x402-cage.sock")
decision = client.check_payment(intent)
if decision.allowed:
    settle_payment(intent)

Over MCP (Claude Desktop, Agent SDK, Cursor, Cline, LangChain): see mcp/README.md. Nine tools, eight invariant schemas as resources, three prompts.

Over TypeScript (@idni/tau-x402-cage-client, @idni/tau-x402-cage-mcp): see ts/README.md. Zero runtime deps.

---

Documentation

Path	Purpose
docs/rfc/2026-04-x402-formal-policy-semantics.md	IETF-style RFC draft-00 of the wire protocol
docs/guarantees.md	15 cataloged guarantees
docs/threat-model.md	STRIDE-aligned threat model, 12 sections, 3 appendices
docs/regulatory-mapping.md	60-row matrix: FCA, PRA, PSD2, DORA, FFIEC, FINRA, NYDFS, OCC, SOC 2, ISO 27001, NIST 800-53
docs/mappings/x402-mapping.md	Wire-level x402 request/response examples
docs/quickstart.md	Zero-to-first-reject walkthrough
docs/adr/001-prover-backends.md	Pattern / Tau / z3 / hybrid split and trade-offs
docs/semantic_fragment_v1.md	Tau-decidable subset, encoding rules
docs/pointwise_revision.md	Revision model, deltas, incremental compile
CHANGELOG.md	Every release with scope and limits

---

Honest limits

• prevented_risk carries a Tau-backed proven_upper_bound_usd alongside an EMA-based observed_trajectory_usd; the witness_status field names which path produced the headline so no figure silently claims more than it can prove. Full semantics: docs/tau_witness.md.

---

Status

• Version: 0.24.0 (2026-04-20)
• Guaranteed Language tier: v1.2.0 (9 rule types + 2 meta-policies)
• Python: 3.11 / 3.12 / 3.13 / 3.14
• Platforms: macOS (aarch64 + x86_64), Linux (x86_64 + aarch64)
• Guaranteed Mode distribution: reproducible via ghcr.io/jme-tau/tau-x402-cage:v0.24.0-guaranteed (multi-arch, ~310 MB); PyPI [tau] extra pending upstream Tau merge
• Upstream Tau: patches filed at IDNI/tau-lang #64 / #65 / #66, pending review
• Pilot status: available for design-partner engagement; hosted SaaS not yet live; zero external production users today

---

Security contact

Report security issues privately to [e-mail]. Do not open public issues for credential, HMAC-key, or prover-chain vulnerabilities. PGP key on request.

---

License

Dual: GPLv3 for open-source use with a royalty-free patent grant, or a commercial license from IDNI for closed-source integrations and hosted services. US patent 12,254,082. Inventor: Ohad Asor / IDNI.