Uwueave · a machine-checked map of the merge
Two
phones.
When two people change the same thing at the same time on different devices, something has to happen when their changes meet. Usually what happens is decided by accident · whatever the code did · and discovered by users, as a number that was quietly wrong or an edit that silently vanished. This is a careful map of that moment.
The list survives.
A shared shopping list. You add eggs; your partner adds bread. Offline. When the phones sync, you have both · no conflict, no server, no waiting. And it isn't luck:
phone A, offline: + eggs [519add] phone B, offline: + bread [38932b] ...the phones sync... phone A now holds: bread, eggs phone B now holds: bread, eggs A.merge(B) == B.merge(A): true (commutative) merging the same delta twice: true (idempotent · gossip may repeat)
"The list only grows" is the kind of promise that survives meeting. It works every time, for any number of phones, with no coordinator anywhere. The merge provably cannot break it.
The money can't.
A shared $100 balance. The app promises its user one rule: balance ≥ 0. You spend $80; your partner spends $80. Each phone, alone, was being perfectly responsible.
start: $100 phone A, offline: -$80 → $20 legal on A (20 >= 0) phone B, offline: -$80 → $20 legal on B (20 >= 0) ...the phones sync... merged: $-60 ← the rule is broken merged the other way: $-60 ← and it converges perfectly both directions agree: true (it is a correct CRDT)
Look closely at what failed. The merge is not a strawman: it is a genuine semilattice join, commutative and idempotent, and it loses nothing. It still overdraws the account · because the promise was never one a merge could keep. No cleverer merge fixes this. That is a theorem, not a bug report.
The universe says no. Then it hands you a menu.
The useful part is that the "no" is not the end of the conversation. It is the start of a priced menu, and every line of the menu is a theorem:
And · the part we're proudest of · some exits provably don't apply to your particular problem. The menu you get is short and honest, not a list of vague possibilities.
The crossings have receipts.
Underneath the demos is a library of judgements: can this promise survive merging? is the counterexample operationally reachable, or a ghost state? what does a repair cost on this workload? The library currently carries 135 crossings between judgements, and each row names the hypothesis evidence needs to travel from one to the other · plus the counterexample without it. A row with no counterexample is a row that isn't finished.
No hidden fork after reachable divergence.
That law is growing a language. In preoscript, a stability claim cannot be written without naming which future it is stable against; a forked result cannot be collapsed to a single answer by accident; and a coordination budget can be rejected by a lower bound but only accepted by a witnessed plan with a proved cost. The compiler is not allowed to be optimistic on your behalf.
Try it yourself.
Those two phones are a program, and the trickiest decisions ship as compiled proofs rather than code someone wrote twice:
git clone https://github.com/emberian/lean-uwueave && cd lean-uwueave/rust cargo run --example two_phones
Two more examples follow the same shape: collaborate builds a real document with two people in it and shows a move that un-happens after a sync · named, in a per-op trace, rather than silently. gated revokes authority mid-flight and shows the ops still sitting in storage while the view drops them.