crdtlib is a Lean 4 library with reusable combinators that can be used to construct conflict-free replicated data types without needing to prove convergence at every step. The combinators each preserve convergence, so whatever you assemble from them is a CRDT by construction: verified in Lean and executable.
Each tab below is a CRDT assembled from the combinators. Watch an operation travel down through the construction, transform at each combinator, and the interpreted state come back up to the application.
Two CRDTs side by side
A grow-only set of tags next to a counter. disjoint_product keeps both: an operation .inl goes to the set, and .inr to the counter.
disjoint_product (gset String) counter.inl "urgent"→({urgent}, 0).inr 2→({urgent}, 2).inl "ux"→({urgent, ux}, 2)Conflict resolution on read
A multi-value register keeps all concurrent writes.
On read, map_interpretation uses a user-defined total order to determine the latest among those values and returns it.
map_interpretation largest (mv_regₜ String)write "blue"→"blue"write "red" ∥→"red"write "green"→"green"A keyed family of CRDTs
The PN-Set: associate turns one counter into a counter per element. Adds count up, removes count down. The set keeps only the elements with a positive counter on interpretation.
map_interpretation positive (map_op ±1 (associate σ counter))add "milk"→{milk}add "eggs"→{milk, eggs}remove "milk"→{eggs}Observed-remove semantics
Adds carry a unique token, and a remove cancels only the tagged adds it has seen using their unique tokens. On interpretation, the set contains elements who's unique token was not removed.
map_interpretation (adds \ removes) (map_op route (disjoint_product union_set union_set))add milk #1→{milk}remove {(milk, 1)}→{}add milk #2→{milk}
An insert adds a node and, through traverse, two edges to a graph.
Removals are tracked in a tombstone set.
Reading the list traverses the graph in order.
map_interpretation po_traversal (disjoint_product (map_op _ (joint_product (gset σ) (po_edges σ))) (map_op _ (gset σ)))insert ⊥ H ⊤→"H"insert H i ⊤→"Hi"remove H→"i"
Games fork into a tree, keyed by path, and every node has a board and a threaded chat. traverse turns one chat message into two list operations: create a message node, then write the text.
traverse route (associate (List String) (disjoint_product (mv_lwwₜ Board) (polist_with_valuesₜ Cursor (mv_lwwₜ String))))place [] ⊞→{[] ↦ (⊞, [])}chat [] "gg"→{[] ↦ (⊞, [gg])}fork [b] ⊞′→{[] ↦ (⊞, [gg]), [b] ↦ (⊞′, [])}
Objects are keyed by id, and each one is a map or a list, chosen by a tagged union. One edit fans out to several objects, and the document is read off the objects from root. It runs 2.4 to 6 times faster than Automerge 0.7 to 0.9.
traverse route (associate Oid (tagged_unionₜ (mapₜ Oid Key) (listₜ Oid Cursor)))put_list root "todos" o₁→{root ↦ {todos: o₁}, o₁ ↦ []}insert o₁ ⊥ "milk"→{root ↦ {todos: o₁}, o₁ ↦ [milk]}insert o₁ p₁ "eggs"→{root ↦ {todos: o₁}, o₁ ↦ [milk, eggs]}The model
Replicas apply operations as they arrive, in whatever order the network delivers them. A CRDT defines what an operation does to the local state, and what the application reads from it.
effect applies an operation to the state σ.
interpret turns the state into the interpreted state γ for the application.
commutative guarantees that events can be applied in any order and produce the same state.
Replicas that have seen the same operations end in the same state, without coordination: strong eventual consistency.
structure CRDTₜ (τ : Type) [PartialOrder τ] (ω σ γ : Type*) where
effect : Event τ ω → σ → σ
interpret : σ → γ
commutative : ∀ (e₁ e₂ : Event τ ω),
Concurrent e₁.t e₂.t → (effect e₂) ∘ (effect e₁) = (effect e₁) ∘ (effect e₂)Convergent by construction
add x then add y; replica B the reverse. The two operations are concurrent, so commutative guarantees that applying them in both orders result in the same state.
Writing a CRDT by hand means proving commutative for the whole data type,
and every change to it means proving it again.
Instead, each combinator automatically constructs a proof of commutativity (and thus convergence) for each constructed CRDT. This holds for any level of nesting, since the CRDT type carries the commutativity proof.
Composition
product c₁ c₂Applies every operation to two CRDTs at once. The only combinator that combines two states.
ωσσ₁ × σ₂γγ₁ × γ₂map_state f f'Changes how the state is laid out, through a function with a left inverse.
ωσσ₂γγassociate κ cTurns one CRDT into a keyed family: a map from keys to independent copies.
κ × ωσAssociate κ σγAssociateInterp κ γtraverse f cTurns one operation into a list of inner operations: none, one, or several.
ω₂σσγγmap_interpretation f cChanges what the application observes. Operations and state stay the same.
ωσσγγ₂map_op f cTranslates each operation into exactly one inner operation. A traverse with singleton lists.
ω₂σσγγdisjoint_product c₁ c₂Two CRDTs side by side; each operation targets one of them.
ω₁ ⊕ ω₂σσ₁ × σ₂γγ₁ × γ₂joint_product c₁ c₂Two CRDTs side by side; each operation updates both, atomically.
ω₁ × ω₂σσ₁ × σ₂γγ₁ × γ₂tagged_unionₜ c₁ c₂Either one CRDT or the other, with a register deciding which one is active.
(ω₁ ⊕ ω₂) ⊕ Choiceσ(σ₁ × σ₂) × …γγ₁ ⊕ γ₂Next steps