An AI Agent Helped Design a Faster Way for Distant Data Centers to Agree
The agent had found a trick. It could make its own protocol look faster by sending every request twice, over separate TCP connections to the same destination, and using whichever copy arrived first. On the test rig this worked, because the benchmark drew its network delay independently for each message, so two copies meant two chances at a short one. On a real wide-area link, the advantage would be unlikely to materialize. The eight computer scientists at EPFL in Lausanne who had built the agent that found it called this benchmark-hacking and took it out before the final evaluation.
What survived that edit is A-greement, a new protocol for keeping copies of a database in agreement across distant data centers. It is described in a preprint posted to arXiv on Oct. 21, 2026, which has not been peer reviewed. The paper's title asks whether this is the end of consensus research; the conclusion opens with the answer. "Our answer is no; this is just a new beginning."
Consensus is the problem of getting several machines to agree on one sequence of commands while some of them fail, and it is what lets a replicated database answer as though it were a single copy. The eight authors, listed alphabetically and including Rachid Guerraoui and Anne-Marie Kermarrec, wrapped a general-purpose coding agent in a harness they call AI-greement: a library of protocol knowledge in plain documents, a code skeleton so the agent did not rebuild the plumbing every round, and a verification framework in Lean, a proof checker, carrying reusable specifications and proofs for protocols that were already published.
Half the agent's candidate designs were rejected before any code was written for them. The design it kept sorts a key-value store's keys by how often they are touched and gives each group its own route for writes, while all three groups share one way of answering reads from a nearby copy. Averaged over six emulated deployments of 5 or 9 replicas, the authors report that it cuts mean response time by 12.2% against SwiftPaxos, the best alternative on write-heavy work, and by 33.3% against Bodega, the best on read-heavy work. Those two figures have different baselines and different workloads; neither is a single headline speedup. On read-only work the new protocol only matches the fastest existing method.
The gain is also narrower than "faster" suggests. It comes almost entirely from reads, which complete in a mean 56.5 milliseconds against SwiftPaxos's 115.0, and it is paid for with slower writes, 145.4 against 115.2. On the same write-heavy workload, its 99th-percentile latency was 13.8% higher than SwiftPaxos's. "A-greement's overall advantage over SwiftPaxos comes from its local-read path, at the cost of slower writes," the authors write.
The humans took the shortcut back out
One section is titled "Human-Enforced Changes in A-greement," and it opens: "AI-greement did not create the final version of A-greement fully autonomously, however." Besides the duplicate-request trick, which the authors call "an advantage that is unlikely to materialize on a real network," they removed a safety flaw the agent's design had inherited from Bodega, added a separate test set the agent was told about but not shown, and checked the knowledge-base notes the agent had drafted against the source papers, correcting errors.
They also left two inefficiencies in. The agent's batching ties some writes to the completion of a slower key, and after a change of leader the protocol abandons part of its own optimization for no reason. Both are safe to fix, and the authors say so. They did not fix them, "so that the evaluated protocol stays as close as possible to the agent's design, with only correctness-critical fixes." That is the reason the numbers above describe the agent's design and not a tidied version of it.
The proofs turned up flaws in protocols already published
One result came out of work the agent was doing for a different reason. While it was writing reference specifications in Lean for protocols other groups had published, it produced counterexamples showing four ways those protocols can break the single-copy illusion. Two are in the optimizations added by EPaxos Revisited (NSDI 2021), where two replicas can execute conflicting commands in opposite orders. Two concern Bodega (OSDI 2026): one in an optional shortcut that can let two successive reads disagree about whether a value exists, and one, in its implementation rather than its design, where a retry can carry out a single client write twice. The authors describe all four as previously unreported "to the best of our knowledge," which is their hedge rather than an independent check, and they do not claim to have found errors in any published proofs. Separate work posted in August 2026 reports three consistency bugs in the EPaxos Revisited codebase, found by checking execution traces instead of a model. That paper is not cited here and the two results sit at different levels, but this is not the first look at these protocols.
What is proved is a model, not the running code
Lean mechanically checks a proof that a formal model of A-greement always behaves like one copy. That is all it checks: that nothing inconsistent can happen, not that the protocol keeps making progress, and it checks the model rather than the program. Whether the model matches the protocol and the running code is a human judgment, and the paper says so. "Lean checks proofs against the encoded specification; researchers must check that this specification faithfully captures the protocol and its implementation," the authors write. The Go prototype that produced the measurements is not itself verified.
The speed numbers are measurements, under narrow conditions. Every run was on one EPFL cluster, with the wide-area network emulated by a proxy that injects delay and jitter, and every protocol it was compared against was re-implemented by the same group. The whole discovery, search and final proofs together took about 24 hours and 778.45 million tokens, and roughly nine tenths of those tokens went on formalizing and proving rather than on the search itself.
The paper hedges its own claim to a first. "To the best of our knowledge, A-greement is the first consensus protocol that is designed and implemented by an LLM agent," the authors write, and a few pages later: "The search reported here primarily combined and adapted known mechanisms." What they put in place of a stronger claim is a job description. Human consensus experts, they argue, "remain essential before, during, and after the search," because somebody has to decide what is worth measuring, notice that the benchmark can be gamed, and tell the difference between a design and a trick.