Collaborative text editing with RGA30 July 2026·24 minsNotes Lean Formal Verification CRDT 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.
