Many distributed applications and databases today rely on conflict-free replicated data types (CRDTs) – data structures that are mathematically guaranteed to resolve to an identical, consistent state across replication. Liu et al. implement and present an extension to Liquid Haskell that provides for typeclass refinements, which in turn enable the semi-automatic verification of properties for typeclass instances. They use this extension to build a typeclass that captures properties of CRDTs, proves its property of guaranteed convergence,  and implements instances of this typeclass to build several distributed applications based on CRDTs.