Metadata-Version: 2.4
Name: tau-x402-cage
Version: 0.26.0
Summary: Formal policy-semantics cage for HTTP 402 agentic payments (x402 + MPP)
Author-email: IDNI <services@idni.org>
License: Tau x402 Cage — Dual License
        Copyright (c) 2026 IDNI (Ohad Asor). All rights reserved.
        
        SPDX-License-Identifier: GPL-3.0-or-later OR LicenseRef-IDNI-Commercial
        
        ================================================================================
          DUAL-LICENSE NOTICE
        ================================================================================
        
        This software is dual-licensed. You may choose one of the two licenses below,
        according to your use.
        
        --------------------------------------------------------------------------------
          1. GNU General Public License v3.0 or later (GPL-3.0-or-later)
        --------------------------------------------------------------------------------
        
        This software is free software: you can redistribute it and/or modify it under
        the terms of the GNU General Public License as published by the Free Software
        Foundation, either version 3 of the License, or (at your option) any later
        version.
        
        This software is distributed in the hope that it will be useful, but WITHOUT
        ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
        FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
        
        You should have received a copy of the GNU General Public License along with
        this software. If not, see <https://www.gnu.org/licenses/gpl-3.0.txt>.
        
        --------------------------------------------------------------------------------
          2. IDNI Commercial License
        --------------------------------------------------------------------------------
        
        Organizations that cannot or prefer not to adopt the GPL-3.0-or-later terms
        (for example: proprietary in-house deployments, enterprise self-host, hosted
        SaaS resale, or closed-source integrations) may obtain a commercial license
        from IDNI on separate written terms.
        
        Contact:  services@idni.org
        Pricing:  see docs/pricing.md
        
        --------------------------------------------------------------------------------
          PATENT NOTICE
        --------------------------------------------------------------------------------
        
        The decision procedure implemented in this software is covered by
        United States Patent No. 12,254,082 (granted 2026-03-18, expires 2044-07-17),
        assigned to IDNI, inventor Ohad Asor. Public prior art: arXiv:2407.06214
        ("Guarded Successor: A Novel Temporal Logic").
        
        Royalty-free patent grant:
          IDNI grants a non-exclusive, worldwide, royalty-free license to the claims
          of US Patent 12,254,082 for the purpose of creating, using, and distributing
          implementations of the "Formal Policy Semantics for HTTP 402 Agentic Payments"
          RFC (see docs/rfc/), provided that such implementations:
            (a) are licensed under GPL-3.0-or-later or a compatible OSI-approved
                open-source license;
            (b) conform to the normative (MUST-level) requirements of the RFC as
                measured by the published TTI conformance battery; and
            (c) preserve this NOTICE in source distributions.
        
        Implementations that do not meet conditions (a)-(c) above require a commercial
        license (see section 2 above). This grant is revocable only for patent
        aggression as defined in standard open-invention-network terms.
        
        --------------------------------------------------------------------------------
          TRADEMARKS
        --------------------------------------------------------------------------------
        
        "Tau Language", "tau-lang", "tau-x402-cage", and "IDNI" are trademarks of IDNI.
        The GPL license does not grant trademark rights.
        
        --------------------------------------------------------------------------------
          NO WARRANTY
        --------------------------------------------------------------------------------
        
        THIS SOFTWARE IS PROVIDED "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES,
        INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
        FITNESS FOR A PARTICULAR PURPOSE, ARE DISCLAIMED. IN NO EVENT SHALL IDNI OR
        ITS CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
        EXEMPLARY, OR CONSEQUENTIAL DAMAGES ARISING IN ANY WAY OUT OF THE USE OF THIS
        SOFTWARE.
        
        For a human-readable summary of GPL-3.0-or-later obligations see:
          https://www.gnu.org/licenses/quick-guide-gplv3.html
        
