Comment by nornagon

Designer & author of the JSON OT algorithm that underlies ShareJS/ShareDB here. I do not have a formal proof for any of the properties of the algorithm, but we have extensively fuzzed it and are confident in its correctness. I believe a proof of correctness is possible, merely tedious.