3 ms·Google Docs uses Operational Transformations (OT). You could try and model OT in TLA+.by theknarf 10mo agoGoogle Docs uses Operational Transformations (OT). You could try and model OT in TLA+.