Project-URL: Homepage, https://github.com/Jme-Tau/tau-x402-cage
Project-URL: Repository, https://github.com/Jme-Tau/tau-x402-cage
Project-URL: Issues, https://github.com/Jme-Tau/tau-x402-cage/issues
Keywords: x402,agentic-payments,formal-verification,policy-enforcement,tau-language,mpp,http-402
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Financial and Insurance Industry
Classifier: License :: Other/Proprietary License
Classifier: Operating System :: MacOS
Classifier: Operating System :: POSIX :: Linux
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Security
Classifier: Topic :: Software Development :: Libraries
Classifier: Typing :: Typed
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: LICENSE-APACHE-2.0
Provides-Extra: dev
Requires-Dist: pytest>=8.0; extra == "dev"
Requires-Dist: pytest-cov>=5.0; extra == "dev"
Requires-Dist: ruff>=0.6; extra == "dev"
Requires-Dist: black>=24.0; extra == "dev"
Requires-Dist: build>=1.0; extra == "dev"
Requires-Dist: twine>=5.0; extra == "dev"
Requires-Dist: fakeredis>=2.20; extra == "dev"
Requires-Dist: redis>=5; extra == "dev"
Provides-Extra: client
Requires-Dist: tau-x402-cage-client; extra == "client"
Provides-Extra: saas
Requires-Dist: fastapi>=0.110; extra == "saas"
Requires-Dist: uvicorn[standard]>=0.27; extra == "saas"
Requires-Dist: httpx>=0.27; extra == "saas"
Requires-Dist: jinja2>=3.1; extra == "saas"
Provides-Extra: tau
Provides-Extra: fragment-v2
Requires-Dist: z3-solver>=4.12; extra == "fragment-v2"
Provides-Extra: signing-ed25519
Requires-Dist: cryptography>=42; extra == "signing-ed25519"
Provides-Extra: signing-policy
Requires-Dist: cryptography>=42; extra == "signing-policy"
Provides-Extra: signing-yubikey
Requires-Dist: cryptography>=42; extra == "signing-yubikey"
Requires-Dist: yubikey-manager>=5.0; extra == "signing-yubikey"
Provides-Extra: signing-ledger
Requires-Dist: ledgerblue>=0.1.40; extra == "signing-ledger"
Requires-Dist: cryptography>=42; extra == "signing-ledger"
Provides-Extra: signing-trezor
Requires-Dist: trezorlib>=0.13.9; extra == "signing-trezor"
Requires-Dist: cryptography>=42; extra == "signing-trezor"
Provides-Extra: history-redis
Requires-Dist: redis>=5; extra == "history-redis"
Provides-Extra: sync-redis
Requires-Dist: redis>=5; extra == "sync-redis"
Provides-Extra: rate-limit-redis
Requires-Dist: redis>=5; extra == "rate-limit-redis"
Provides-Extra: metrics
Requires-Dist: prometheus-client>=0.20; extra == "metrics"
Provides-Extra: webhooks
Provides-Extra: grpc
Requires-Dist: grpcio>=1.60; extra == "grpc"
Provides-Extra: grpc-dev
Requires-Dist: grpcio>=1.60; extra == "grpc-dev"
Requires-Dist: grpcio-tools>=1.60; extra == "grpc-dev"
Provides-Extra: auth-jwt
Requires-Dist: pyjwt[crypto]>=2.8; extra == "auth-jwt"
Provides-Extra: demo-onchain
Requires-Dist: web3>=6.15; extra == "demo-onchain"
Requires-Dist: eth-account>=0.11; extra == "demo-onchain"
Requires-Dist: python-dotenv>=1.0; extra == "demo-onchain"
Provides-Extra: all
Requires-Dist: pytest>=8.0; extra == "all"
Requires-Dist: pytest-cov>=5.0; extra == "all"
Requires-Dist: ruff>=0.6; extra == "all"
Requires-Dist: black>=24.0; extra == "all"
Requires-Dist: build>=1.0; extra == "all"
Requires-Dist: twine>=5.0; extra == "all"
Requires-Dist: fastapi>=0.110; extra == "all"
Requires-Dist: uvicorn[standard]>=0.27; extra == "all"
Requires-Dist: httpx>=0.27; extra == "all"
Requires-Dist: jinja2>=3.1; extra == "all"
Requires-Dist: z3-solver>=4.12; extra == "all"
Requires-Dist: cryptography>=42; extra == "all"
Requires-Dist: redis>=5; extra == "all"
Requires-Dist: prometheus-client>=0.20; extra == "all"
Requires-Dist: grpcio>=1.60; extra == "all"
Requires-Dist: grpcio-tools>=1.60; extra == "all"
Requires-Dist: pyjwt[crypto]>=2.8; extra == "all"
Requires-Dist: web3>=6.15; extra == "all"
Requires-Dist: eth-account>=0.11; extra == "all"
Requires-Dist: python-dotenv>=1.0; extra == "all"
Requires-Dist: yubikey-manager>=5.0; extra == "all"
Requires-Dist: ledgerblue>=0.1.40; extra == "all"
Requires-Dist: trezorlib>=0.13.9; extra == "all"
Dynamic: license-file

<p align="center"><a href="./docs/rfc/2026-04-x402-formal-policy-semantics.md"><img src="./docs/img/banner.svg" alt="tau-x402-cage" width="100%"></a></p>

