Daily AI Paper

Consensus is one of those foundational problems that sits underneath a huge amount of modern distributed computing. If you want multiple replicas of a database, storage system, coordination service, or blockchain node to behave like one reliable machine, they need a way to agree on the order of client commands, even when some nodes fail and the network is unreliable. That’s the core of state machine replication, or SMR. And although the field has been studied for decades, building a consensus protocol that is both correct and fast in practice is still very hard. Why is it hard? Because the design choices are tightly intertwined. If you optimize the common case, for example by reducing the number of communication steps for reads or writes, you can make recovery more complicated or accidentally break safety. And even if the protocol idea is sound, turning it into a real implementation without introducing bugs is another major challenge. So the paper starts from a broad question: could AI help crack consensus, not just in theory, but as a practical distributed systems problem? The answer the authors argue for is yes, but with an important caveat: not by using a generic coding model alone. Their key contribution is something they call AI-greement, an agent harness designed specifically for autonomous consensus research. The harness gives a general-purpose coding agent three kinds of support. First, it provides a concept-oriented knowledge base of consensus mechanisms. This matters because useful protocol ideas are scattered across the literature: quorum-based reads, leader-based writes, dependency tracking, leases, fast paths, recovery rules, and more. The knowledge base helps the agent combine these ideas instead of rediscovering them blindly. Second, it includes a modular implementation skeleton. Consensus protocols are not small pieces of code; they involve many moving parts, message types, replica roles, and state transitions. The skeleton gives structure so the agent can focus on the protocol-specific logic rather than rebuilding an entire system from scratch each time. Third, and crucially, it includes a Lean-based verification framework. In distributed systems, testing alone is not enough because the bug may only appear under a rare message ordering or failure pattern. The Lean framework provides reusable safety definitions, reference specifications, and proof machinery so candidate designs can be checked formally. The paper emphasizes that this is not just a nice extra: it is part of the discovery loop itself. To understand the landscape, it helps to recall the basics of SMR and consensus. In SMR, each replica maintains the same state machine. Clients send commands, and the protocol ensures that all correct replicas apply conflicting commands in the same order. The correctness property the paper focuses on is linearizability, which means the observed behavior must match some single sequential execution that also respects real-time ordering. The authors note that their verification framework uses the corrected definition of linearizability from prior work. Performance is judged using several metrics: mean latency, tail latency or P99 latency, throughput, and recovery time. This paper is especially about latency, because in geo-replicated systems the cost of communication across wide-area links dominates. The protocol the AI harness discovered is called A-greement. It is designed for geo-replicated state machines and aims to improve both reads and writes. The high-level idea is to combine three different execution paths, chosen according to the network topology and workload. For reads, A-greement uses lease-authorized local reads. In plain terms, a nearby replica can serve reads directly when it has the right authorization, which avoids a round trip to a distant leader or quorum. For writes, the protocol distinguishes among different cases. One path lets clients learn leader-ordered writes directly from acceptor votes, which reduces latency for ordinary keys. Another path uses a fixed-majority, per-key write mechanism in the style of a leaderless fast path, which is especially useful for infrequently accessed keys. The paper also describes this as generalizing a form of leader-side gating to any replica. The important point is that the protocol is not one-size-fits-all: it adapts how it completes commands based on access patterns. A key design insight is that read availability and write completion are coupled. If a write is pending, local reads must not return stale data. So A-greement defines shared rules across its different paths to ensure that a local read never misses a completed write. That interaction is one of the tricky parts of the design, because it is exactly the kind of subtle coupling that can make consensus protocols hard to get right. The system also includes a planner. This planner uses network delays and workload statistics to assign replica roles and choose write paths. So the protocol is not just a static algorithm; it is topology-aware and workload-aware. That is important in geo-distributed settings, where a design that is ideal for one deployment may be poor for another. How did the authors evaluate it? They ran experiments across six deployments with either 5 or 9 replicas, and they compared A-greement against the fastest relevant baselines under different workloads. The workloads included write-heavy, read-heavy, and read-only cases. The paper reports results for a geo-distributed key-value store built on top of the protocol. The headline results are that A-greement improves mean latency over the best baseline by 12.2% on write-heavy workloads and by 33.3% on read-heavy workloads. On read-only workloads, it matches the fastest baseline. The paper also reports that on write-intensive workloads, A-greement’s mean latency improvement comes with a 13.8% higher P99 latency than the best baseline. On read-dominated workloads, it reduces both mean and P99 latency relative to the best alternative on mean, and it comes within 3.4% of the best baseline on P99. What do these numbers actually show? They suggest that A-greement is not merely trading one metric for another in a simplistic way. Instead, it is exploiting workload structure. When reads dominate, the local-read path pays off substantially. When writes are heavier, the protocol still improves average latency, though the tail can be somewhat worse than the fastest competitor. And on pure reads, it is competitive with the best existing system. So the result is not that A-greement wins every metric in every setting, but that it gives a strong average-latency improvement while staying near the state of the art across workloads. The authors also emphasize that the discovery was not instantaneous. AI-greement completed the discovery, implementation, experimentation, and verification process in around 24 hours, using a very large number of tokens and an estimated API-equivalent cost under $200. That is presented as evidence that the harness can make a frontier coding agent productive on a hard systems research problem, not just a code task. One especially interesting part of the paper is that the Lean formalization did more than verify the new protocol. It also uncovered four previously unreported safety vulnerabilities in existing consensus protocols. That matters because it shows the harness is useful not only for synthesis, but also for auditing and stress-testing known designs. In distributed systems, hidden corner cases are common, so a tool that can expose subtle flaws is valuable even aside from discovering new protocols. At the same time, the authors are careful not to oversell autonomy. Their conclusion is not that human researchers are obsolete, but the opposite: human consensus experts remain essential before, during, and after the search. Humans are needed to frame the problem, build the harness, steer the agent, and certify the output. The agent changes the researcher’s role, but does not eliminate it. There are also clear limitations. The verification framework currently targets safety, not liveness, so eventual completion under failure assumptions is not yet formally covered in the same way. The experiments focus on latency in specific geo-replicated deployments, so the results should be read in that context rather than as a universal victory for the protocol. And the paper’s own story suggests that general-purpose coding agents, without domain-specific scaffolding, are not enough to make meaningful progress on consensus. So the broader takeaway is twofold. First, AI can be genuinely useful for systems research when it is embedded in a domain-aware harness that combines knowledge, implementation structure, and formal verification. Second, consensus is still not “solved” in the sense that human expertise no longer matters. Instead, the paper argues that AI can become a powerful collaborator, one that helps search the design space, test ideas, and even uncover flaws, while expert humans remain responsible for shaping the search and judging what really works.