Elle: a black-box transactional consistency checker that reasons backwards

Elle checks a history, not a database

Elle is a transactional consistency checker for black-box databases, written in Clojure, and it works from recorded client observations rather than from any cooperation from the server under test. Given a history of transactions plus minimal constraints on the datatypes and operations involved, it decides whether that observation exhibits transactional anomalies.

The inference runs backwards from an impossibility. Elle looks for a sequence of events in the history that could not possibly have occurred in that order, and it uses that to argue the history cannot be internally consistent. That framing explains both its strengths and its limits. It needs a history that someone already recorded, so it is a post-hoc checker rather than a live monitor, and it can only report what a client could have seen.

Two audiences are described for it. Teams that want to check a database can use Jepsen, where Elle is built in. Teams with their own histories can add Elle as a dependency to any JVM project and invoke the checker functions directly. The README also points non-JVM users at a wrapper path: write the history to a file or a stream, then call a small wrapper program to produce output.

Dependency edges come from reads, writes, and observed values

The demo model is deliberately small. Each object is a list of numbers. A read is written as [:r :x [1 2 3]] and returns the current value of that list, while a write is written as [:append :y 4] and appends a number to the end of the list. Within those constraints, Elle has to work out the ordering of operations from the outside.

The README walks through a three transaction history. The first appends 1 to :x and observes :y equal to [1]. The second appends 2 to :x and 1 to :y. The third observes :x and sees [1 2]. Elle infers a write-read relationship between the first two transactions from their reads and writes, and it infers the write-write ordering between them because the third transaction observed :x as [1 2], which constrains the possible order of the appends. Those two edges close a loop.

That loop is a G1c anomaly, cyclic information flow. On the complexity question, the README states that Elle is roughly linear in history length and roughly constant, rather than exponential, with respect to concurrency. That is the project's own claim about its own cost, and the practical consequence is that the check stays affordable on long Jepsen runs where the interesting anomalies appear in small clusters of transactions rather than across the whole history.

Adding Elle to a JVM project, and what the demo needs

There is no install command in the README. If you want Elle to check a database, the project tells you to go through Jepsen, where Elle comes built in. If you want to check your own histories, you add Elle as a dependency to any JVM project and call the checker functions directly. The repository has a project.clj at its top level, alongside src/ for the implementation and test/ for the accompanying test suite, and the README links a Clojars badge and cljdoc documentation for the published artifact.

The demo additionally needs a copy of Graphviz installed before you start, because the checker renders dependency plots.

Loading the checker and the history helpers looks like this:

