Cloud services, such as iCloud, rely on complex database systems working behind the scenes to reliably store photos, notes, and files. To manage massive amounts of data, these systems split it into multiple partitions, stored at different servers. To ensure the data survives even catastrophic failures, the systems maintain multiple replicas of each partition at different geographic locations and seamlessly keep them in sync.
Apache Cassandra is a leading open-source database system that allows developing cloud services of such an extreme scale. But so far, its scalability has come at a price: Cassandra could not execute strongly consistent transactions on data across multiple partitions. This forced application developers to implement the required functionality using ad hoc, error-prone approaches. To address this challenge, Accord was born – an advanced distributed protocol collaboratively designed and verified by researchers from the IMDEA Software Institute, Apple, and Télécom SudParis. Accord will be officially integrated into the upcoming release of Apache Cassandra 6.0.
Historically, distributed database systems maintained different data replicas in sync by funneling all transactions through a distinguished “leader” replica. This created a bottleneck that increased client latency and limited scalability. Accord takes a fundamentally different approach, making it the first leaderless distributed protocol for production systems operating at a global scale. What makes Accord particularly compelling is it can often complete complex multi-partition transactions in a single network round trip between different geographical sites.
The seeds of this breakthrough lie in previous research conducted by Professor Alexey Gotsman’s group at IMDEA Software. Building upon these theoretical foundations, an international team, led on the technical side by Benedict Elliott Smith (Apple) alongside engineering colleagues, and featuring Alexey Gotsman, Fedor Ryabinin (IMDEA Software) and Pierre Sutra (Télécom SudParis), brought the algorithm to life.
However, designing an algorithm for millions of users is only half the battle: it must be mathematically proven correct, since even a minor flaw can corrupt data on a global scale. This is where IMDEA’s researchers made several crucial contributions. First, postdoctoral researcher Fedor Ryabinin wrote a hand proof of correctness, rigorously demonstrating that Accord is safe. To ensure the proof does not contain mistakes, the team then used AI to automatically formalize it in the Lean proof assistant. Intern researcher Alexandre Siret also built a formal model of Accord in the TLA+ language and simulated its behavior under adversarial scenarios.
The project has just been presented at the Community over Code 2026 conference in Glasgow, the flagship conference of the Apache Software Foundation. During the conference, the IMDEA Software team delivered two presentations: Fedor Ryabinin presented Accord’s theoretical architecture and explained how it overcomes the limitations of traditional protocols. Alexandre Siret demonstrated how TLA+ modeling enabled verifying the protocol, thus increasing the confidence in its correctness.
The arrival of Accord in Apache Cassandra 6.0 marks a milestone as the first successful deployment of a leaderless transaction protocol at production scale. In the future, the protocol will serve as a foundation for more scalable and resilient distributed databases.
