When do copies of your data still agree?
Systems that keep copies across regions, devices or services often accept a write and then repair it: cap the stock, clamp a balance, run a compensating step. Every copy can run that repair correctly and the copies can still disagree: oversold stock, a wrong balance, a deleted record that comes back. This work gives the exact conditions for when they agree, every one machine-checked, and gsm, a Go library, checks them at build time for systems that repair in the same transaction as the write.
Before either system was run, the theory predicted which delivery orders bring a deleted document back in CouchDB (a widely used open-source database) and PouchDB. All 216 observations matched, and a behavior found along the way was a CouchDB bug, now fixed upstream.
New to this? Sections 1 and 2 of the guide take about 3 minutes. Unfamiliar words are in the glossary.
Same events, different results
Replicas apply the same events in different orders, because networks delay, reorder and retry messages. After each event, every replica runs the same repair to restore its invariants. Do replicas that have seen the same events end in the same state?
Not always. A shelf holds 5 items and has 4 in stock. Two events arrive, "add 3" and "remove 1". Each replica records an update first, and then the repair caps the stock at 5.
Replica A applies "add 3" (7), repairs (5), then "remove 1": 4. Replica B applies "remove 1" (3), then "add 3" (6), repairs: 5.
Same events, same repair, different stock. In A the cap throws away 2 items before the removal; in B the removal comes first, so the cap throws away only 1.
Here the repair runs right after each event, and the two orders give 4 and 5: the repaired events do not commute. If the repair runs later, say in a background job, there is a second failure: from a raw 7, repairing first and then removing 1 gives 4, while removing 1 first gives 5.
So there are three questions to ask of a repair:
- (a) Does repairing early or late change what the next event produces?
- (b) Does the order of events change the repaired result?
- (c) Does the repair always finish?
The shelf fails (b), and (a) too if the repair runs late. The guide turns each question into a test you can run.
Who should care
Anyone whose system applies the same writes in more than one place and repairs them afterwards:
- active-active databases and multi-region writes;
- offline-first apps that sync when they reconnect;
- queues that retry and reorder messages;
- sagas with compensating steps;
- reconcilers and Kubernetes-style controllers.
The engineer's guide shows how to check your own system.
A prediction about real software
CouchDB and PouchDB replicate documents between databases. Using the theory, a model of each computed which delivery orders bring a deleted document back. The prediction was committed before either system was run. Then both systems were run: all 216 observations matched. A larger scenario that was not part of the scored prediction found an error in the CouchDB model, since corrected. That error led to a CouchDB behavior, reported upstream, confirmed as a bug by a CouchDB maintainer, and fixed. It matters because a validation function that accepts every document should not change what replicates, but in CouchDB it can decide whether a deleted document comes back.
The computed orders: 6 of 24 in CouchDB, none when CouchDB trims old revision history once at the end instead of after every update, and 12 of 24 in PouchDB. Each order ran three times. The real CouchDB replicator reaches the same behavior. Details: P3 · replicator · apache/couchdb#6162
When the repair runs matters
If the repair runs in the same transaction as the event, check question (b). If it runs in a background job or a reconciler, also check question (a). A system can be correct one way and break the other.
The guide's example: an account is charged past its limit, and a risk review follows. A background reconciler covers the overdraft from a credit line. If the reconciler runs before the review, the account stays in good standing; if the review comes first, it suspends the account, and the reconciler has nothing left to fix. Same events, same order, two different end states, decided by when the reconciler ran (guide, section 4).
In practice: if your repair runs in the same transaction as the event, test (b). If anything runs it later, test (a) as well, or move the repair into the transaction.
Proofs: atomic_exact · atomic_derived_from · atomic_not_descent
Checking a system with gsm
gsm is a Go library. You describe your system as a registry; a registry is one service's state, rules and events. In Go you list its variables, each with a finite range, its business rules with their repairs, and its events. The registry can live in a test next to your service; it does not have to be your production code. At build time gsm checks every state of that finite model, and either accepts it or names the order that diverges. It also checks a rules change before deployment, under the delivery the system actually has.
go get github.com/blackwell-systems/gsm
Here is the shelf:
r := gsm.NewRegistry("shelf")
stock := r.Int("stock", 4, 8)
r.Invariant("fits_on_shelf").
Watches(stock).
Holds(func(s gsm.State) bool { return s.GetInt(stock) <= 5 }).
Repair(func(s gsm.State) gsm.State { return s.SetInt(stock, 5) }).
Add()
r.Event("add_3").Writes(stock).
Apply(func(s gsm.State) gsm.State { return s.SetInt(stock, s.GetInt(stock)+3) }).Add()
r.Event("remove_1").Writes(stock).
Apply(func(s gsm.State) gsm.State { return s.SetInt(stock, s.GetInt(stock)-1) }).Add()
_, report, err := r.Build()err: gsm: Compensation Commutativity (CC) check failed
WFC: PASS (max repair depth: 1)
CC (Compensation Commutativity): FAIL
Events: (add_3, remove_1)
State: {stock=4}
add_3→remove_1: {stock=4}
remove_1→add_3: {stock=5}In the output, WFC (well-founded compensation) is question (c): the repair always finishes. CC (compensation commutativity) is question (b): repaired events give the same result in either order. The build refuses the shelf, and the failure it names is the story's: from 4 in stock, "add 3" then "remove 1" gives 4, and the other order gives 5.
gsm runs each event and its repair as one step, so it checks question (b) and question (c). If your repair runs in a background job, also run the guide's property test for question (a), or move the repair into the transaction.
The model's stock runs from 4, the story's starting stock, to 8, the most "add 3" can reach from a full shelf; gsm reports the first failing state it finds, counting up from the bottom. Output from gsm v0.16.0, abridged: lines were removed, none changed.
What adopting it costs. Go, and a model: you write your state, rules, repairs and events in a test, as above. gsm checks every state of that finite model. Large systems are checked in pieces (groups of variables that change together, one item of a collection, one link of a network of registries), so the cost depends on the largest piece, not the whole system.
No Go? The guide's property tests check the same three questions in an ordinary test suite. They sample states, so they can find a failure but cannot show that none exists. When a check fails, the guide's section 5, When a check fails: your options, lists the design moves.
A system that converges behaves like a CRDT on its repaired steps. What gsm adds is a way to build one: write the operations you want and the rules they must keep, and the build either proves every order converges or names the order that fails.
The Convergence Atlas
Every regime the theory covers, on one map. A regime is one kind of system: its shape (one service, a chain, a loop) and its delivery guarantee. The map covers free and causal delivery, CRDTs and streams, federations, networks with cycles, lossy channels, reconfiguration and composition. Each tile is an exact condition, a proof that no efficient one exists, or one of the 7 open problems (9 open tiles on the atlas), and opens to its theorem and counterexamples.
Where to go next
The rest of this page is for researchers. In short:
For researchers
Normalization confluence: an exact theory of when repair can replace commutativity. The research summary: the three conditions, how they relate, the framework, what is proved, how it was tested, and what is open.
Three conditions
Raw states may differ along the way; what has to agree is the result after repair. Write N for the repair. The theory proves a condition at each of three scales: necessary at one event when events can arrive mid-repair, exact for a single registry when combined with the condition on sequences, and exact for infinite runs on finite state spaces.
State descent
Question (a). Does repairing early or late change what the next event produces?
Applying an event to a state or to its repaired form gives the same result after repair: N(e(N x)) = N(e x). Convergence requires it.
History descent
Question (b). Does reordering events change the repaired result?
Every reordering the delivery model allows gives the same result after repair: free, causal, at-least-once, or declared independence.
Canonical recurrence
For systems whose repair may never stop. Does every fair run settle on one result?
On networks where repair may never stop, every fair run eventually stays on one repaired result.
How the conditions relate
- descent_not_history: state descent without history descent. Repair does nothing, and two events that do not commute separate a reordering.
- history_not_descent: history descent without state descent. One event, so every reordering is trivial, while the event does not respect what repair identifies.
- history_from_descent: given state descent, history descent of the raw runs is the same question about the repaired runs.
- nd_derived_from: with terminating repair, every run from a start has one result exactly when history descent and state descent both hold there.
Each exact condition is necessary and sufficient, with a counterexample for each hypothesis. CRDTs are the case where repair never runs. Repair enlarges which operations can be used: some converge only with repair, and no CRDT built from the same operations converges. The resulting behavior is itself a CRDT on the repaired steps; what repair adds is a way to build it from operations that do not commute.
Three layers
The same structure organizes the results across regimes. Three layers, and three proved interfaces between them:
Execution
Which executions count as the same. One theorem recovers the exact results for causal, at-least-once and declared-independence delivery, and for reconfiguration.
Consistent states
The fixed points of repair are exactly the solutions of a constraint problem, which places consistency in known constraint-satisfaction algebra.
Long-run behavior
Whether runs settle, and where. Oscillation, livelock and settling on the wrong state are classified in one vocabulary.
- A to B: an event must respect consistency only after repair, not strictly. Strict commutation is sufficient but not needed, and a real federation shows the difference. xu_iff_respects · strict_not_necessary
- B to C: a system can have exactly one consistent state and still never reach it. flip2_unique_solution_livelock · settled_canon_exact
- A to C: local conditions plus termination give convergence (Newman's lemma), and fair schedules alone do not, exactly when some action is starved forever. newman_bridge · four_point_fair_not_confluent · fair_sn_exact
- The compensation-commutativity theorem is the base case. The core single-registry theorem is derived from the framework's kernels, unchanged: the one-event condition is state descent and the commutation condition is history descent. The framework was built after that theorem, so this is a derivation, not a prediction. nd_derived_from · nd_cc_exact
What's proved
The headline numbers are above. Every theorem is checked on three Coq versions on every pull request. P1 was refuted by a counterexample before it was committed, so it never counted (how). Most of the open problems are on networks with cycles.
Checked against known results and real software
Recovering results the framework was built from shows organization, not reach. So the test is stricter: freeze every existing proof file, fix the pass criterion in advance, and recover a classical theorem from outside the repository. Each step the frozen framework could not express is reported as a leak.
Dijkstra's self-stabilization (1974)
A finite system stabilizes under fair schedules exactly when no fair loop leaves the legitimate states: one line from layer C. Dijkstra's K-state token ring follows for every ring size with K at least the number of machines, under fair and arbitrary schedules. Three leaks, all stated.
CRDT strong eventual consistency
Shapiro, Preguiça, Baquero and Zawirski (2011), and Gomes and others (2017). Op-based: passed, a short bridge from layer A with a repair that does nothing; replicas converge exactly when concurrent operations commute where they can be delivered. State-based: proved, but the merge of two replica states is not a kernel event, so that step leaked out of the frozen framework.
A preregistered prediction (P2)
Committed before any test: a matching market with exactly one stable matching can still cycle forever when every pair gets its turn. Confirmed at 3 by 3 and proved in Coq; about a quarter of 4 by 4 markets with one stable matching cycle.
A computed prediction about real software (P3)
Committed before either system was run: CouchDB and PouchDB bring a deleted document back on exactly the delivery orders a model built through the framework computed. All 216 observations matched. The counts and the upstream report are above.
Invariant confluence
Bailis and others (VLDB 2015): a set of transactions is invariant confluent exactly when the merge is a polymorphism of the reachable valid states, one short step from layer B. A polymorphism of the whole invariant is enough but not needed: two versions under set union with "not both present" is invariant confluent for "add a" while union breaks the invariant. Necessity of their Theorem 1 holds in a replica model; for an arbitrary system it needs a partition model the framework lacks, stated as a leak.
The CRDT test is the weakest: the repository proved CRDT convergence directly before the framework existed. The framework stays frozen, its files hash-checked in CI, while predictions written down before any test are checked (how).
Prior work and contributions
- Newman's lemma
- Trace theory for reorderings
- Constraint-satisfaction algebra: polymorphisms and sections
- Fair cycles and fair termination
- Exact conditions for governed convergence across the regimes, each hypothesis shown needed
- The regime map: exact, provably hard, or listed as open
- All of it mechanized, axiom-free
- The framework, tested on outside theorems with its proofs frozen
- Normalization confluence derived from the framework's kernels, without circularity
- Two preregistered predictions confirmed (P2, P3), committed before their tests
- New mathematics in the tools
- That the framework derives answers by theorem alone. Its predictions were a bet that came out right (P2) and a model computation checked against running software (P3).
- Exact long-run results beyond finite state spaces
Open problems
Each is listed in the regime audit with the progress made on it. The gaps are numbered as in the regime audit, which keeps closed gaps' numbers, so the list skips some. The atlas shows these 7 on 8 tiles, because gap 16 spans two; its ninth open tile, gap 13, is a narrower question about how local states glue into a global one, which the audit keeps apart from these 7.
- Gap 3Settling without a root on networks whose maps are not invertible.
- Gap 16Distributed propagation beyond its current hypotheses: events mixed with rootless propagation on cycles, monotone cycles with no finite height, repair as separate steps on cycles.
- Gap 17Rootless dynamics with lossy maps: whether every fair order reaches a quiescent state, and whether that state is unique.
- Gap 18Existence and counting of fixed points in the resolver reading without a spanning root.
- Gap 19Composition beyond collapsing to an acyclic network, in the cases not yet closed.
- Gap 20Reconfiguration inside a run: rules or topology changing while events are in flight, in the cases not yet closed.
- Gap 21Propagation over channels that delay, reorder or duplicate, in the cases not yet closed.
Researcher resources
Papers
- Normalization confluence: an exact, mechanized theory of when repair can replace commutativity (2026, version 5; doi:10.5281/zenodo.23311489; source). The main result, the three-layer framework, and its tests on outside theorems and preregistered predictions.
- Normalization Confluence in Federated Registry Networks (2026, version 2; doi:10.5281/zenodo.18677400)
- Normalization Confluence for Registry-Governed Stream Processing (2026, version 2; doi:10.5281/zenodo.18671870)
How to cite
@misc{blackwell2026federated,
author = {Blackwell, Dayna},
title = {Normalization Confluence in Federated Registry Networks},
publisher = {Zenodo},
year = {2026},
doi = {10.5281/zenodo.18677400}
}
@misc{blackwell2026stream,
author = {Blackwell, Dayna},
title = {Normalization Confluence for Registry-Governed Stream Processing},
publisher = {Zenodo},
year = {2026},
doi = {10.5281/zenodo.18671870}
}
@misc{blackwell2026theory,
author = {Blackwell, Dayna},
title = {Normalization confluence: an exact, mechanized theory of
when repair can replace commutativity},
publisher = {Zenodo},
year = {2026},
doi = {10.5281/zenodo.23311489}
}
@misc{blackwell2026categorical,
author = {Blackwell, Dayna},
title = {The Categorical Structure of Federated Convergence:
Limits, Sheaves, and Minimal Coordination},
publisher = {Zenodo},
year = {2026},
doi = {10.5281/zenodo.23311468}
}
@misc{blackwell2026nc,
author = {Blackwell, Dayna},
title = {Normalization Confluence: an exact regime map of governed concurrent state},
year = {2026},
howpublished = {\url{https://github.com/blackwell-systems/normalization-confluence}},
note = {Coq development}
}