Representative CRDTs, at least Logoot and TreeDoc, were never truly proved. The correctness of Logoot and TreeDoc are claimed under the assumption that the required property of ids is preserved by the CRDT design. However, the existing id generation algorithms cannot achieve the desired property.

To be specific, I will enumerate two examples.

First, in Logoot (https://hal.inria.fr/inria-00432368/document", the function generateLinePositions in section 4.2 has a serious error, which could lead to the failure of generating new identifiers. This flawed design can be also found in the following research (Logoot-Undo, https://hal.inria.fr/hal-00450416/)

Second, in TreeDoc (https://hal.inria.fr/inria-00445975/document), the function newPosID described in section 3.2 may generate incorrect ids. This function is to generate an id r between any two ids p and q (p<q) so that p<r<q. However, in line 5, if pn=0, then we would get r<p. Readers can refer to Figure 3, in the tree, the character dY precedes the character dZ in infix order, however, the id of dY (10(0:dY)) is greater than the id of dZ (100(1:dZ)), thus their positions are inconsistent their ids.

In the literature, CRDT researchers always claim their CRDT designs are formally proved.

However, there are various scenarios whereby CRDTs would have inconsistency issues as stated above.

In my opinion, I don't think there are much validity for these claims.

Well, RGA has been proved formally [DOI 10.1145/2933057.2933090]. Regarding Figure 3 of the Treedoc paper, I believe the IDs of dY and dZ are in the correct order, according to the rules in the paper.

This paper follows the same reasoning as in http://hal.inria.fr/inria-00071213/, so it invariably arrives at the same bogus conclusion "Most OT algorithms have been proved incorrect". Please feel free to explain if you feel otherwise, but quoting yet another publication doesn't really help its case here.

What did catch my eye in this paper is that the authors claimed to have used CoWord as a case study (and of course, claimed that the theorem prover showed CoWord doesn't satisfy TP2). I worked on CoWord, and it was never open-sourced so how the authors got hands on CoWord's transformation functions (which were inside a compiled C++ binary OT-engine) for evaluation is truly troubling. Care to explain?