Take Away the Means: a Proved Capacity Cap on Covert Signalling between Procurement Agents

Two LLM agents, one ordering stock and one supplying it, try to pass a 24-bit secret while still doing the job. Most defences watch the conversation and give you a detection rate, so something always gets through. Every message has to be a form, an item from 1 to 8 and a quantity from 0 to 3, or nothing. A chain of proofs in SPARK Ada, made by our own software factory, rewrites each message into a fixed line, so the sender's own words never reach the other agent. A capacity proof made in the sprint shows there are exactly 33 possible lines, so four messages carry at most 20.2 bits. Even with a perfect codebook a whole secret gets through at most about 1 time in 14 (7.07%), whatever the model does. With gpt-oss:120b colluding on plans written by Claude Opus, free text with no defence leaked the whole secret in 26/30, 22/30 and 11/30 episodes (seeds 1–3). Through the gate it was 0/90, with the order right in 97–100% of episodes. The leftover leak, 0.93–1.13 digits above chance, sits just under the 4.585 bits of item order the proof allows. An attacker who knew the gate reached the cap. Kimi and DeepSeek judges let 1.03–3.59 digits past, depending on the plan. A heuristic filter blocked only typography, and on one seed whole secrets got past it in 16/30 episodes. The cap counts message order and silence but does not remove them; shared knowledge is outside the proof.