1: \begin{abstract}

2: Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network.

3: However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood.

4: Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness.

5: In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data.

6: We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms.

7: We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours.

8: Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks.

9: Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency.

10: We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter.

11: We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.

12: \end{abstract}

13: