一句话：提出五个内建收敛保证的组合子，使 CRDT 组合后天然收敛，并在 Lean 4 中形式化与实现。
CRDT 能在分布式副本间保证最终收敛，是实时编辑器、分布式数据库等系统的关键构件。然而经典 CRDT 理论并不保证收敛 CRDT 的组合仍收敛，开发者必须为每个组合重新推理收敛性，这恰恰违背了引入 CRDT 的初衷。本文提出一个面向一大类基于操作的 CRDT 的组合式框架，由 Product、MapState、Associate、Traverse 和 MapInterpretation 五个组合子构成，每个组合子都内建收敛保证，因此任何用它们组装的 CRDT 本身仍是 CRDT，收敛性由构造保证。该组合子集合无冗余，并涵盖了此前提出的组合子。作者在 Lean 4 中完整发展了框架、底层理论与证明，产出既可作为形式模型又可执行的已验证实现，并发布可复用库 Crdtlib。案例研究包括实现 Shapiro 等人的常见 CRDT、在完整应用中应用组合子，以及编码出与 Automerge 表达力相当、运行时与内存开销有竞争力的 JSON 树 CRDT，表明开发者无需为每个组合重新证明收敛。
Conflict-Free Replicated Data Types (CRDTs) are abstract data types that ensure eventual convergence among data replicas in distributed systems. As they provide convergence out-of-the-box, CRDTs have become key building blocks for highly available, collaborative, and offline-capable systems, powering applications from real-time editors to distributed databases. Adopting an individual CRDT is straightforward, but real-world software routinely requires composing them. For example, an application might store a set of counters, combining a set CRDT with a counter CRDT. Unfortunately, classical CRDT theory does not guarantee that a composition of convergent CRDTs converges, forcing developers to reason about convergence again - the very burden CRDTs were introduced to remove. In this paper, we introduce a compositional framework for a broad class of operation-based CRDTs. It assembles CRDTs from five principal combinators -- Product, MapState, Associate, Traverse, and MapInterpretation -- each with built-in convergence guarantees. Any CRDT assembled from these combinators is itself a CRDT, preserving convergence by construction. This set is free of redundancy and subsumes previously proposed combinators. We develop the framework, its underlying theory, and its proofs entirely in Lean 4, producing a single artifact that serves as both the formal model and an executable, verified implementation. Our reusable library, Crdtlib, provides implementations and proofs for every combinator and CRDT in this paper. Our case studies (i) implement common CRDTs from Shapiro et al., (ii) apply the combinators in a complete application, and (iii) encode a JSON-structured tree CRDT as expressive as Automerge, with competitive runtime and memory use. These case studies show that developers can compose CRDTs without re-proving convergence for each composite.
@article{paperbot12118,
title = {Composing CRDTs Convergent by Construction},
author = {Alexander Städing Dominguez and George Zakhour and Pascal Weisenburger and Guido Salvaneschi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839478}
}