adya brings Jepsen-style isolation checking to CI in a single Rust binary

A developer has released adya, an open-source Rust tool that checks whether a database actually delivers the transaction isolation it claims, without requiring the JVM that Jepsen's Elle checker is built on. In a post on dev.to, the author describes it as an attempt to make black-box isolation verification cheap and portable enough to run in ordinary continuous integration.

What adya does

adya consumes a history — a log of what each client requested and what the database returned — and reports which isolation guarantees held. For each violation, it prints the transactions involved and the chain of reads and writes that proves the anomaly. According to the post, it is an independent implementation of the approach from Elle (Kingsbury and Alvaro, VLDB 2020), reading the same history formats and accepting the same flags.

The underlying problem is that isolation bugs do not surface in unit tests. They require a specific interleaving of concurrent transactions, and when they occur nothing crashes: a balance is simply wrong, or two bookings land on the same seat. Write skew is the standard example — two transactions each check a condition, see that it holds, and commit changes that jointly break it. Snapshot isolation permits this, and Postgres's REPEATABLE READ is snapshot isolation, so applications assuming stronger semantics can ship the bug unnoticed.

Elle's contribution was showing that such anomalies can be detected from the outside: record client operations, infer dependencies between transactions, and look for the cycles each isolation level forbids. The anomaly classes (G0, G1c, G-single, G2) come from Atul Adya's 1999 thesis, which also supplies the tool's name.

Why not just use Elle

Elle is a Clojure library, and teams wanting it outside a Jepsen run typically shell out to elle-cli from a Go or Python harness. The author cites two open-source projects doing exactly that in CI, including bytecaskdb, whose pull request documents the friction: a blocked Clojars mirror, a crash when graphviz was missing, and log lines corrupting JSON output. He also reports that elle-cli 0.1.11 hung with no output on anomalous histories on Windows, and that on Linux it needed more than five minutes on five of forty random 300-transaction histories and exhausted a 6 GB heap on one more. adya, he says, checked all forty in 0.2 seconds.

Elle also leaves the workload to you: the client that generates transactions, runs them against the database and records the history is your responsibility. adya bundles both halves in one binary — after cargo install adya, a single command can execute a workload at one isolation level against a live Postgres connection or a built-in simulator, then check the resulting history against a stricter model.

How the checking works

The default workload is list-append, borrowed from Elle: keys hold lists, transactions append unique values and read whole lists back, so each read reveals the order of every append before it without trusting the database. adya builds a dependency graph from those orderings using Adya's ww, wr and rw edge types, adding real-time edges for strict serializability, with a transitive reduction keeping the graph roughly linear in the history's size.

Each anomaly class is a cycle with constraints — G-single has exactly one rw edge, for instance. Instead of enumerating cycles, adya runs a breadth-first search over transaction and path-state pairs, where the state is seven bits tracking rw counts and edge adjacency, returning the shortest cycle of the requested shape. Cheaper strongly-connected-component checks run first so that anomaly classes which cannot occur are skipped entirely. The author reports a 100,000-transaction history (30 MB of JSON) checks in about 1.6 seconds on his laptop.

Validation and database results

Because a wrong checker is worse than none, validation took most of the effort, the post says. adya matches all 56 histories in elle-cli's test suite — same verdicts, anomaly types and weakest models ruled out — and its CI cross-checks randomly generated histories against live Elle; in the first full run Elle completed 34 of 40 histories and adya agreed on all 34. A simulator implementing serializable, snapshot isolation, read committed, read uncommitted and a deliberately broken level asserts that correct runs produce zero anomalies at their own tier and the expected ones above it.

The project's CI also drives 4,000 transactions from 10 clients over 6 hot keys against Postgres 17 and MySQL 8.4. Postgres SERIALIZABLE validates against every model; Postgres REPEATABLE READ shows G2-item when checked against serializability, matching snapshot isolation's known limits; Postgres READ COMMITTED shows G-single, G2-item, internal and lost-update anomalies. Notably, MySQL's REPEATABLE READ failed even the snapshot-isolation check in the published table, surfacing anomalies that Postgres's same-named level does not exhibit.

Why it matters

Most teams treat isolation levels as documentation promises. adya turns that promise into an automated, repeatable test: one Rust binary generates the workload, records the history and checks it in seconds, removing the JVM fragility that made Elle awkward in CI pipelines. The Postgres-versus-MySQL results already show the payoff — identical level names can hide materially different guarantees. Black-box history checking remains empirical rather than a proof of correctness, but routinely looking for these bugs is a significant step up from never checking at all.