1: \begin{abstract}

2: 

3: %

4: 

5: %

6: Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts.

7: %

8: Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence.

9: Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations.

10: %

11: Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants.

12: Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalisation instead of a real-world implementation.

13: %

14: Furthermore, writing mechanized proofs is reserved to verification experts and is extremely time consuming.

15: %

16: %

17: %

18: %

19: To simplify the design, implementation, and verification of RDTs, we propose \VeriFx, a high-level programming language with \emph{automated} proof capabilities.

20: \VeriFx lets programmers implement RDTs atop functional collections and express correctness properties

21: that are verified automatically.

22: %

23: Verified RDTs can be transpiled to mainstream languages (currently Scala or JavaScript).

24: \VeriFx also provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions.

25: These libraries implement the general execution model of those approaches and define their correctness properties.

26: We use the libraries to implement and %

27: %

28: %

29: %

30: %

31: %

32: %

33: %

34: %

35: %

36: %

37: %

38: verify an extensive portfolio of 35 CRDTs %

39: %

40: and reproduce a study on the correctness of OT functions.

41: %

42: 

43: \end{abstract}

44: