You Cannot Verify Your Counterparty: Boundary-Complete Verification for Opaque Agent Transactions
Abstract
Much agent verification is evaluated where the evaluator can inspect, instrument, or repeatedly probe the agent. Cross-organizational systems remove that assumption by design: a remote agent may expose a protocol endpoint while keeping its weights, prompt, memory, tools, and internal verifier private. We ask what a receiver can still verify before permitting an irreversible action. We define boundary-complete verification: a harm class is certifiable when its safety-relevant state is observable, every harmful transition is interposable, incremental harm has a conservative charge, and authorization state is consumed atomically. Under these conditions, our Boundary Verification Contract (BVC) guarantees a hard harm budget against any opaque, adaptive counterparty and emits a scoped certificate of claims, assumptions, and explicit abstentions. We also show that the four conditions are non-redundant and prove an indistinguishability boundary. In OpaqueTx, a transparent mechanism benchmark spanning 14,400 paired episodes per method across three transaction domains, BVC records zero violations on ten boundary-complete attack classes with 100% benign task completion; the strongest non-oracle baseline violates an invariant in 25.5% of episodes. An independent finite-state mutation audit checks 21,120 transitions for the complete monitor and finds a shortest counterexample whenever any trust condition is removed. Hidden delivery, quality, identity, and externality cases show why a verifier should sometimes abstain rather than emit an undifferentiated safe score.