Collaborative text editing with RGA30 July 2026·24 minsFpl Notes Lean Formal Verification CRDT MRDT RGA Collaborative Editing Distributed SystemsNotes on a tombstone-free RGA: proved RA-linearizable in Lean 4, then found to reorder your text on delete. Why convergence is not correctness.