tau-x402-cage 0.23.1

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.

What auditors actually ask — "prove two rules don't silently contradict", "prove the decision came from your engine, not a compromised sidecar", "reconstruct the rule set that was live last Tuesday" — nobody has shipped. The cage closes that gap.

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
}

---

60-second install

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.

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/.

---

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

Runtime layers built on top

Adaptive tightening (v0.21.0). Four independent signals (retry density, denial rate, velocity spike, identical-request fingerprint) feed a bounded level in [0, 1] that shrinks spend caps, grows cooldowns, and decays back to baseline over a 900s half-life. Deterministic. Policy-aware — limits only tighten, never weaken. In v0.22.0 the tightening parameters themselves are Tau-admitted as an AdaptiveTighteningPolicy: changes pass the same NoWeakening gate every other policy mutation does.

Composed violations (v0.21.0). When two rules fire on the same intent, the decision envelope lists both plus any near-threshold invariants so downstream remediation can see the whole picture.

Cross-revision awareness (v0.21.0) + BranchRespectsCore (v0.22.0). Runtime decisions surface previous_policy_revision and current_policy_revision. If a feature branch tries to mutate a rule tagged "core", the transition rejects at admission — protected-class provenance carries across branches.

Tau-proven upper bound (v0.22.0). estimate_prevented_risk returns a dual figure: proven_upper_bound_usd (a Tau-extracted bv witness for the maximum cumulative spend the active policy admits; structural ceiling when the Tau probe is inconclusive) plus observed_trajectory_usd (the EMA estimate). witness_status marks exactly which path produced the headline.

Peer authentication (v0.22.0). Every mutation op is gated by a kernel-verified peer credential (SO_PEERCRED on Linux, LOCAL_PEERCRED / getpeereid on macOS) against an admitted PeerAuthenticationPolicy. Adding a new trusted peer requires a NoWeakening-passing mutation — compromised operators cannot silently add themselves.

Audit evidence. PolicyAdmissionEvidence and RuntimeDecisionEvidence are frozen, append-only, and serialisable to an HMAC-signed bundle an auditor can verify offline without the daemon. Counters and caps go in. Payer PAN, cardholder name, and raw counterparty strings do not — pinned by regression test.

Adaptive tightening (v0.21.0). Four independent signals (retry density, denial rate, velocity spike, identical-request fingerprint) feed a bounded level in [0, 1] that shrinks spend caps, grows cooldowns, and decays back to baseline over a 900s half-life. Deterministic. Policy-aware — limits only tighten, never weaken. In v0.22.0 the tightening parameters themselves are Tau-admitted as an AdaptiveTighteningPolicy: changes pass the same NoWeakening gate every other policy mutation does.

Composed violations (v0.21.0). When two rules fire on the same intent, the decision envelope lists both plus any near-threshold invariants so downstream remediation can see the whole picture.

Cross-revision awareness (v0.21.0) + BranchRespectsCore (v0.22.0). Runtime decisions surface previous_policy_revision and current_policy_revision. If a feature branch tries to mutate a rule tagged "core", the transition rejects at admission — protected-class provenance carries across branches.

Tau-proven upper bound (v0.22.0). estimate_prevented_risk returns a dual figure: proven_upper_bound_usd (a Tau-extracted bv witness for the maximum cumulative spend the active policy admits; structural ceiling when the Tau probe is inconclusive) plus observed_trajectory_usd (the EMA estimate). witness_status marks exactly which path produced the headline.

Audit evidence. PolicyAdmissionEvidence and RuntimeDecisionEvidence are frozen, append-only, and serialisable to an HMAC-signed bundle an auditor can verify offline without the daemon. Counters and caps go in. Payer PAN, cardholder name, and raw counterparty strings do not — pinned by regression test.

---

What's different about tau-x402-cage

	tau-x402-cage	OPA / Rego	AWS Cedar	TLA+ / Alloy	Kevros
Rule-rule contradiction detection at declare-time	yes	no	no	yes (offline)	not published
Signed verdicts with intent binding	yes (HMAC + intent_hash)	no	no	n/a	cryptographic, no semantic
Temporal reasoning over traces (LTL + past-LTL)	yes	no	no	yes	not published
Decidability guarantee over composed rule sets	yes	no (T-complete)	partial	yes	not published
Multi-typed reasoning in one engine (atomless BA)	yes	partial	partial	yes	n/a
Runs in the request path	yes	yes	yes	no (offline)	yes
Single-digit-ms p95	yes (< 10ms)	yes	yes	n/a	not published
Public TTI benchmark	yes	no	no	n/a	no
Live product + managed service	not yet	yes	yes	n/a	yes (Azure)

