Conflict-Free Replicated Datatypes (CRDTs) are a class of distributed data structures where replica states are allowed to temporarily diverge, but will eventually converge (in the absence of network partitions). 2
Specifically, the class of CRDTs known as state-based (or convergent) achieved the above by requiring the data structure state to be drawn from a (semi)lattice (thus drawing on properties of least upper bound to achieve convergence).
Causal consistency is a consistency model where events/operations are applied in an order that is consistent with Lamport's happens-before relation. 3
Is there a formal proof that state-based CRDTs are, by construction, causally consistent?
This is hinted at in this paper 4, but without a full proof (or a full theorem statement, for that matter):
