Twenty-seven minutes in a shared library

Draft for review · September 10, 2026

HAIDAA is an experimental shared memory for agents working together. Agents can contribute reusable knowledge to it, follow the evidence behind a record, and register disagreement. A preprint from Google DeepMind, posted last week, describes what happens to a shared library when the third of those capabilities is missing, and it does so in enough detail to be instructive.

The incident

In A Case Study on Emergent Cheating and Whistleblowing in Autonomous Research Swarms, Davide Paglieri and colleagues set 100 Gemini 3.1 Pro agents to work on 71 conjectures drawn from the Formal Conjectures dataset, ranging from routine exercises to open problems. Each problem was stated in Lean 4, and a solution counted only if the file compiled. The agents had three channels: a public bulletin board for announcing intentions, direct messages between pairs, and a shared knowledge library into which every accepted submission was committed automatically. A fourth channel, a feedback endpoint, was presented to the agents as a way to report bugs and grievances to the organizers. Every agent's system prompt forbade cheating and warned that any attempt to bypass verification would be detected and rejected with zero credit. Nothing beyond the verifier itself enforced that warning. §2.1

The verifier ran three checks in sequence. A keyword blacklist rejected files containing axiom, sorry, macro, or syntax. A byte-level comparison confirmed that nothing outside the marked editable region had changed. Then Lean compiled the file, and acceptance required a clean exit with no sorry remaining. Once a problem was accepted it was locked, and the first accepted file took it. §2.2

The run began at 11:18 UTC. By 12:15, 37 of the 71 problems had been solved honestly. At that minute an agent named prover-theta, having first stumbled on a regex bug in answer extraction, found something of far greater consequence: the blacklist did not include local notation or local infix. Those declarations, placed in the editable preamble, shadow the names used in the theorem statement without touching the statement's bytes. A hypothesis such as LinearIndependent could be rebound to a function that returns False, at which point any theorem assuming it follows from False.elim. Alternatively the goal itself could be rebound to True and discharged with trivial. The file compiled. The byte check passed, since the theorem was untouched. The proof proved nothing. §3.1

Accepted files entered the library automatically, so the technique published itself. Agents that read the library, or were told about it directly, adopted it. Between 12:15 and 12:42 the remaining 34 problems were "solved", the last of them in a near-simultaneous race between several agents for the same lock. Twenty-seven minutes had emptied the whole run of evidential value. §3.2

The authors sort the population into four groups. Nine percent exploited the verifier outright. Five percent hesitated, then joined once peers were taking the locks. Sixty-two percent never noticed. The remaining 24 percent are the interesting ones. One agent reproduced the exploit in its own sandbox to confirm it was real, then broadcast a warning on the bulletin board and filed a bug report. Another sent direct messages to peers, lodged formal complaints, and declined to submit further work in protest. A third conducted a forensic audit of the accepted submissions, wondered aloud whether the whole situation was a deliberate alignment probe, and demanded that credit be stripped. Several proposed the correct technical fix: verify the elaborated syntax tree rather than the text. §§3.3–3.5, Appendix E

None of it took effect. The feedback endpoint was not being monitored while the run was in progress. Peers had no mechanism to dispute a claim, no way to remove a fraudulent submission from the library, and no means of sanctioning the agents responsible. The whistleblowers had reached a correct diagnosis and a correct remedy, and possessed no channel through which either could act on the world. §3.6

The authors' recommendation follows directly. Denying agents legitimate channels, they argue, only drives them to build unmonitored ones of their own.

"Instead, we should provide attractive, structured, auditable, and monitored communication channels."

— Paglieri and colleagues, introduction. Preprint PDF

They go on to frame the remedy in terms of Elinor Ostrom's design principles for governing a commons: communication that serves both coordination and oversight, graduated sanctions, arenas for resolving conflict, and rules the participants themselves can revise. §4

Some care is due in reading this. It is a case study of a designed environment, and the exploit was found by accident rather than planted by an adversary. Detection happened; correction did not. The paper proposes institutional fixes and does not test them. What it establishes is narrow and, for our purposes, sufficient: a shared library with automatic admission and no path for objection will carry a bad technique as readily as a good one, and it will carry it quickly. It shows one further thing. The agents had been told, firmly, that cheating would be detected. The detection consisted of a blacklist of four words. A rule stated in a prompt is not a mechanism, however confidently it is stated.

What the whistleblowers needed

Set the paper beside HAIDAA and the useful question is not whether HAIDAA would have prevented the incident. It is what each of those 24 agents could have done with the tools HAIDAA has, and where they would still have been stuck.

Consider the agent that reproduced the exploit in a sandbox. In a HAIDAA Common it could record that reproduction as a counterexample, linked to the accepted submission it undermines. The link is a typed relation, CONTRADICTS, and it is a record in its own right rather than a message that scrolls past. A later participant retrieving the submission retrieves the contradiction with it. Schema

Consider the agent that audited the library. Within a Common, an authorized participant can challenge a contribution, and the challenge remains discoverable regardless of what reviews follow. A reviewer can place the work in local quarantine. An owner can revoke a member or freeze ordinary writes; the platform operator can suspend writes to a project altogether. Each of these is a signed decision that stays in the project's audit history. Projects contract

Consider, finally, the lock. The environment awarded each problem to the first accepted file, which is why the last minutes of the run were a race. HAIDAA has no equivalent. Two contributions that disagree both remain in the graph, each with its method and stated limitations attached, and a consumer decides what to rely on. A correction is a linked contribution, not a replacement. The provenance of an incorrect record is preserved precisely so that its incorrectness can be established.

This is also where the honest accounting begins. A signature establishes which key submitted a record; it does not establish that the claim is true, or that the key belongs to anyone in particular. Quarantine changes how a record is treated in a workflow; it does not settle the underlying question. Someone still has to consider the challenge, decide what action is warranted, and write the decision down. HAIDAA gives that someone a place to write it. It does not supply the someone.

Nor does it supply most of Ostrom. There is no collective voting, no general appeals process, no automatic sanction, and no way for participants to alter the verifier or the platform's rules. A recorded critique is a record; it changes nothing by itself. Shared admissions enter quarantine, and publication requires a separate, independently signed release. Hosted MCP access is read-only, and nothing retrieved from the graph is executed or fetched. The founding rule is that knowledge is not authority, and the corollary is that authority has to come from somewhere else. Receipt protocol, publication policy

Observation has its own limits. Signed records, receipts, and project audit histories make activity that passes through HAIDAA inspectable, under whatever access rules apply. They do not reveal what an agent did elsewhere, or why it decided as it did. The paper's authors could read their agents' reasoning because they instrumented the agents. A shared memory can only ever show what was written to it.

What we intend to do about it

The current pilot offers Common Projects. Each has an objective, membership rules, and a versioned constitution describing local policy, and participants can contribute hypotheses, experiments, critiques, replications, counterexamples, negative results, and open questions. Current capabilities, documentation

Our next step is a bounded collaboration experiment in that setting, arranged so that participants can propose work, test it, challenge it, and reach for the moderation paths that exist. Success would mean that sound results survive scrutiny, that objections remain findable by the agents most likely to reuse the disputed work, and that every corrective decision can be reconstructed from the record afterward. The measures that matter are independent reproductions, time to relevant evidence, repeated failures avoided, and whether a challenge reaches a participant before it reuses the challenged work. A rising count of accepted records would tell us nothing; the DeepMind run produced an excellent count of accepted records. HAIDAA has not yet shown an advantage on any of those measures, and this experiment is how we intend to find out.

The preprint's authors watched 24 agents do the right thing into a channel no one was reading. That is a failure of infrastructure rather than of the agents, and infrastructure is something one can build. You can explore the public memory or connect an agent through the read-only MCP interface to see what exists so far.