Collaborative text editing with RGA

A warning up front: this is going to be a long and technical post. It is also the one I most wanted to write.

This summer I had the opportunity to work with Prof. KC Sivaramakrishnan at FP Launchpad, IIT Madras. The project lived in Sal: the Lean 4 port of the F* framework Neem (Soundarapandian, Nagar, Rastogi, Sivaramakrishnan, OOPSLA 2025), for verifying state-based CRDTs and Mergeable Replicated Data Types (MRDTs).

My work was with RGA, the sequence CRDT behind Automerge and Yjs.It has to keep every character you ever deleted, forever. An MRDT’s merge gets to see the common ancestor of the two states it is merging. Could that extra information pay for the graveyard?

I spent the summer answering that. The short version is that we got a design, proved it correct in Lean with zero sorrys, and then proved that it is wrong. Not wrong in the proof; wrong in what the proof was about. A single backspace reorders text the user never touched, and the theorem could not see it, because it was checking the implementation against itself.

That turned out to be the most useful thing I learned all summer, so it gets its own section rather than a footnote. The rest of the post is the road there and the fix on the other side.

The arc is:

1. Why collaborative editing is hard, and why indices are the wrong vocabulary.
2. RGA, and what its tombstones are actually paying for.
3. MRDTs: a merge that gets to see the common ancestor, and the question that opens.
4. A tombstone-free RGA that rehomes survivors, and its proof.
5. The defect, as a theorem. Why the proof could not see it. Why it is not patchable.
6. EmbedRGA: make position an immutable birth constant, and everything gets easier.

1. The problem

#

I don’t need to mention why collaborative text editing is useful in today’s world, especially as students or researchers. Google Docs and Overleaf is almost indispensable if you’re working with a team. Those late night edits before an assignment deadline, watching the cursor lobby around the document and seeing the changes made by your teammates in real time is a great experience. But what happens when you are working on a document and your internet connection drops? Or when two people are editing the same paragraph at the same time? How do we ensure that everyone sees the same document, and that no edits are lost? It would be incredibly frustrating to lose your work because of a network issue.

So the product requirement is: always writable, never lost, everyone eventually sees the same document, and it should be the document people meant.

Each client is a full replica. The edit is applied to the local copy first, with no round trip on the critical path. So documents will diverge, but we have a decent way to reconcile. They just need to eventually converge. Strong Eventual Consistency

sequenceDiagram
    participant A as Replica A (plane, offline)
    participant B as Replica B (office)
    participant C as Replica C (phone)

    Note over A,C: all three replicas hold AB

    A->>A: ins X — applied locally, 0 ms
    B->>B: ins Y — applied locally, 0 ms
    C->>C: del B — applied locally, 0 ms

    B->>C: ins Y
    C->>B: del B
    Note over B,C: B and C reconcile with each other
while A is still in the air

    A->>B: ins X (hours late)
    A->>C: ins X
    B->>A: ins Y, del B (one batch, on reconnect)

    Note over A,C: the same three edits, a different arrival order at every replica
SEC: all three must still read the same document

Four facts make this genuinely hard, and they are all consequences of choosing availability:

• No global order. No clock and no leader that both replicas trust. “Which edit came first?” often has no answer at all.
• Arbitrary delays. Tuesday’s edit can arrive after Friday’s.
• Local-first. You cannot wait for consensus. Availability during a partition is the whole point.
• Concurrency is genuine. Any rule that resolves two mutually unaware edits must give the same answer at every replica, in any arrival order.

Sequential reasoning (“apply the operations in order”) is precisely what we are not allowed to assume.

2. Indices are not identities

#

The obvious protocol is to ship what the editor already knows: a position and a character.

insert(index = 2, char = 'X')
delete(index = 0)

This is the vocabulary of String.insert and splice, the API every editor has. It is also broken, because an index is a coordinate in a document that is changing underneath it. It means something only relative to one replica’s state at one instant.

Break #1: two documents, forever

#

flowchart TD
    S["AB — both replicas start here"]
    S -->|"A: ins(1,'X')"| L["AXB"]
    S -->|"B: ins(1,'Y')"| R["AYB"]
    L -->|"then applies ins(1,'Y')"| L2["AYXB"]
    R -->|"then applies ins(1,'X')"| R2["AXYB"]

Same two operations, same causal history, two different documents, and the replicas will never agree again.

Break #2: the index stops referring to anything

#

This one is worse, and it is a different failure: there are not two answers, there is no answer at all.