The first five rows are the formally-grounded core. The rest is parity incumbents can reach in a quarter — except productisation, which is where Kevros currently leads. See docs/why_this_exists.md for the full competitive landscape.

---

What Tau Language uniquely enables

Tau Language is a decidable temporal logic with self-reference, developed by IDNI for nearly a decade (GitHub). Every capability below pairs with a specific module on master.

• Declare-time contradiction detection. adapter/hybrid_prover.py composes rule bodies and runs the consistency check before the policy admits traffic. Surfaced via tau-x402 lint.
• True incremental SAT. adapter/prover.py::IncrementalZ3Prover holds a persistent z3 solver across revisions with push/pop frames keyed by deterministic per-invariant tags from adapter/z3_compiler.py::frame_tag. Adding or removing a rule is delta-priced.
• Past-LTL invariants. RetryRateLimit uses the unary past operator O (and a & alias at wff level) to express "retry only if there was no recent reject for this pair" directly in the rule body. See adapter/invariants.py::RetryRateLimit._body. Required three upstream Tau patches (IDNI/tau-lang#64 / #65 / #66).
• Cross-fragment hybrid verdict. HybridProver composes Fragment v1 (Tau set-algebraic) with Fragment v2 (z3 arithmetic-temporal) under shared-variable projection, and admits a policy only when both fragments agree.
• SAT witness extraction. adapter/z3_compiler.py::extract_witness returns a concrete permit trace (amount, provider, timestamp) when the composed spec is consistent. adapter/prover.py::TauConsistencyProver::extract_bv_witness (v0.22.0) does the same against Tau's bv BA for the prevented-risk proven upper bound.
• Pointwise revision with proof provenance. add_invariant / remove_invariant / update_invariant / diff_revisions mutate one rule at a time, each producing a new policy_revision_id that is MAC-bound into the signed verdict envelope (adapter/verdict_signer.py). Every permit or reject ties back to the exact ruleset that produced it.
• Branching and 3-way merge over policies. Git-like policy branches with auto-merge of disjoint deltas. BranchRespectsCore (v0.22.0) prevents feature branches from mutating rules tagged core.
• Meta-policy tier (v0.22.0). Adaptive-tightening parameters and peer-authentication policy lift into Tau-admitted first-class policies. Changes pass NoWeakening. See adapter/meta_policy.py.

Tau is the decidable core. OPA, Cedar, and request-path policy engines answer "does this rule fire on this request". Tau answers "is this rule set internally consistent" at declare time over the x402 payment fragment, so contradictions are caught before traffic hits the registry — not after.

---

Mode	How to pick	Language surface	Prover
Flexible (default)	Start here. Broader rule surface, easier to author, no opt-in.	Full rule set + free-form variants	Tau + z3 + pattern fallback
Guaranteed (opt-in)	Switch to this for bank-grade deployment. Narrower rule surface; every admitted rule closes under a pure-Tau proof.	v1.2.0 tier: 9 rule types + 2 meta-policies, per_tx / per_window / per_provider_per_window scopes, past-LTL G / O / H	Pure Tau

Guaranteed Mode covers SpendingCap, MaxPerCall, ProviderAllowlist, RetryRateLimit, RollingWindowCap, BurstVelocityCap, JurisdictionRule (enum), CounterpartyConstraint (enum), MutualExclusion (composition). Plus two admitted meta-policies: AdaptiveTighteningPolicy and PeerAuthenticationPolicy. Anything outside that set is refused with UNSUPPORTED_FOR_GUARANTEED_MODE — no downgrade, no z3 fallback, no nlang smuggling. Natural-language variants of JurisdictionRule / CounterpartyConstraint stay Flexible-only until upstream nlang work merges.

See docs/guarantees.md, docs/threat-model.md, and 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.23.0 (2026-04-20)
• Guaranteed Language tier: v1.2.0 (9 rule types + 2 meta-policies)
• Tests: 2328 passing, 12 skipped, CI green
• Python: 3.11 / 3.12 / 3.13 / 3.14
• Platforms: macOS (aarch64 + x86_64), Linux x86_64
• 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

---

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.