Doniyor
Botirov.

Async bugs are not random. What is random is the interleaving the operating system happens to pick — which is why the failure shows up once in three hundred runs and never reproduces. unflake takes that choice away from the OS: time, timers and the order of ready callbacks all become values drawn from a seed. The same seed produces the same run, byte for byte. A found bug is shrunk to a minimal schedule and repeats on any machine.

Anyone can write leader election that works on a good day. The hard day is the one where the network splits, two nodes think they are in charge, a message from four seconds ago arrives twice, and a machine back from the dead brings a stale log. bulwark is Raft in TypeScript, held up by deterministic simulation: partitions, crashes and message reordering are drawn from a seed, the paper’s five safety properties are checked after every state transition, and every client history is verified linearizable. The centrepiece is the bug museum: each of its seven exhibits switches off exactly one rule of Raft and requires the harness to catch it — with a seed, and with a named property. One exhibit is a bug the harness found in the implementation itself.

Every database advertises isolation levels. Almost nobody can show you what theirs actually admits. “We provide snapshot isolation” is two claims at once: that nothing weaker ever happens, and that it is genuinely SI rather than something stricter wearing the name. Neither is checkable by reading code — they are properties of executions, not of text. adya catches executions and interrogates them: on one side an MVCC engine with four isolation levels, where serializable is Cahill’s algorithm, the one PostgreSQL implements; on the other a checker that builds a dependency graph from the observed history, hunts for cycles in it, and names what it finds by the names in Adya’s thesis — G0, G1a, G1b, G1c, G-single, G2-item. Every level is held to both directions: it never produces what it must prevent, and it does produce what the next level prevents. Neither side is trusted alone — each convicts the other.

This repository exists because of one sentence in unflake’s limits section: hundreds of seeds is a very good fuzz run, not a theorem. Sampling schedules finds bugs and can never prove their absence; proving absence means visiting every reachable state, which is exponential. So the interesting part of a model checker is not the search but everything done to avoid searching: symmetry (six interchangeable processes give 15,625 assignments but only 210 multisets) and partial-order reduction. The core problem is that a broken reduction answers exactly what a working one answers — “no violation found”. So the exhaustive search is kept alongside, slow and unable to be wrong, and every specification must produce a matching verdict in both. Liveness is checked under weak fairness: a spinlock is caught by a counterexample, Peterson’s algorithm passes.