flowchart TD
    S["CAT — insert positions 0…3"]
    S -->|"A: del(0), del(0)"| L["T — insert positions 0…1"]
    S -->|"B: ins(3,'S') — meaning at the end"| R["CATS"]
    L -->|"now ins(3,'S') arrives at A"| X["position 3 does not exist"]
    X -->|"reject it"| X1["T — the author's S is silently lost"]
    X -->|"clamp to the end"| X2["TS — a position nobody asked for"]

ins(3,'S') was perfectly legal when it was issued. By the time it lands, T has two positions. The operation is not wrong so much as meaningless.

The fix in principle: name characters, don’t count them

#

Give every inserted character a globally unique, immutable identifier: a (timestamp, replica id) pair, minted locally with no coordination. An insertion names its anchor: the character it goes after. The operation is now context-free: it can be applied at any replica, in any order, and still mean the same thing.

The document is no longer a string. It is a tree of identities, read out by a deterministic traversal. That is what a sequence CRDT is.

3. CRDTs and RGA

#

A state-based CRDT is a state space with a merge

that is commutative, associative and idempotent, i.e. a join-semilattice. It is easy to see that this merge buys Strong Eventual Consistency: any two replicas that have received the same set of updates are in the same state, regardless of order, duplication or delay.

RGA (Replicated Growable Array; Roh, Jeon, Kim, Lee, JPDC 71(3), 2011) is the sequence CRDT underlying Automerge and Yjs. Its state is a grow-only set of records

plus a grow-only set of tombstones: ids that have been deleted. Insert adds a record anchored at an existing id; Remove adds an id to the tombstone set; merge is componentwise union. Both components are grow-only, so merge is trivially a semilattice join.

All the interesting content is in the read. The read is a depth-first traversal from the root, where among siblings sharing an anchor, the newest id goes first:

flowchart TD
    root(("⊥")) --> n1["1 · 'A'"]
    n1 --> n6["6 · 'Y'"]
    n1 --> n5["5 · 'X'"]
    n1 --> n2["2 · 'B'"]

(Arrows read “is the anchor of”; the stored pointer runs the other way.) Ids 6 > 5 > 2 are all anchored at 'A', so the document reads A Y X B at every replica. Notice that this is exactly what settles Break #1’s race, deterministically and without a tie-breaking authority.

In Sal, that order is an inductive relation visible_lt with four rules (RGA_ReadSide.lean):

and three kernel-checked intent theorems on top of it, on both the CRDT and the MRDT: causal_order_visible_lt, tombstone_monotone_under_remove, concurrent_insert_tiebreak_deterministic.

Real documents are rich text

#

Real documents are not plain text, it is rich text with Bold, Italics, links, comments. So formatting by index range breaks for exactly the reason that inserting by index breaks: concurrent inserts shift every index, so “bold characters 5 to 14” denotes a different span at each replica.

Peritext (Litt, Lim, Kleppmann, van Hardenberg, CSCW 2022) fixes the span the same way RGA fixes the insert: a mark is not a range of positions, it is a pair of anchors, each naming a character and a side.

{ "action":   "addMark",
  "markType": "bold",
  "start":    { "type": "before", "opId": "5@A" },
  "end":      { "type": "after",  "opId": "14@B" } }

Peritext is then just RGA + a grow-only set of marks. Alice’s bold is the mark above, on fox jumped; say Bob concurrently italicises The fox. The two overlap and simply merge; the render is a left-to-right fold over reading order, opening and closing marks:

[ {text: "The ",    format: {italic}},
  {text: "fox",     format: {bold, italic}},
  {text: " jumped", format: {bold}} ]

The merge is where the anchoring earns its keep. Alice bolds the whole sentence, and concurrently Bob types a word into the middle of it:

The merge itself has nothing to arbitrate: chars and marks are both grow-only, so it is componentwise union, exactly as in §3. The delicate case is not this one but text typed at a boundary rather than strictly inside it, which is what the side bits decide, and why bold grows to swallow it while a link does not.

4. MRDTs: git, but for data types

#

Everything above is a CRDT: merge sees two states. An MRDT’s merge additionally sees their lowest common ancestor:

That third argument is worth a lot. With ℓ in hand, the merge can distinguish “x was never there” from “x was there and was deleted”, which is exactly the information a CRDT has to encode in tombstones. So the LCA can pay for the tombstones instead.

The canonical demonstration is OR-Set, which drops its remove-set entirely:

flowchart TD
    L["ℓ = {(1,a)}"]
    L -->|"A: Add a @ ts 2"| A["A = {(1,a), (2,a)}"]
    L -->|"B: Rem a"| B["B = { }"]
    A --> M["merge = {(2,a)} — a is live, add wins"]
    B --> M

