Repository logo

AMC: Towards Trustworthy and Explorable CRDT Applications with the Automerge Model Checker

Accepted version


Conference Object

Change log


Mortier, Richard 


Conflict-free Replicated Data Types (CRDTs) enable local-first operations and asynchronous collaboration without the need for always-on centralised services. CRDTs can have a high overhead, so implementations need to be optimised, but this optimisation can lead to bugs despite the use of test suites and fuzzing. Furthermore, using CRDTs in applications is complex, observing unexpected conflict resolution, issues synchronising documents and difficulties implementing appropriate data models. Automerge is a library, exposing a JSON CRDT, that sees users having difficulties in modelling their problems, understanding their edge cases and implementing applications correctly. We introduce the Automerge Model Checker (AMC), empowering application developers to check properties about their implementations and explore them dynamically. AMC can check a range of applications as well as being able to check properties about the core of Automerge itself, helping to make more trustworthy Automerge applications.



conflict-free replicated data types, distributed systems, eventual consistency, model checking

Journal Title

Proceedings of the 10th Workshop on Principles and Practice of Consistency for Distributed Data

Conference Name

10th Workshop on Principles and Practice of Consistency for Distributed Data

Journal ISSN

Volume Title


Is supplemented by:

Version History

Now showing 1 - 2 of 2
2023-11-22 09:09:38
Published version added
2023-04-12 23:30:36
* Selected version