[![PyPI](https://img.shields.io/pypi/v/tau-x402-cage?color=007ec6&label=pypi)](https://pypi.org/project/tau-x402-cage/)
[![GHCR](https://img.shields.io/badge/ghcr.io-tau--x402--cage-0b7eaf)](https://github.com/Jme-Tau/tau-x402-cage/pkgs/container/tau-x402-cage)
[![CI](https://github.com/Jme-Tau/tau-x402-cage/actions/workflows/tti-gate.yml/badge.svg)](https://github.com/Jme-Tau/tau-x402-cage/actions/workflows/tti-gate.yml)
[![Tests](https://img.shields.io/badge/tests-2328%20passing-brightgreen)](./tests)
[![Patent](https://img.shields.io/badge/US%20Patent-12%2C254%2C082-111)](https://patft.uspto.gov/)
[![License](https://img.shields.io/badge/license-GPLv3%20%2F%20Commercial-777)](./LICENSE)

> [!IMPORTANT]
> **Dual-licensed.** [GPLv3](./LICENSE) for OSS + royalty-free patent grant. Commercial license for closed-source integrations. Contact [`services@idni.org`](mailto:services@idni.org).

---

## 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](https://x402.org). 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.

```mermaid
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](https://x402.org) 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](https://classic.artemis.ai/asset/x402), 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](https://aws.amazon.com/blogs/security/how-aws-uses-automated-reasoning-to-help-you-achieve-security-at-scale/) uses z3, OPA has linting, [Rego](https://www.openpolicyagent.org/) 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, optionally hash-chained.** 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. Envelopes can opt into a MAC-bound hash chain (`chain_index`, `prev_envelope_hash`) so reordering or dropping a link in an audit export also fails verification — that's the re-derivable analogue of Kevros's hash-chained action log. 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`](./docs/why_this_exists.md). Real-world incidents that inform the runtime design: [`docs/why_this_matters.md`](./docs/why_this_matters.md).

---

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

![hero demo](./demos/hero_retry_loop.gif)

```bash
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:

```json
{
  "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

```bash
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:

```bash
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](https://github.com/IDNI/tau-lang/issues/64), [#65](https://github.com/IDNI/tau-lang/issues/65), [#66](https://github.com/IDNI/tau-lang/issues/66)). The published image bundles that binary so no local Tau build is needed:

```bash
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`](./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](https://github.com/IDNI/tau-lang/issues/64)/[#65](https://github.com/IDNI/tau-lang/issues/65)/[#66](https://github.com/IDNI/tau-lang/issues/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

![corporate card](./demos/corporate_card.gif)

```bash
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](https://www.sec.gov/files/litigation/admin/2013/34-70694.pdf), [Milkie Way Cloud Run 2020 HN #25372336](https://news.ycombinator.com/item?id=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.

```mermaid
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.

```mermaid
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`](./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/guaranteed_mode_install.md), [`docs/guarantees.md`](./docs/guarantees.md), [`docs/threat-model.md`](./docs/threat-model.md), [`docs/regulatory-mapping.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` |
| Attacker reorders, drops, or rewrites envelopes in a hash-chained audit export | `chain_index` + `prev_envelope_hash` MAC-bound on every link; `verify_chain_continuity` raises `ChainError` at the tampered link | `tests/test_verdict_chain.py::TestChainContinuity` |

### 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`](./docs/threat-model.md). **Section 10** of that document names six attacker capabilities the cage explicitly does *not* defend against today, with residual-risk sizing and mitigation paths — read that before any regulated deployment.

---

## 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:

```python
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`):

```python
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`](./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`](./ts/README.md). Zero runtime deps.

---

## Documentation

| Path | Purpose |
|---|---|
| [`docs/rfc/2026-04-x402-formal-policy-semantics.md`](./docs/rfc/2026-04-x402-formal-policy-semantics.md) | IETF-style RFC draft-00 of the wire protocol |
| [`docs/guarantees.md`](./docs/guarantees.md) | 15 cataloged guarantees |
| [`docs/threat-model.md`](./docs/threat-model.md) | STRIDE-aligned threat model, 12 sections, 3 appendices |
| [`docs/regulatory-mapping.md`](./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`](./docs/mappings/x402-mapping.md) | Wire-level x402 request/response examples |
| [`docs/quickstart.md`](./docs/quickstart.md) | Zero-to-first-reject walkthrough |
| [`docs/adr/001-prover-backends.md`](./docs/adr/001-prover-backends.md) | Pattern / Tau / z3 / hybrid split and trade-offs |
| [`docs/semantic_fragment_v1.md`](./docs/semantic_fragment_v1.md) | Tau-decidable subset, encoding rules |
| [`docs/pointwise_revision.md`](./docs/pointwise_revision.md) | Revision model, deltas, incremental compile |
| [`CHANGELOG.md`](./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`](./docs/tau_witness.md).

---

## Status

- **Version:** 0.25.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](https://github.com/IDNI/tau-lang/issues/64) / [#65](https://github.com/IDNI/tau-lang/issues/65) / [#66](https://github.com/IDNI/tau-lang/issues/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 [`services@idni.org`](mailto:services@idni.org). Do not open public issues for credential, HMAC-key, or prover-chain vulnerabilities. PGP key on request.

---

## License

Dual: [GPLv3](./LICENSE) 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](https://patft.uspto.gov/). Inventor: Ohad Asor / IDNI.
