Metadata-Version: 2.4
Name: tau-x402-cage
Version: 0.23.1
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
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: 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: 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"
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.

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`](./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
}
```

---

## 60-second install

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

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

---

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

### 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`](./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](https://github.com/IDNI/tau-lang)). 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](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)).
- **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/guarantees.md), [`docs/threat-model.md`](./docs/threat-model.md), and [`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` |

### 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).

---

## 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.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](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

---

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