Garbage-collecting Byzantine, open-membership CRDTs without a quorum — by recomputing the stability certificate that authorizes it, not agreeing on one.
Gustavo Schneiter · humanguardrail.github.io
A short technical report. Everything below is backed by a runnable artifact; every claim links to the exact program that establishes it. The long version — full threat model, definitions, and runnable evidence — is the extended technical report.
CRDTs converge without coordination, but they can't forget: to stay safe they hoard reconciliation metadata forever. The standard fix — causal stability — lets a replica discard that metadata once every peer has seen an update. It assumes you can establish that fact. Under open membership (devices join and leave) and Byzantine peers (some lie), you normally can't — so the field's escape hatch for safe GC is a BFT quorum, which reintroduces the coordination CRDTs existed to avoid.
Anchored Stability certifies causal stability by recomputation instead of agreement: every replica independently re-derives and checks the stability certificate from evidence it can verify itself. Byzantine writers get detected and fenced, not out-voted. No quorum on the stability path.
The interesting part isn't the claim — it's what happened when I tried to break it.
| Bugs found by attacking the safety argument | 3 (two before writing it up, one in an independent adversarial audit) |
| Reference simulator | 21 adversary scenarios, all pass |
| Bounded model-checker | 17 configs · 1126 states · 0 safety violations · 11 fault-injection "teeth" (ten fix-reverts + one vacuity probe), all biting |
| Independent TLA+/TLC model | convergence exhausted over 2,299,968 states (every delivery order; no symmetry reduction, so this is coverage, not proof depth); the fence, when removed, produces the divergence in 7 steps |
| What I claim | checked, not proven — and I'll show you exactly where that line is |
None of that table is prose to take on faith. Every row regenerates from dependency-free
Python (plus a stock tla2tools.jar run) in this repo — python3 anchored_stability_sim.py,
python3 anchored_stability_checker.py, and the three bug reproductions.
Clone it and watch it check itself; the rest of this page just explains what you're looking at.
A CRDT keeps tombstones, version vectors, and causal context so that any update which might still arrive can be reconciled. Left alone that metadata grows forever — a document you edited for a year carries the sediment of every keystroke. Causal stability is the natural garbage-collection trigger: once an update is stable (everyone has it), its reconciliation metadata is safe to drop. But "everyone has it" is a membership fact, and under open, Byzantine membership a malicious peer can forge that fact, get honest peers to drop the metadata that protected a write, and then introduce a conflict that can no longer be reconciled. The write is silently lost, or the replicas diverge. The published way out is consensus. This is the way out without it.
The certificate is a recomputation, not an agreement. There is no privileged signer whose word is trusted — only evidence every replica checks the same way:
- Leases bind each writer's lineage to a genesis anchor for a bounded term (this is how open membership is handled: grant, renew, supersede, depart).
- Content-bound signed acks: when a writer flushes a position it signs a root that is bound to the content at that position. A fork has different content, so a different root — it can't borrow another write's acknowledgement.
- Stability by recomputation: any replica re-derives the stable frontier from the signed evidence and checks it locally. A Byzantine writer that equivocates incriminates itself in the evidence, and every replica that sees the evidence fences it — the same way, in any order.
Byzantine tolerance here is by detection, not prevention: a fork can be transiently read before the contradicting evidence arrives, but once any replica has the evidence, the fork is never stable again, and honest replicas converge. That eventual-detection boundary is the honest scope of the whole thing, and I keep it in the open.
A safety argument that has never been mechanically attacked is a draft of an argument. So I built two replicas in a model, made them exchange every message in every order, and let a program — not my conviction — decide whether they still agreed. It caught three real bugs.
Bug 1 — ack-equivocation, opposite order. A Byzantine writer signs two conflicting
versions of one position and sends them to two replicas in opposite order. My code recorded
"first seen wins," so each replica called a different fork stable — a convergence break
under identical evidence. Fix: a position with two conflicting signed roots has no
canonical root; fence every fork there. Both replicas eventually see both acks, both fence,
both converge.
repro_ack_equiv_divergence.py.
Bug 2 — content-free ack forgery. My stability rule trusted that a position was
"covered" if an ack existed — without checking the ack was bound to the content. A
Byzantine issuer could mint a contentless "yes, this is stable" and stabilize a fork. Fix:
an op enters the stable set only if the signed root is content-bound and its own content
matches. repro_content_free_forgery.py.
Bug 3 — a garbage-collector that erased evidence it still needed. This one I did not
find — a cold reviewer's mechanized attack (an independent adversarial audit of the
finished draft, not external human peer review) found it, and it broke the headline claim.
The oldest machinery (the shed, which reclaims a stabilized position's
data) conflicts with the newest fix (keeping an omitted acked write recoverable). A
replica sheds the winning write, believing the position settled; a concurrent
lower-priority write then recovers; the replica that shed resolves to the loser while an
unshed replica keeps the winner. Same evidence, two reads. Fix: a shed retains a tiny
per-key resolution marker so a recovered lower write can never flip a shed winner. It is
now a permanent test. repro_shed_r126_divergence.py
prints converged with the fix and DIVERGENCE without it.
The pattern is the point: each bug lived where the newest fix met the oldest machinery, and each was found by a program asking an order I hadn't. The third one is the strongest evidence the method works — it broke my headline claim on a runnable counterexample, and the fix became another biting tooth.
Zero violations proves nothing if the check is vacuous. So the model-checker carries teeth: for each load-bearing fix, a meta-test reverts it in the model and asserts the checker then fires the exact invariant that fix protects. Revert the equivocation fence → Bug 1 reappears. Revert the canonicity gate → Bug 2's fork stabilizes. Revert the shed marker → Bug 3 diverges. Eleven teeth, all biting; if a future refactor silently defeats a guarantee, a tooth stops biting and the build goes red. (This is mutation testing + vacuity detection, wired into a shippable artifact.)
An independent second witness: an independent TLA+ model of the convergence property, checked with the standard TLC model-checker — no code of mine in the loop. Fence on: exhaustive green over 2.3M states. Fence off (one flag): TLC produces the opposite-order divergence in a seven-step counterexample. It mechanizes both the property and its falsifiability.
A GC paper owes a number. The measurement harness drives the same simulator the checker verifies — no toy model. A grow-only CRDT's retained state is linear in the work done; Anchored Stability sheds below the certified frontier and holds the bulky state flat (a tiny hash-per-position marker residual remains — see §7/§8, not literally zero). The one honest cost: a live, persistent equivocator can deny GC — but only for its own retained evidence, bounded to the detection window (measured 80 → 0 once convicted), not unbounded. I report the ugly cases too (a starvation schedule that retains an acked-pending write at +1 op/round); none of them is hidden.
- Checked, not proven. The model-checker is exhaustive over its configurations; the TLA+ model is exhaustive over its states — both finite. A machine-checked unbounded proof (TLAPS, for all N) is future work, and I don't claim it.
- LWW scope. The composed guarantee (safe GC plus recoverable durability) is established here for last-writer-wins registers. A sequence/text CRDT may need reconciliation metadata a shed already discarded — the very workload that motivates the problem. Named, not hidden.
- Stable ≠ settled. What's certified is stability-of-the-set, not finality-of-the-value: an omitted acked write can later recover and flip a read you already acted on — and this is reachable in honest runs, not only under attack. If your application needs settled reads, this scheme gives you safe GC and recoverable durability, not settledness. It is the paper's sharpest limitation (§8), so it belongs here too.
- "Without a quorum" ≠ without trust. The membership roster is relocated to a genesis-rooted anchor. A quorum tolerates f faulty authorities; a single anchor tolerates none. This trades write-path agreement for trust in the anchor — priced, not eliminated; threshold-distributing the anchor is the obvious hardening.
- The honest limit of the method itself: the version you can run does not break in every order I know how to ask it — which is a smaller claim than in every order. Bug 3 is the proof that the difference is real, and shipping the harness is how the next person asks an order I didn't.
Everything is dependency-free Python plus a standard TLA+ model; every number above regenerates from these:
anchored_stability_sim.py— reference simulator (21 scenarios)anchored_stability_checker.py— bounded model-checker (17 configs, 11 teeth; ~7–8 min — it re-runs every config under each tooth)metadata_growth.py— the GC measurementAnchoredStability.tla+AS_small_bug.cfg— the TLA+ model and its falsifiability counterexampletla_nonvacuity_census.py— regenerates the model's non-vacuity counts- the three bug reproductions: 1 · 2 · 3
The TLA+ model needs a stock tla2tools.jar (not vendored — it is the standard
TLA+ toolbox distribution):
java -cp tla2tools.jar tlc2.TLC -config AnchoredStability.cfg AnchoredStability.tla # exhaustive: 2,299,968 states, ~4 min
java -cp tla2tools.jar tlc2.TLC -config AS_small_bug.cfg AnchoredStability.tla # the 7-step divergence, ~1 sThe extended technical report has the full threat catalogue, the formal definitions, the prior-art placement, and every limitation argued in full.
Code (*.py, *.tla, *.cfg) is MIT-licensed — see LICENSE. The written
report (README.md and PAPER.md) is licensed
CC BY 4.0: reuse and quote freely, with
attribution to Gustavo Schneiter.
Gustavo Schneiter. Anchored Stability: Garbage-collecting Byzantine, open-membership CRDTs without a quorum. 2026. Zenodo. https://doi.org/10.5281/zenodo.21209725
The DOI above is the concept DOI — it always resolves to the latest version.