=> (require '[elle.list-append :as a]
            '[jepsen.history :as h])
nil

You then build a history from three committed transactions:

=> (def h (h/history
            [{:process 0, :type :ok, :value [[:append :x 1] [:r :y [1]]]}
             {:process 1, :type :ok, :value [[:append :x 2] [:append :y 1]]}
             {:process 2, :type :ok, :value [[:r :x [1 2]]]}]))
h

The check itself takes a map of options and the history:

=> (pprint (a/check {:consistency-models [:serializable], :directory "out"} h))

The options map names the consistency models to test against and the directory that receives the anomaly output, which in the demo is called out/. The result map reports :valid? as false and :anomaly-types as (:G1c), and it lists the models the history fails in :not and :also-not, which in the demo covers read-committed together with stronger levels including consistent-view, snapshot-isolation, serializable, and update-serializable.

What out/G1c.txt and the two kinds of plot tell you

The :directory option is not a scratch file. It is where the checker writes one text file per anomaly class and a corresponding plot. For the demo history, the text file reads:

$ cat out/G1c.txt
G1c #0
Let:
  T1 = {:index 1, :time -1, :type :ok, :process 1, :f nil,
        :value [[:append :x 2] [:append :y 1]]}
  T2 = {:index 0, :time -1, :type :ok, :process 0, :f nil,
        :value [[:append :x 1] [:r :y [1]]]}


Then:
  - T1 < T2, because T2 observed T1's append of 1 to key :y.
  - However, T2 < T1, because T1 appended 2 after T2 appended 1 to :x: a contradiction!

The two orderings contradict each other, which is the whole argument in eight lines. The README notes that Elle can point to a minimal set of transactions witnessing a consistency violation, and the text file is that set written out in plain language.

Plots come in two flavours. Elle renders a graph for each individual cycle, where the point is to show as small a set of transactions as possible. It also renders a plot for each strongly-connected component of the dependency graph, which is a different question: cycles show you one contradiction, while strongly-connected components show you the scope of the anomalous behaviour around it. A history with realtime edges, write-write, write-read, and read-write dependencies can produce a far larger component than any single cycle, and that gap is where the debugging effort usually goes.

Completeness comes with a predicate caveat

The README claims Elle can find every non-predicate anomaly from Adya, Liskov, and O'Neil's Generalized Isolation Level Definitions. That is a specific completeness claim about a specific model family, not a general promise that every consistency bug will be found.

The parenthetical matters and the README does not expand on it. Anomalies in that framework that are stated in terms of predicates, that is, conditions over sets of values rather than single keys, sit outside what Elle claims to detect. The project also points at src/elle/consistency_model.clj as the place where consistency models are rigorously defined, and it invites contributions there specifically, which suggests that the boundary between what a model covers and what the checker can prove is still being worked on. If your workload depends on multi-key predicate constraints, or on applications that enforce invariants across several keys at once, you need to read that file yourself rather than trust the summary line.

The second limitation is about what Elle sees. Every input is a client observation, so an anomaly is invisible if no client ever read the value that would have revealed it. Elle can only reason about the operations it was given, and the demo's operations are deliberately narrow: reads of a whole list and appends to it.

The README asks you to re-check its own verdicts

The most useful sentence for an adopter is also the most cautionary. The README states that Elle is still under active development and that the maintainers are not 100% confident in its inference rules yet, and it says that Jepsen recommends checking reported anomalies by hand to make sure they are valid.

That is not a rounding error in the confidence interval. It means the intended workflow is: let Elle scan a long history, then hand-verify the handful of cycles it hands you. Elle's value is in the scan, in finding small witnesses buried in thousands of transactions, not in being the last word. Anyone wiring the :valid? flag into a CI gate without a manual review step is reading the project backwards.

This also sets the bar for the wrong-tool cases. If you have no recorded history, there is nothing for Elle to read. If you need a guarantee that holds for every possible interleaving rather than for one observed run, a post-hoc checker is the wrong shape of tool. If you need predicate-level anomalies, the claim above does not cover them. What Elle does fit well is triage: a fast pass over an existing history to answer whether an anomaly is present, where it is, and which few transactions are responsible.

Maintenance signals, the EPL-2.0 licence, and upgrade cost

The last push to the repository was on 2026-10-16, and the project is not archived, so the codebase is being changed. The README still describes Elle as under active development, and it explicitly welcomes help with the formal proof in the proof/ directory, which is written in Isabelle/HOL and described in the README as a nowhere-near-complete sketch. The paper referenced from the README carries the intuition behind the goals and a rough formalization of the soundness proof.

The repository has no GitHub releases. Version tracking therefore lives outside the release page, in CHANGELOG.md at the top level and on Clojars, which is where the README badge points. For a dependency that encodes consistency models, that is a real upgrade cost to plan for: the set of models the checker supports can change between commits, so pinning matters and reading the changelog before a bump is worth the minute.

The licence is EPL-2.0. It is a copyleft licence with file-level obligations, so if you modify Elle's own files you must keep those files available under the same terms, and combining it with proprietary code in the same files is restricted. That is a summary of the licence text, not legal advice; if you intend to embed Elle in a commercial product, have counsel look at the specific arrangement.

Editorial conclusion

Elle is a good fit for teams that already record histories, whether through Jepsen or their own harness, and want a fast triage pass over anomalies rather than a proof of correctness. It is a poor fit for anyone who needs predicate-level guarantees or a formally verified checker, because the README says the inference rules are not yet fully trusted and the proof in the repository is described as nowhere-near-complete. Before adopting it, check the version published on Clojars against the commit you plan to run, read src/elle/consistency_model.clj to see which models the checker actually encodes, and reproduce the three-transaction demo history to confirm the output matches what you expect.

Frequently asked questions

Official sources

1. Issues
2. jepsen-io/elle on GitHub
3. License: EPL-2.0
4. README