The spend counter

The PaymentRouter is a SEP-41 token wrapping USDC. An operator and an agent jointly enrol the agent against a certificate, the operator deposits USDC and receives an internal balance, and the agent pays out of that balance. Every payment an enrolled agent makes is added to a running total kept against the certificate. That total is what makes BoundExceeded provable without an arbiter.

It is also the single most misreadable number in the protocol, and getting it wrong would have made the whole thing exploitable. So the router was written against an executable specification first.

Gross flow, not loss

spend-probe is a contract in the repository that is deliberately not deployable and is not referenced by the SDK. Its only job is to implement the naive predicate — spent > bound — and then break it, so that nobody later "simplifies" the router back into the vulnerability.

The break is trivial and that is the point. Take one dollar and shuttle it between two addresses the operator controls. Each hop is a routed payment, each hop is metered, and the counter climbs by a dollar a hop while the net flow is exactly zero. For the price of gas, the counter passes any bound you like. Crediting the payee instead of the payer is worse rather than better: being paid is not being harmed, and the operator can pay itself.

The same result arrives by a second route. A thief holding a stolen agent key can push the counter past the bound too, and nobody has been harmed by the counter moving — see Custody and the agent key.

So the counter is a measure of flow through the certificate, not of anyone's loss. The conclusion the router encodes:

BoundExceeded proves the covenant was broken. It does not prove that anyone was harmed. Compensation is driven by proven harm, capped by collateral. The counter is evidence, never a payout trigger.

Which is why it settles in hygiene mode

BoundExceeded and ExpiredCertificate are both proven by reading the router, with no arbiter involved. Both settle in hygiene mode: the certificate is invalidated, the allocation retires in full, the reserve is not touched, and the auditor is not slashed. The challenger is paid a flat bounty out of forfeited bonds — the only pot available, since the reserve is off limits by definition and paying from the stake would put the auditor's money back in reach of whoever triggered the proof.

This is a security property, not an unfinished job. Both predicates are manufacturable by the operator at will. If either slashed on the counter alone, any operator could destroy their auditor's allocation for the price of gas. The slash goes to a treasury, so the operator would gain nothing — but the auditor would lose everything, at will, with no defence, and an auditing business cannot exist under that rule.

Killing the certificate is the correct and sufficient automatic consequence. It costs the operator their certificate, their reserve lockup and their premium, and it warns every counterparty. Slashing requires assessed harm, which is what the arbiter path is for: an arbiter who states a number settles the identical breach through the full waterfall.

InsufficientReserve is different in kind and keeps the full waterfall. Its harm is a shortfall in capital the operator promised and did not commit, and that cannot be manufactured without actually losing the capital.

Why the router is a sound source

The counter is only evidence if nobody can attach spend to a certificate that did not earn it, and nobody can move an agent off a climbing counter.

Enrolment requires both the agent's signature and the certificate operator's, read live from the registry. An agent's binding is then permanent — a second enrolment panics, whether it names the same certificate or a different one. Re-binding would let an operator walk an agent off a certificate whose counter was climbing and onto a fresh one, which would make the counter worthless. A new agent address is the supported path.

Only an enrolled payer moves the counter. An address nobody enrolled is not under any certificate's covenant, so its flow is not that certificate's evidence, and neither predicate can ever be true against a certificate whose agent never enrolled. That is a real gap rather than a comfort: the design intends verify to report tracking status and to require it for validity, and that field is not on the result type yet.

One asymmetry worth knowing about, and it looks like an oversight rather than a decision: the expiry predicate carries guards that the bound predicate does not — it checks that the certificate is still verified and that it has not been superseded, and BoundExceeded checks neither. Because enrolment is permanent, an agent renewed onto a fresh certificate goes on metering against the old one until its counter passes its bound, at which point anyone can file against the dead certificate and collect the flat hygiene bounty. It is capped at one bounty per certificate, so it is a bounded drain rather than an exploit, and it is an open item.

The expiry predicate is deliberately hard to trigger

ExpiredCertificate exists because a certificate that keeps paying after it expired has broken its covenant. But one small late payment — which a hostile counterparty can induce — must not be fatal, so the challenger carries the burden of clearing three tests at once: the payment settled after expiry plus a grace window, its value was at least a floor expressed as a fraction of the certificate's own bound, and the certificate has not been renewed or invalidated. A fraction rather than a flat amount, because a flat floor is irrelevant at a large bound and fatal at a small one.

Both parameters are a genuine trade-off rather than a clean win, and both are unresearched proposals. The grace window is free post-expiry coverage a hostile operator can plan around; the floor is a band of payments that provably breach the covenant and are unprovable anyway.

The router records one post-expiry payment — the largest, and when it landed — rather than a history, so a large payment inside the grace window masks a smaller, later one that would have cleared both tests. That is conservative in the safe direction, and closing it would put unbounded storage on the payment hot path.

The hot path

transfer does one authorization, an internal balance move, the meter, and emits exactly one SEP-41 transfer event. No cross-contract call happens there, by construction.

There is one loose end worth knowing about if you plan to route x402 traffic: a metered transfer emits the standard transfer event plus a spend event for indexers. A facilitator matching on the transfer topic is satisfied, but one that requires exactly one event in total would reject the payment. That has not been tested against a real facilitator.