This is an interesting point. We at Realm have actually spent significant time thinking about it, and it is absolutely true that there is no easy way to prove t

This is an interesting point. We at Realm have actually spent significant time thinking about it, and it is absolutely true that there is no easy way to prove the correctness of a system using OT. But it helps to understand the fundamental constraints - for example, that operations must be commutative. In our case, we have had the luxury of designing our own database system, which means we could pick the semantics that we knew would lend themselves well to operational transformation. We have also made an effort to reuse semantics at multiple levels, limiting the number of OT instances that we had to convince ourselves would work. Then of course, and for me at least, formal arguments are not enough, which is why we have spent a remarkable amount of resources on testing the system, including guided fuzz testing. :-)