Carlos Baquero — Synchronizing State-Based CRDTs: Two-Party, Multi-Party, and AI-Discovered Protocols
Conflict-free Replicated Data Types (CRDTs) let replicas evolve independently and still converge, but keeping them synchronized efficiently is a problem in its own right. This talk follows a single thread from foundations to the research frontier. We start with state-based CRDTs and the observation that their states admit join decompositions, which recasts synchronization as reconciling sets of irreducible components. From there we build up reconciliation itself: first the two-party case, where digest-driven techniques such as rateless Bloom filters and invertible Bloom lookup tables transfer only what differs, saving an order of magnitude over full-state exchange; then the harder multi-party setting, where network topology and forwarding strategy reshape the trade-offs. Finally, we turn the problem on its head: instead of hand-designing these protocols, can an AI agent discover them? We show how an autoresearch loop — edit, evaluate, keep or revert over a faithful simulator — autonomously finds multi-party protocols within a few percent of theoretical bounds.
Antonio Fernandez — A Modular Event-based Framework for Concurrent Object Specification
We introduce a modular framework for specifying distributed systems that we call AMECOS. Specifically, our framework departs from the traditional use of sequential specification, which presents limitations both on the specification expressiveness and implementation efficiency of inherently concurrent objects, as documented by Castañeda, Rajsbaum and Raynal in CACM 2023. Our framework focuses on the interactions between the various system components, specified as concurrent objects. Interactions are described with sequences of object events. This provides a modular way of specifying distributed systems and separates legality (object semantics) from other issues, such as consistency. We demonstrate the usability of our framework by (i) specifying various well-known concurrent objects, such as registers, shared memory, message-passing, reliable broadcast, and consensus, (ii) providing hierarchies of ordering semantics (namely, consistency hierarchy, memory hierarchy, and reliable broadcast hierarchy), and (iii) presenting a novel axiomatic proof of the impossibility of the well-known Consensus problem.
Claudia-Lavinia Ignat — Sequence-Based CRDTs for Collaborative Editing Systems
Collaborative editing systems must support concurrent, low-latency work while maintaining a consistent shared document. This talk will briefly trace their evolution, introduce sequence-based Conflict-free Replicated Data Types (CRDTs) as a key replication mechanism for collaborative editing, and open broader perspectives on future distributed collaborative systems.
Carla Ferreira — Ensuring Invariants in Replicated Databases
Replicated databases provide availability and offline operation, but weakly consistent replicas can diverge and violate application invariants. Coordination fixes this at the cost of latency and offline work. This lecture presents two coordination-free alternatives: repairing conflicting operations by adding reparation effects (IPA, VLDB 2019) and discarding one of two conflicting operations under a programmer-defined policy (the No-Op approach, ECOOP 2025), which together guarantee convergence and invariant preservation. We develop both on a running example and compare their strengths and limits.
Carla Ferreira — Verifying Concurrent Protocols with TLA+
TLA+ lets you write down what a system is allowed to do, and TLC checks every possible behavior of a given model. A test tries some interleavings; TLC tries all of them, and shows you the exact steps when one breaks your claim. In this hands-on session, participants write a specification for a semaphore, state its mutual-exclusion invariant, and then break it three ways: a non-atomic test-and-set, a lock-ordering deadlock, and starvation. Each time, they read the counterexample TLC produces. The second half looks at safety versus liveness. The same correct semaphore can starve a process under weak fairness but not under strong fairness — liveness only holds relative to a fairness assumption. The session ends by building that fairness into the algorithm itself, instead of assuming it. The same idea sits behind every "eventually" guarantee in distributed systems: eventual delivery, eventual consistency, leader election.
Davide Frey — Byzantine Fault Tolerance: From Foundations to Current Perspectives
In 1982, Leslie Lamport and his co-authors introduced the Byzantine Generals Problem as a way to model arbitrary process behavior caused by bugs or malicious actions. Byzantine fault tolerance later received renewed attention with the emergence of blockchain systems, alongside specialized applications in security-critical computing, avionics, and spacecraft design.
This lecture will introduce the foundations of Byzantine fault tolerance, starting with the system models, fault assumptions, and communication primitives on which Byzantine-resilient protocols are built. It will review several fundamental results on reliable broadcast and consensus, highlighting the role of synchrony assumptions and resilience bounds. It will conclude with a research perspective on the use of weak agreement abstractions in Byzantine settings and on how such abstractions may enable more scalable protocols for open and decentralized systems. In particular, it will discuss how recent systems increasingly seek to avoid global agreement when weaker, more localized abstractions are sufficient.
Elisa Gonzalez Boix — CRDTs from a Programming Language Implementation Perspective
Distributed systems replicate data to improve availability, scalability, and fault tolerance. Ensuring that replicas remain eventually consistent is difficult. Current practices advocate for the use of Replicated Data Types (RDTs), which guarantee convergence out-of-the-box, e.g., CRDTs. However, using these RDTs when building distributed systems is often not trivial.
In this lecture, we look at what it means for developers to utlize CRDTs in their applications. Besides choosing an appropriate RDT design, developers need to consider implementation details such as replica discovery, memory and network usage, responsiveness to changes, and security. Moreover, building advanced collaborative applications may require custom RDTs tailored to the application's needs. That implies extending or composing existing RDTs, or designing new ones.
We will present some work building on pure operation-based CRDTs, a structured framework for designing operation-based CRDTs while avoiding issues related to unbounded metadata growth. We will discuss extensions to address implementation concerns, focusing on distribution concerns (e.g., how to discover replicas? how to use CRDTs in dynamic networks?) and memory management. Throughout the lecture, we will also revise some fundamental concepts such as reliable causal broadcasting on which pure op-based CRDTs rely.
The lecture is complemented by a lab session in which students will get hands-on experience with optimizations using Flec, a TypeScript (pure op-based) CRDT framework that features an open implementation, making it an ideal laboratory for experimenting with novel CRDT designs and implementation techniques.
Ragnar Mogk — Protocol RDTs: Programs as Replicated Data
Protocol RDTs extend the concept of replicated data types by treating programs—not just data—as the replicated entity. This approach captures both state and behaviour, enabling systems to enforce application-level correctness under weak consistency. The talk presents the foundations of Protocol RDTs and demonstrates how they enable expressive, coordination-free distributed programming.
Fernando Pedone — Is Synchrony Back? A Path to Efficient and Sustainable Replication
For decades, distributed systems researchers have treated synchrony as an unrealistic assumption. After all, how can a protocol rely on timing guarantees in a world of unpredictable networks and arbitrary delays? But what if this conventional wisdom no longer holds?
In this talk, I will revisit one of the oldest assumptions in distributed computing through the lens of modern public clouds. Drawing on an extensive measurement study across multiple cloud providers and geographic regions, I will show that communication delays are often far more predictable than commonly believed, particularly for small messages.
Motivated by these findings, I will explore what becomes possible when synchrony is treated not as a theoretical convenience, but as a practical design tool. I will illustrate these ideas with SyncPaxos, a synchronous variant of Paxos, along with several extensions that exploit characteristics of public cloud infrastructures. We will examine their performance, their robustness to timing violations, and the trade-offs they make compared to traditional partially synchronous approaches.
The talk will argue that synchrony is not a relic of textbook models, but an increasingly practical foundation for cloud-scale distributed systems. Beyond improving performance, synchronous protocols can reduce protocol complexity, eliminate costly recovery mechanisms, and enable more resource-efficient replication. In this sense, synchrony may offer a path toward not only faster but also more sustainable distributed systems.
Guido Salvaneschi — Taming the Distributed Systems Beast with Programming Languages
Distributed systems are notoriously hard to design, implement and deploy. In this talk, we argue that programming languages are a fundamental tool to tackle the complexity of distributed systems.
We first discuss concrete examples of how abstractions offered by programming languages have been fundamental in solving problems in distributed systems. Then we discuss recent research results in this area, such as abstractions for data consistency and behavioral types for distributed applications. Finally, we outlook promising research directions.
Marc Shapiro — Availability vs consistency, from CRDT to Consensus
A system is consistent if it maintains some specific invariant; e.g., "account is non-negative" or "graph is acyclic." It is available if concurrent participants never wait because of consistency conflicts; e.g., on "spend the last euro," or "add an edge."
How to maintain consistency at the minimal cost in availability? There is no universal solution. Our approach identifies general classes of invariants and associates a minimal-cost availability protocol to each.
We distinguish: (1) Local invariants, those that have no availability impact, requiring only that updates converge, e.g., by using CRDTs. (2) All-or-nothing constraints, requiring to deliver transactions atomically. (3) Implication constraints, which require causal delivery. These three classes are both available and partition-tolerant.
The remaining class, (4) TOCTTOU-sensitive updates, requires them to be applied in a total order. We present CISE, a program analysis that detects harmful TOCTTOU. We also discuss two opposing approaches to total order: a posteriori, available but at the cost of rollbacks, vs. a priori, based on consensus/coordination. Finally, we discuss how to ensure that an update is stable, i.e., known to be delivered at all replicas.
Tom Van Cutsem — Introduction to Blockchain and Distributed Ledgers
Blockchain and distributed ledger technology (DLT) are key enabling technologies for building open, resilient and secure distributed transaction processing systems. This introductory lecture will provide you with an up-to-date view on both the foundations and open challenges in the field. We will cover: the origins of Blockchain, the cryptographic building blocks of blockchains, how blockchain networks process transactions, consensus in blockchain networks: Proof-of-Work, Proof-of-Stake and BFT Consensus, “permissioned” versus “permissionless” blockchain networks, programming blockchains using smart contracts and latest trends.
