A Cap Makes Brute Force Win
We aimed our own IC3/PDR model checker at the split-brain proof expecting it to beat explicit-state enumeration. It lost — because the lease guard caps one quantity, and that collapses the space brute force has to search.
quorum-types¶
Split-Brain, Unrepresentable
A type can make the bad state impossible to write down and still fail to make it impossible to reach.
Disjoint Becomes Intersecting
Generalizing a partition-based type system to a failure-tolerant one is not making the set bigger — it is flipping which set relation the type guards.
Where Structure Ends
A reconfigurable quorum system has two safety mechanisms that look redundant. They are not — they partition the problem by regime.
Up Is Gated, Down Is Free
A value's consensus strength forms a small lattice of levels, and the types that carry it are built from one asymmetry: earning a guarantee demands evidence, discarding one demands nothing.
A Merge Is a Proposal
Two committed values disagree and a certified function merges them. The design's central refusal — the result is not a decision — turns out to be a boundary between two literatures: CRDTs (conflict-free replicated data types), where replicas merge freely, and consensus, where they must agree first. Written as a compile error.
The Famous Number Assumes a Signature
Every rung of this series assumed nodes fail by stopping. Let them lie, and the evidence has to change type — not size. Along the way, the best-known constant in Byzantine fault tolerance turns out to be licensed by an assumption this toy doesn't get to make.
The Wire Is Where Const Generics Die
Every quorum certificate in this crate is indexed by a compile-time epoch; a socket hands you the epoch as eight bytes. What survives that crossing is worth stating exactly.
A Witness Changes Weight
The value lattice commits a value and throws its quorum witness away. Under nodes that lie, that same witness becomes the only thing holding the value up.