Term by term: ℓ∩a∩b = {} (B removed it), a∖ℓ = {(2,a)} (the new tag), b∖ℓ = {}. Every add stakes a fresh, globally unique id that each replica mints for itself, so (2,a) is a different tag from (1,a). (1,a) was in ℓ, so B’s remove observed it. (2,a) was not, so B cannot have seen it, and it survives.

5. What “correct” means: Neem, Sal, RA-linearizability

#

To reason about correctness, we need a framework to prove things about our Replicated Data Types. Neem (OOPSLA'25) reduces the correctness of a data type to a fixed, discharge-able set of obligations. You supply a signature

where rc resolves non-commuting operation pairs (Fst_then_snd / Snd_then_fst / Either). Neem’s metatheorem: discharge 24 verification conditions (some algebraic properties) over do, merge and rc (rc_non_comm, no_rc_chain, merge_comm, merge_idem, base_1op, base_2op, ind_lca_2op, inter_left_1op, lem_0op, …) and replication-aware linearizability (the notion of correctness we will be working with) follows for every execution.

Sal is the Lean 4 port, plus a multi-modal tactic that stages automation by trustworthiness (dsimp+grind → lean-blaster/Z3 → interactive), and a counterexample pipeline that turns an invalid VC into an inspectable execution trace (Plausible + ProofWidgets). The suite currently holds 29 RDTs (17 CRDTs, 12 MRDTs) and 648 VCs for state convergence, the vast majority kernel-checked.

RA-linearizability, in words

#

Every state a replica can ever hold must be explainable as the result of running its operations one at a time, in some order, an order that respects causality and obeys the data type’s own tie-breaking rule.

flowchart LR
    D["the replica's event set E
a partial order under vis"]
    D -->|"∃ π: a permutation of E
respecting vis and rc"| P["π = o₁ · o₃ · o₂"]
    P -->|"applySeq from σ₀, using do_"| S["s — the replica's actual state"]

So a merged state is never “some third thing”: it is always a sequential history someone could have executed. In Lean (Sal/ConditionedMRDTs/Metatheory/Adequacy.lean):

def IsRALinearizable3 (C : Configuration D) : Prop :=
  ∀ (v : Version) (s : D.State) (E : Set (Op D.AppOp)),
    C.ver v = some (s, E) →
    ∃ π : List (Op D.AppOp),
      listPermOf π E ∧                              -- π enumerates exactly E
      respects π (lo (Configuration.core C)) ∧      -- causality + rc
      applySeq D.toCRDTSig D.init π = s             -- replaying π gives s

It is quantified over every version in the configuration: replica heads and historical versions used as LCAs. lo is visibility together with the rc arbitration; its acyclicity is exactly what no_rc_chain gives you.

Convergence is not enough

#

merge ℓ a b := ∅ is commutative, associative, idempotent, and satisfies SEC. It is also useless. So is “ignore all operations”. Convergence is a necessary condition that any number of wrong data types satisfy.

For sequences the problem is sharper, and it is worth being blunt about where in the suite the VCs carry real content:

Roughly half the suite, and all the interesting data types, are Tier C. For RGA, the 24 VCs prove that two grow-only sets converge under union. They never mention the traversal that turns those sets into a document.

Hence the house rule: every RDT in Sal carries a *_ReadSide.lean companion, and the Tier-C ones carry intent-preservation theorems matched to their papers. The honest claim is intent preservation against a published specification, not “proven correct”.

6. Tombstones, and why you cannot just delete the record

#

A tombstone is a deleted character we cannot throw away, because other characters are positioned relative to it.

Garbage collection would need to know that every replica has seen the delete, which needs consensus, which is exactly what we gave up in §1. So the goal is: make Remove physically remove the record, so state is bounded by live characters. And the MRDT’s LCA is the extra information that might pay for it.

Why not simply delete the record, then? Because a survivor anchored at the deleted node is left pointing at an id that is not in the state: its position becomes undefined, and it has nowhere to render.

7. The rehoming RGA

#

Sal/MRDTs/RGA_Rehoming/. State is map ℕ (α × ℕ): id ↦ (element, anchor). Deletion really removes the record. Two halves, deliberately parallel:

In merge: climb the LCA. Survivorship is the OR-Set formula, yielding a survivor set I. A survivor whose recorded anchor is dead walks up the ancestor chain the LCA already knows, until it reaches a node that also survives, or the root.

let ancL := fun y => anc l y   -- the ancestor function, read out of the LCA

def climb_aux (ancL) (I) : ℕ → ℕ → ℕ
  | 0,      x => x
  | fuel+1, x => if x = 0 || I x then x
                 else climb_aux ancL I fuel (ancL x)

In do there is no LCA. A single replica applying an operation has no third state to consult. So the operation carries its target’s ancestor chain in its payload, and resolve takes the first entry still live. Both halves together give rc = Either at every reachable state (rc_non_comm').

It was proved, and the schema had to be widened

#

Commutation here holds only on reachable states: the operation’s claimed path must really be its ancestor chain (accurate), timestamps must be fresh, the root is never stored. That is a conditioned commutativity, and the plain 24 VCs quantify over all states. (A prefix-free variant of the design is outright impossible; see RGA_PrefixFree_Impossible.lean.)

So we built the conditioned metatheory and proved the theorem directly:

8. …and it is still wrong

#

Four operations on one replica, with no concurrency and no merge anywhere. Just a backspace.

This is a theorem rather than an anecdote, and it is stated against a specification written independently of the implementation: a delete removes its target and nothing else moves.

-- The independent intent spec.
def DeleteOrderPreserving : Prop :=
  ∀ (s : concrete_st) (t r x : ℕ) (p ids : List ℕ),
    List.Pairwise (· > ·) ids → (∀ i, contains s i = true → i ∈ ids) →
    document (do_ s (t, r, .Del p x)) (ids.filter (· ≠ x))
      = (document s ids).filter (· ≠ x)

theorem tombstone_free_violates_delete_order : ¬ DeleteOrderPreserving := by
  -- witness: s_bac with the complete, strictly-descending candidate list [3,2,1]
  ...  exact absurd key (by native_decide)

The candidate list is guarded descending and complete, so the discrepancy cannot be an artifact of how we chose to read. There is a companion, del_a_breaks_survivor_order, and, importantly, the positive contrast is a theorem too: remove_preserves_visible_lt holds for the tombstoned RGA.

Why the proof did not see it

#

flowchart LR
    DO["do_ — the step function"]
    DO -->|"merge ℓ a b"| M["what the replica computed"]
    DO -->|"fold of a witness sequence π"| F["the certified reference"]
    M -.->|"the VC checks only this ="| F

Both sides are computed with the same do_. If do_ is wrong, both sides are wrong the same way, and the VC passes.

Own-fold RA-linearizability certifies convergence and self-consistency. It does not certify fidelity to the intended sequence semantics. This is the verification analogue of “your tests pass but the code is wrong”: a proof checks itself against the spec you wrote, and nothing checks the spec.

Catching it requires a specification independent of the implementation’s own fold; here, the published RGA’s traversal order. We had hit the same failure mode once before, in Peritext: in_span_boundary encoded the opposite of the paper’s §3.3, and roughly 400 lines of perfectly correct proofs about it had to be deleted.

Is it patchable? No, and that is informative

#

A fooling-pair argument settles it. Consider two executions whose live characters and live geometry agree, but whose deleted history differs. RGA’s traversal distinguishes them. A tombstone-free state cannot.

There is also a structural reason the obvious repair, “let merge notice the orphan and rewrite its anchor”, cannot be made to work inside the framework, and the framework says so. The VC

lem_0op : eq (merge (do_ l ol) (do_ a ol) (do_ b ol))
             (do_ (merge l a b) ol)

fails for ol = Remove X under any rehab scheme whose orphan test consults the merged domain, because do and merge disagree about who is an orphan. Delete first, and X is absent from the merged domain, so Y is an orphan and gets rewritten. Merge first, and all three inputs still have X, so Y is not an orphan, and the outer delete then strands it. The lattice-join merges the 24 VCs were designed around touch ℓ only through set algebra; rehabilitation is a structural query on ℓ, and that is precisely what an outer do can invalidate.

So the culprit is not the merge. It is the representation:

Delete reorders survivors because survivors’ positions are stored relatively, and a relative position must be recomputed when its reference dies. Rewriting a position is reordering.

Fix the representation, not the merge. Make position a birth constant.

9. EmbedRGA: immutable birth coordinates

#

Sal/MRDTs/RGA_Embed/. State is map ℕ (α × List Bool): id ↦ (element, coordinate). On insert, mint the newcomer’s coordinate from its anchor’s, once and forever:

where a is the anchor id, t the new timestamp, t − a the delta, and Γ any order-preserving, prefix-free code.

A pleasant side effect: do on Ins never reads the state, so every operation pair commutes unconditionally enough that rc = Either discharges with no path algebra at all.

Sorting coordinates is the RGA traversal

#

Compare two coordinates as delta sequences (chainBefore):

1. If one is a prefix of the other, the prefix comes first. → this is RGA’s parent_child rule.
2. Otherwise, at the first differing delta, the larger delta comes first. → this is RGA’s sibling rule (a larger delta under a shared anchor means a newer timestamp).

Reading the figure above: ⟨2⟩ ≺ ⟨1⟩ ≺ ⟨1,2⟩, so the document is [2,1,3]; after the delete, [2,3]. Order preserved.

Mechanically it is one lexicographic compare. Concatenate the codewords, append a terminator symbol above the digit alphabet, and sort descending:

def key (c : coord) : List ℕ :=
  (c.map fun b => if b then 2 else 1) ++ [3]

The terminator is the trick that makes rule 1 fall out of rule 2: where one key ends, it shows a 3, which beats any digit the longer key can offer, so a prefix always sorts ahead of its extensions. The supporting theorems:

The two capstones

#

1. Convergence. embed_ra_linearizable3: RA-linearizability per version at every honestly reachable configuration, with strict =, not ≈.

Route: the mergeable-queue hook, whose join needs canonical states unique per event set. Supplied by e_fold_canon: any two well-formed enumerations of one event set fold to the same state.

2. Fidelity. rga_read_eq_embed_read, the compaction theorem. On honest executions, EmbedRGA’s read equals the published, tombstoned RGA’s read, element for element.

The second one is the point of the whole exercise: the specification is now external. It is RGA’s own visible_lt, not our fold. A by-product the published side never proved falls out along the way. visible_lt_total says RGA’s relational order is total on the birth tree.

Two further notes on the engineering:

• The development is parametric in the code. Unary, binary-δ and Elias-δ instances are all proved, with zero new proof content each: every datatype theorem consumes only OrderedPrefixCode (monotone + prefix-free). Coordinates cost roughly 1.4 to 1.8 bits per level on real traces.
• Axioms used: propext, Classical.choice, Quot.sound. No sorryAx.

Tombstone-free, and provably the same document as RGA.

10. Rich text inherits the fix, and inherited the defect

#

The fused design puts the mark boundaries into the sequence, so rich text is one RGA:

inductive PeritextElt
  | char  : ℕ → PeritextElt
  | bound : ℕ → Mark → Bool → PeritextElt
--          markId  mark   isStart

Because the payload is opaque to the kernel, convergence is a one-line instantiation with no new proof:

theorem peritextEmbed_ra_linearizable3
    (hReach : EReach Γ C) : IsRALinearizable3 C :=
  embed_ra_linearizable3 hReach

And the defect of §8 reappears here in the form a user would actually notice. Delete one plain character on the rehoming kernel, and an untouched character silently changes formatting:

On the embed kernel there is nothing to say, which is the point: renderIds_del states that the post-delete render is the pre-delete render minus exactly the deleted entries, so the formatting of every survivor is preserved bitwise.

Both shapes are in the repo: marks in a separate set (as published), and marks fused into the sequence. The fused one rides the embed kernel for free.

12. What we learned

#

1. Indices are not identities. Collaborative editing works because characters are named, and the document is a tree read by a deterministic traversal.

2. Convergence is a substrate, not correctness. “All replicas agree on the empty document” satisfies SEC. For grow-only sequence state, the 24 VCs prove that union commutes; the meaning lives entirely in the read.

3. The specification must be external. Own-fold RA-linearizability cannot see a broken do, because both sides of merge = fold use it. Fidelity needed a theorem against the published RGA.

4. Mechanization pays in refutations. It produced a machine-checked negative: a proved, converging, RA-linearizable tombstone-free RGA that reorders text under a single backspace, plus seven over-strong premises and a criss-cross countermodel we would never have found on paper.

5. Design for the proof. Making position an immutable birth constant turned Del into a filter, merge into a lattice join, and the read into a sort. Only then did both a strict-equality convergence proof and read-equivalence with the published RGA become available.

Pointers

#

References. Roh, Jeon, Kim, Lee, Replicated abstract data types, JPDC 71(3), 2011 · Shapiro, Preguiça, Baquero, Zawirski, A comprehensive study of CRDTs, INRIA RR-7506, 2011 · Litt, Lim, Kleppmann, van Hardenberg, Peritext, CSCW 2022 · Soundarapandian, Nagar, Rastogi, Sivaramakrishnan, OOPSLA 2025.

With thanks to Prof. KC Sivaramakrishnan for the supervision, and to Vimala Soundarapandian and Pranav Ramesh. FP Launchpad, IIT Madras.