The on-chain, trust-minimized counterpart to centralized custodial Agent-payment rails. Autonomous agents pay per-token for LLM API calls within on-chain spending caps their principal sets.
Status: milestone-complete, experimental. A specification plus a formally verified (bounded) reference implementation. Not a product, not infrastructure, not seeking adoption. The reference contracts are not third-party audited; do not use with real funds. The mechanism is governed by
FORMAL-SPEC.md; on any conflict with prose, the specification prevails.
An autonomous agent needs to pay for LLM API calls. Centralized custodial rails for this shipped at scale by 2026. Tessera is the on-chain, trust-minimized counterpart, for the segment that prefers self-custody and counterparty-agnosticism over a trusted intermediary. It is the minimal settlement primitive for bounded autonomy:
- The agent's funds stay in a publicly auditable on-chain escrow, never prefunded into a platform.
- Spending authority is bounded by two on-chain caps: a per-instant cap (the amount ever at risk) and a global cap (the cumulative budget; the principal re-authorizes at the boundary). The boundary is the principal's deliberate control point.
- A call's cost is settled in two segments. Input cost is pre-authorized before service against each side's own exact metering (no estimate, no lock-up); output cost is authorized incrementally in adjustable ticks during generation.
- The protocol is counterparty-agnostic (any OpenAI-compatible endpoint) and has no operator and no native token. Providers self-register through a decentralized on-chain registry; clients route trustlessly.
Integration is zero-code for the agent: point the OpenAI base URL at a
local proxy. Full design intent and problem framing: WHITEPAPER.md.
flowchart LR
A["AI agent / app<br/>(zero-code: base_url)"] --> PX["Client proxy<br/>metering + two-segment auth"]
W["Principal wallet"] -->|"deposit (≤ caps)"| E[("On-chain escrow<br/>publicly auditable")]
R[("Decentralized<br/>provider registry")] -.->|trustless routing| PX
PX -->|"input pre-auth + per-tick output auth"| V["Provider<br/>(OpenAI-compatible)"]
V -->|"claim highest signed cumulative"| E
E -.->|"bounded autonomy: per-instant + global cap"| W
Agentic payments are emerging as a category (machine-to-machine spend, agent wallets), but a large, fragmented market already exists today: thousands of independent API resellers/aggregators where users pre-fund balances into operators they cannot audit and price-shop across them. It is structurally durable for economic reasons. Access to upstream models is intermediated wherever a pricing gradient exists; reputable operators are structurally costlier, leaving a permanent low-cost long tail; and prefund-plus-opacity makes counterparty default intrinsic. In such a market trust is the scarce good, which the market cannot supply itself. Centralized custodial rails now serve much of this with convenience. Tessera targets the segment that prefers self-custody with on-chain-bounded authority, per-token settlement, and no trusted intermediary. Its success criterion is design rigor, not adoption.
| Layer | Artifact | Result |
|---|---|---|
| L3 protocol-state model checking (TLA+/TLC) | model/Tessera.tla .cfg |
Under the full adversary (Byzantine signing/over-serving, concurrent lanes, reordering/delay, withdrawal races), for SafetyInv (conservation / dual caps / bilateral metering / financial gate) + S4_RecoverableBeforeTerminal: two independent configurations (2-lane / 3-lane) exhaustively (queue drained) counterexample-free. Over 6 iteration rounds every counterexample was (a)/(c); none was a (b) design flaw. Record: model/RUNS.md. |
| L4 contract level (native solc SMTChecker) | contracts/TesseraEscrow.sol |
BMC found and fixed 2 real overflow bugs; CHC gave an unbounded inductive proof that escrow balance never exceeds the per-instant cap, cumulative spend never exceeds the global cap, settlement is monotone, and a claim never overpays; the one CHC-unproven item is discharged by the rigorous lemma L-I2 (sub-facts CHC-proven). Record: contracts/L4.md. |
| L5 end-to-end existence proof | impl/e2e.js |
The full closed loop (deploy, register, initSession, deposit, OpenAI-compatible call through the proxy, input pre-auth, bilateral metering, per-tick output auth, on-chain claim, balance closure) passes on a local EVM (EXIT=0). Record: IMPL.md. |
Calibration: L3 is strong bounded-exhaustive evidence, not an unbounded mathematical proof; the network/nonce model is a faithful abstraction; multi-channel is a design-orthogonal generalization not separately modeled. L4's core invariants are contract-level unbounded-inductively proven with the real bugs fixed; the single blind spot is discharged by a rigorous manual lemma (standard practice). No specification-level design flaw found; no unfixed model issue. The reference contracts are not independently third-party audited.
One command each (Node 20; make help lists all targets):
make install # impl/ + contracts/ deps
make e2e # L5 end-to-end existence proof
make fuzz # cross-lane I-1 conservation fuzz (the documented L4 gap)
make conformance # regenerate + self-check conformance vectors
make l4 # L4 contract compile self-check (0 errors)
make l3 # L3 TLA+/TLC model check (needs Java + model/tla2tools.jar)
make all # install + l4 + conformance + e2e + fuzzFull L4 (SMTChecker) run, solc-select recommended:
cd contracts && solc --model-checker-engine chc --model-checker-targets assert \
--model-checker-timeout 120000 --model-checker-show-proved-safe TesseraEscrow.solWHITEPAPER.md design intent (problem, positioning, scope, non-guarantees)
FORMAL-SPEC.md mechanism authority (state, transitions, invariants, adversary)
IMPL.md reference-implementation tracker (L5 PASS)
contracts/
TesseraEscrow.sol reference escrow contract (the trust root / L4 target)
TesseraRegistry.sol decentralized provider registry
MockERC20.sol demo settlement asset (not a protocol component)
L4.md L4 record + lemma L-I2; compile.js / verify.js
impl/
tessera-core.js shared primitives (tokenize / integer cost / auth digest)
proxy.js client proxy: metering + two-segment auth + routing
provider-shim.js provider side: admission gate + bilateral metering + claim
e2e.js L5 orchestration + closed-loop assertions
fuzz-i1.js contract-level cross-lane I-1 conservation fuzz
config.example.json config template (e2e regenerates config.json)
conformance/
vectors.json deterministic test vectors (pinned to spec version)
gen-vectors.js / check.js regenerate / self-check for independent implementations
README.md how to conform an independent implementation
model/
Tessera.tla / .cfg L3 model + config
RUNS.md L3 record and iteration trace
CHANGELOG.md spec version history (v0.1.0)
Makefile one-command reproduction (make help)
.github/workflows/ci.yml CI: L4 compile + L5 e2e on every push / PR
The contracts use native solc plus small scripts rather than Foundry/Hardhat.
This keeps dependencies minimal, and native solc is required for the L4
SMTChecker. An independent implementation in any stack is welcome.
- Out of scope: the security/correctness layer above settlement (prompt
injection, intent-vs-execution mismatch, service poisoning, adjudicating
whether a task was genuinely completed). These are explicit non-guarantees,
ceded by design. See
SECURITY.mdandWHITEPAPER.md. - Tron-native hardening (signature recovery, address derivation, energy,
finality-margin constraint): documented as
TRON-TODO, not done; does not block the existence proof. - No token, no operator, no commercialization, no paid promotion. These are structural preconditions of the protocol's neutrality.
WHITEPAPER.md: design intentFORMAL-SPEC.md: mechanism authority (governing)IMPL.md: reference-implementation trackermodel/RUNS.md: L3 record ·contracts/L4.md: L4 recordCHANGELOG.md: spec version historyCONTRIBUTING.md·SECURITY.md
The highest-value contribution is a counterexample to a stated invariant, or an
independent implementation of the specification. The (b)-flaw discipline is
mandatory: write the fix back into the spec, never patch around the verified
contract. See CONTRIBUTING.md.
Apache-2.0 (code and documents). See also NOTICE.
Draft, milestone-complete. All parameters (caps, tick, slack, windows, grace period) are illustrative. Any quantitative figure presented externally must be independently verified before being cited.