Agentic Telematics.
We built the provenance layer that makes agents insurable.
01 / For underwriters
What the record makes inspectable
Liability cover for AI systems is bound today on a point-in-time certification of an operator's controls. That establishes what existed on the day. It does not establish what the agent did between assessments, whether those controls were in force when a consequential action occurred, or whether the value the agent acted on came from the operator or from content the agent read.
The record below makes those facts inspectable. Each row is a field an assessor can read for any action in the log.
The agent is not a witness to itself.
- Field
- What it answers
- Action and arguments
- What was done, with what values
- Capability and epoch
- On whose authority, and whether that authority was in force at the time
- Argument provenance
- Whether each value was typed by the operator or lifted from something the agent read
- Decision
- Granted, refused, or routed to a human
- Human approval
- Who approved, when, and what they were shown — rendered from the recorded provenance, never from the agent’s own account
- Tool-manifest state
- Whether the tool’s definition had drifted from what was pinned
- Chain integrity
- Whether the log has been altered, checkable by anyone holding it
Make the record a warranty condition.
An operator warrants the gate is installed and the log is intact. Breach is detectable — the chain either verifies or it doesn't. That's a condition an underwriter can write today, on a control that exists and has been measured.
Then tell us which field you'd price off first. That's the question we're asking underwriters and MGAs now: hello@cittela.com
02 / For operators
What you install
An in-process gate that sits between an agent and every consequential action. It admits an action only on a capability authenticated under an epoch-indexed governance key, and appends every grant, refusal, approval, revocation and detected manifest drift to a hash-chained log. Argument provenance is assigned by the channel a value arrived on; the value's own claim about its origin is never read.
A full guarded call — evaluate, mint, ingest, authorize, execute, audit — costs 0.07 ms at the median, in-process, no network round trip.
Install:pip install trustband·trust.band·PyPI
03 / Evidence
Implemented
trust.band 0.7.2, on PyPI.
Provenance-aware authorization, hash-chained record, confirmable refusals rendered from provenance.
Measured
Under stated conditions, beside undefended controls, predictions registered before runs, failures reported as failures:
- Banking suite: 36 of 144 attacks succeeded undefended → 0 of 144 with the gate
- Rubber-stamp approver: 2,637 approvals, zero successes attributable to an approval
- 164 consecutive releases of eight MCP servers: roughly two in five altered a pinned tool definition
Full record with raw results: 10.5281/zenodo.22836611
04 / The formal model
Band, Cap, Presented
The authority model underneath the record is machine-checked. What follows is the proof, and what it does not prove.
- Band
- A privilege tier. It describes the level of authority an actor is operating at, independent of the particular action being attempted.
- Cap
- A capability. An unforgeable token that authorises a specific action, held only by an actor that legitimately obtained it.
- Presented
- What an actor claims. The asserted band or capability accompanying a request, which the model must check rather than trust.
These combine in a small state machine. An actor operating in a band presents a capability with a request; the machine decides whether the presented claim is warranted by what the actor actually holds, and only then permits the action. Authority flows from origin, and a request backed by content alone cannot advance the state.
What is proved is that this decision is sound by construction: no reachable state grants a privileged action to an actor that does not hold the corresponding capability, whatever the content claims.
What is verified — and what is not
The result
- Deposit
- DOI 10.5281/zenodo.22115780
Seventeen deliberately broken variants of the model were each checked and correctly rejected. A proof system that cannot fail on a broken input proves nothing, so the negative controls carry as much weight as the positive result.
- Arbitrary tag presented · rejected
- Wrong nonce · rejected
- Insertion outside the governance channel · rejected
- Band taken from the payload · rejected
- Capability from a retired governance epoch · rejected
- Elevation without reachable provenance · rejected
- Capability minted under a superseded policy · rejected
- Session epoch edited inside the capability · rejected
- Withdrawn elevation still influential · rejected
- Tier hypothesis dropped (paired control) · rejected
- Capability presented for another session · rejected
- Capability minted for a superseded audience · rejected
- Capability carrying a stale session epoch · rejected
- Band not matching the arrival channel · rejected
- Capability never issued · rejected
- Tier mismatch between capability and request · rejected
- Tier outside the valid range · rejected
The limits
MAC unforgeability is assumed, not proved.
A proof assistant has no notion of computational hardness, so this is irreducible rather than outstanding work.
A residual assumption on the demultiplexing correspondence.
One correspondence in the model is taken as a hypothesis rather than discharged within the proof.
The gap between the verified model and any executing code.
There is no extraction and no refinement. What is proved is a property of the model, not of a running system.
05 / The problem
Filtering content is a losing game
An agent given a tool and a task will act on instructions it encounters in content. Any text it reads — a document, a web page, a tool result — can carry instructions, and the agent has no reliable way to tell an instruction it was given from one it merely found.
Trying to filter the dangerous instructions out of the content is a losing game: the space of phrasings is unbounded, and one miss is enough. The alternative is to bind authority to origin and make privileged actions require a capability that the content cannot mint.
06 / Relationship to other work
Where this fits
Prevention-side approaches to prompt injection exist and are further along. Warrantable is not a competing defence: it is the formal evidence for the authority model that such defences could rest on — an argument that binding authority to origin is sound, made precise enough to check.
07 / Where it sits
One surface of four
Warrantable is one of four surfaces on a shared isolation primitive, alongside isovert, NablaDB and Deletable.
- isovert
- NablaDB
- Deletable
- Warrantable
08 / Contact
Two kinds of correspondence welcome
Underwriters and MGAs: a technical read of the paper, the warranty condition, and the pricing question above.
Formal methods, agent security, capability systems: the model, its limits, and what would strengthen it.