[theknarf]

Google Docs uses Operational Transformations (OT). You could try and model OT in TLA+.