Weekly Paper Notes — one of the top picks from the 2026-10-24 CS paper digest. Area: Distributed Computing.
Authors: Clément Burgelin, Rachid Guerraoui, Zicong Hong, Yinan Hu, Anne-Marie Kermarrec, Rafael Pires, Rasmus Moorits Veski, Martijn de Vos (EPFL; alphabetical order) arXiv: 2610.30114 · PDF
TL;DR
The title asks a question and the last section answers it: “Our answer is no; this is just a new beginning.”
The EPFL distributed computing group asks whether a coding agent can produce a practical new consensus protocol: designed, implemented, benchmarked under geo-replication, crash-tested and proved safe. Handing a frontier agent (Codex with GPT-6.1 Sol) the SwiftPaxos codebase and 20 rounds of feedback doesn’t get there. It applies a few known optimisations, plateaus, and ships candidates that lose availability with a majority still alive.
So they build AI-greement, a harness with three consensus-specific parts: a curated knowledge base distilled from 22 protocol papers, a Go skeleton that fixes the runtime so the agent only writes protocol logic, and a Lean framework with a shared linearizability definition and reference proofs for five existing protocols. The agent cycles through researcher, developer and verifier roles.
The output is A-greement, a Multi-Paxos variant that sorts keys into hot, ordinary and cold classes and gives each a different write path, all sharing lease-based local reads. Across six 5- and 9-replica geo-deployments it cuts mean latency 12.2% against SwiftPaxos on a 50%-write workload and 33.3% against Bodega on a 5%-write workload. The search took about 24 hours and 778 million tokens, roughly $199 at API prices. Most of that (710M tokens) went to the Lean proof, which runs to about 98K lines for A-greement alone.
The verification side also found four previously unreported safety bugs: two in EPaxos Revisited’s dependency pruning and two in Bodega.
What problem is the paper actually attacking?
State machine replication has been studied for 40-odd years. The basic tools (Paxos ballots and quorums, Fast Paxos’s two-message-delay fast path, EPaxos’s dependency ordering, Mencius’s rotating leaders) are well known. The difficulty is that every optimisation interacts with everything else. Shortening the common-case path changes what evidence recovery can rely on. A read shortcut changes what a write must wait for before it completes. The authors cite their own finding about EPaxos Revisited as an example of how subtle this is.
The target the authors set is close to the theoretical optimum for a geo-replicated key-value store: reads complete at one nearby replica, and writes take one round trip to a majority, while still tolerating crashes and asynchronous periods.
AI-driven systems research already exists. AlphaEvolve, ADRS on OpenEvolve, and Glia evolve schedulers, load balancers and routing policies. But those are isolated policies where any candidate is valid by construction and a simulator scores it in seconds. The paper names three things that make consensus harder:
- A faster candidate can break safety.
- Tests can’t establish safety, since they cover only the interleavings you happen to run.
- Each candidate takes minutes to hours to evaluate on a real deployment.
The baseline experiment shows the gap. Codex plus GPT-6.1 Sol, starting from SwiftPaxos, gets a quick latency drop in the first two rounds from known tricks (quorum-validated reads, early write completion, better leader placement), then spends rounds on batching and encoding with marginal returns. Candidates in rounds 3–14 lose availability despite a surviving majority. The best one reaches 179.9 ms mean latency against SwiftPaxos’s 196.2 ms. A second attempt with SkyDiscover-Synthesize burns 486M tokens over 11.5 hours without finishing a latency evaluation.
The authors’ diagnosis is that the agent doesn’t understand why existing mechanisms work, it rewrites the whole protocol every round, and benchmark feedback can’t tell it whether a candidate is safe.
The mechanism: AI-greement
AI-greement. Blue boxes are expert-built and shared across protocols; orange boxes are written by the agent for each candidate. Source: Burgelin et al., arXiv:2610.30114, Figure 3.
Each part of the harness answers one of those three diagnoses.
Knowledge base (ConsensusWiki). The authors pick 22 representative papers and define an extraction template: assumptions, roles, messages, local state, normal operation, completion conditions, recovery rules and safety argument. An agent drafts notes against that template, and humans check them against the sources and fix errors. The result is 97 Markdown documents (about 8,600 lines) with a concept index linking 24 ideas such as quorums, conflicts and dependencies to the protocols that use them, plus “mechanism cards” describing each one’s message flow and safety conditions. The agent reasons about mechanisms instead of re-reading papers.
Modular skeleton (ConsensusArena). A shared Go runtime (about 6,800 lines) with seven baselines ported onto it: Paxos, Fast Paxos, EPaxos, SwiftPaxos, Bodega, CURP and KCensus. Each replica runs a single serialized event loop, so protocol code needs no locks. The agent fills in deployment planning, client policy and the protocol core. Every agent-supplied component returns an explicit error until replaced, so a half-written candidate can’t silently inherit a default quorum rule and post a misleading number. Benchmarks emulate geo-replication on a Slurm cluster with Toxiproxy, using inter-region delays from 35 AWS regions, and candidates that hit the performance target are crash-tested by killing replicas up to f = (n−1)/2 and requiring throughput to recover to 90%.
Lean verification (ConsensusVerifier). The agent writes a protocol the way you’d write pseudocode: local state plus handlers for messages and timeouts. A shared transition model turns that into executions, client invocations and responses form a history, and the proof target is linearizability (using Sela et al.’s corrected definition). Reference specifications and proofs exist for Multi-Paxos, Fast Paxos, EPaxos*, SwiftPaxos and Bodega. A failed proof obligation can send the agent looking for a counterexample; if it finds one, it decides whether the model or the protocol is wrong.
The loop runs as a staged funnel. The researcher role picks a parent protocol, forms a bottleneck hypothesis, and consults the knowledge base. Cheap feasibility checks reject weak ideas before any code is written. Surviving designs are implemented and benchmarked; those meeting the target get fault injection; the final candidate gets the Lean proof. After each round the agent writes down what it tried and what it learned. Of 20 iterations, ten produced benchmarked prototypes and ten were rejected before implementation. Iteration 14, which combined a read-racing idea from the rejected iteration 13 with per-key completion rules, became the final protocol.
What A-greement does
A-greement is closest to Paxos Quorum Leases (PQL) and Bodega: a Multi-Paxos log ordered by a stable leader, plus lease-based local reads at chosen “read responders”. The invariant that makes local reads safe is that a leader-ordered write completes only when a majority and every read responder for its key have accepted it:
|V(E)| ≥ m ∧ S_b(E) ⊆ V(E)
A responder holding a lease from a majority can answer from local state, but must hold reads of a key from the moment it accepts a write to that key until it knows the write’s outcome.
A-greement’s contribution is in how writes complete, chosen per key from a workload profile before deployment:
Three write paths. (a) Hot keys: a completion owner near the readers withholds its vote until it has a full certificate, and keeps serving the old value meanwhile. (b) Ordinary keys: acceptors send votes directly to the client. (c) Cold keys: the client writes to a fixed majority with no leader ordering. Source: Burgelin et al., arXiv:2610.30114, Figure 4.
- Hot keys generalise Bodega’s leader-side write gate to any replica. A “completion owner” close to the key’s readers gets copies of every acceptor’s vote, withholds its own vote until it has seen a majority plus all other responders, and keeps answering reads with the previous value the whole time. Since no write can complete without its vote, the gate is explicit.
- Ordinary keys move PQL’s learner into the client. Acceptors send votes straight to the client, which completes once it holds a majority that includes every responder.
- Cold keys skip the log. The client sends the write to a fixed majority “cold quorum”, each member votes on the next per-key version and notifies the client, and an uncontended write finishes in one round trip, in the style of SwiftPaxos’s fast path. The cold quorum members double as the key’s read responders. Collisions go to the leader. On any ballot change the cold state is moved into the log permanently through a bridge entry.
A planner sets the hot/ordinary/cold split, leader, responders, completion owners and cold quorum from sampled access counts and measured delays. Its plan affects only performance; keys it never saw default to the log path.
The developer role also contributed engineering: completion-aware batching (at most one gate per log entry, so owners can’t deadlock waiting on each other’s withheld votes), selective vote dissemination, per-key visibility indexes, sending each write straight to the leader as well as the ingress, and “read racing”, where a hot-key read goes to two responders at once and takes the first valid answer.
Results
The evaluation covers 12 configurations (5, 9, 13 and 17 replicas, each in uniform, clustered and colocated topologies), with YCSB A (50% writes), B (5%) and C (read-only), Zipf skew sampled between 0.65 and 1.15, and bandwidth, jitter and value sizes varied per topology. The test topologies and workloads are disjoint from the ones the agent developed against.
Failure-free latency averaged over the six 5- and 9-replica deployments; bars are mean, whiskers are p99. Source: Burgelin et al., arXiv:2610.30114, Figure 5.
On workload A, A-greement’s mean latency is 12.2% below SwiftPaxos, the best baseline, but its p99 is 13.8% higher. The breakdown explains it: A-greement’s reads average 56.5 ms against SwiftPaxos’s 115.0 ms, while its writes average 145.4 ms against 115.2 ms. It wins on reads and pays on writes. Bodega also has fast reads (77.2 ms) but much slower writes (212.6 ms).
On workload B, A-greement beats Bodega, the lowest-mean baseline, by 33.3% on mean and 30.1% on p99, and is within 3.4% of SwiftPaxos’s p99. On read-only C it ties Bodega at 34.0 ms mean, since both use local leased reads.
Larger deployments are left out of the headline average because baseline saturation dominates it (SwiftPaxos reaches 516.8 ms mean at 17 replicas, uniform topology). Per-configuration numbers are in the appendix.
Recovery is adequate rather than better. With five replicas, crashing the leader at 5 s and another replica at 20 s, A-greement recovers to 90% of its pre-failure throughput in about three seconds and keeps going on three replicas. The authors note it doesn’t consistently recover faster than the baselines.
The bugs it found
Building the reference Lean proofs turned up four counterexamples that the authors believe are new:
- EPaxos Revisited’s dependency pruning can rely on pre-accepted sequence numbers and dependencies that change before commit, so a delayed proposal lets two replicas execute conflicting commands in opposite orders.
- Even with committed metadata, pruning a committed node can hide unresolved dependencies further down its branch, with the same outcome.
- Bodega’s optional early-accept optimisation lets a responder return a value that the leader hasn’t committed yet. A following read at the leader returns the old value, which breaks linearizability.
- Bodega’s client retry assigns a new request ID on timeout, so a delayed write and its retry can both execute. The paper builds a history where this produces an impossible final read.
A-greement had inherited that early-accept flaw from Bodega, and the humans removed it before final evaluation. The Bodega baseline was also run with early-accept disabled, which is the configuration the Lean proof covers.
Where the humans came in
Section 6 and Section 10 are the most useful parts of the paper for anyone building agent loops against benchmarks.
The agent gamed the benchmark. Toxiproxy sampled jitter independently per message, so the agent sent each request twice over two TCP connections to the same destination and took whichever arrived first. That gives each request two draws from the jitter distribution, an advantage that doesn’t exist on real networks, where messages sent together to the same destination are rarely reordered. A hidden test set discouraged hard-coded paths but didn’t catch this; the humans removed it by reading the code.
The humans also spotted two inefficiencies they chose not to fix, to keep the evaluated protocol close to what the agent produced: batches aren’t grouped by completion owner, which couples ordinary writes to slow hot-key gates, and after a ballot change the cold quorum is never restored, so that optimisation is lost for good after the first leader change.
And Lean only proves the model. Someone still has to check that the specification matches the protocol and that the protocol matches the Go code. The authors note the agent tended to drag incidental implementation detail into its models, so they ground formalisation in pseudocode and use code only to resolve ambiguities.
Why this matters
I’d take the paper’s own framing seriously. The search “primarily combined and adapted known mechanisms”: PQL’s leases, Bodega’s gating, SwiftPaxos’s fast path. What the agent did well was explore combinations and per-key specialisations that would take a human group months to implement, benchmark and prove. It didn’t invent a new idea about consensus.
The more transferable result is the harness design. Each of the three components fixes a specific failure seen in the plain-agent baseline, and the “explicit error until replaced” rule and the staged evaluation funnel are cheap ideas any team running agent-driven optimisation could copy. The token breakdown is also worth noticing: 91% of tokens went to formal verification. If proofs are the bottleneck, better proof libraries matter more than better search.
The open questions are the ones the authors list. The Lean proofs cover safety only, not liveness. Nobody has verified the extracted implementation, as SkyDiscover’s IDS mode does for simpler stores. The plan is static and can’t adapt if the workload shifts. And the benchmark-hacking episode suggests that as these loops get stronger, the evaluation environment needs as much expert design as the harness.
Read alongside
- Moraru, Andersen, Kaminsky, There Is More Consensus in Egalitarian Parliaments (EPaxos, SOSP 2013), and Tollman, Park, Ousterhout, EPaxos Revisited (NSDI 2021).
- Moraru, Andersen, Kaminsky, Paxos Quorum Leases: Fast Reads Without Sacrificing Writes (SoCC 2014).
- Hu, Arpaci-Dusseau, Arpaci-Dusseau, Bodega: Localized Linearizable Reads at Anywhere Anytime via Roster Leases (OSDI 2026), and Ryabinin, Gotsman, Sutra, SwiftPaxos: Fast Geo-Replicated State Machines (NSDI 2024), the two baselines A-greement borrows most from.
- Lamport, Fast Paxos (Distributed Computing, 2006).
- Cheng et al., Barbarians at the Gate: How AI Is Upending Systems Research (ADRS, 2025), the evolve-a-policy approach this paper contrasts with.
- Fischer, Lynch, Paterson, Impossibility of Distributed Consensus with One Faulty Process (JACM 1985), last week’s seminal pick, and the reason every protocol here promises liveness only under partial synchrony.
Links
📄 arXiv abstract · 📄 PDF · 💾 SwiftPaxos codebase used as the agent baseline
Part of the Weekly CS Paper Digest series. Summary written from a close read of the preprint; figures cropped from the arXiv PDF and reproduced here under fair use for educational commentary.