Cheng Tan

Consistency Checking Is the New Verifier

Notes from the first Symposium on Consistency Checking Principles

· systemsresearchverification ·中文

On September 4th, in a ballroom in Boston, ten papers and one keynote made up the first Symposium on Consistency Checking Principles (SCCP), co-located with VLDB. A first workshop is a big thing sociologically: it is the moment a scattered set of researchers—who until now published in traditionally different communities, databases, operating systems, distributed systems, formal methods—decide they have been working on the same subject all along. I want to write down what I think that subject is, and why I believe it is about to matter a great deal more than it does today.

A mental model of a concurrent world

Start with the mental model, because everything else is a special case of it. Several entities read and write some shared state. Nobody watches the state directly; what an observer gets is a history, a record of operations and the values they returned. The question is whether that history could have been produced by a system obeying the rules it claims to obey.

Several entities read and write shared state. An observer sees only a history of operations, and must decide whether some legal ordering explains it.

Name the entities and the state differently and you get different systems. Transactions over database rows. Processes over files. Clients over objects in a store. Replicas over a CRDT. Threads over memory. And now agents over a shared workspace. The rules change name too—serializability, snapshot isolation, linearizability, causal consistency—but the question underneath stays the same: does there exist a legal execution that explains what we saw? Readers of an earlier post will recognize that shape; it is the existential definition of correctness, and consistency checking is its oldest and most concrete instance.

Defining consistency is (mostly) finished; checking it is only beginning

For thirty years the hard, prestigious work in this area was definition, and then delivering on it: saying precisely what snapshot isolation means, and designing a protocol that implements it more efficiently than the last one. That work is largely done. The definitions exist and are formal, the protocols exist, and many of them now press against limits we can prove.

What is not done is checking them. Given a real history from a real system, decide whether it satisfies the level. That question splits into two hard halves. The theoretical half: what is the complexity, and can it be dodged? The engineering half: how do you make the check fast enough to run against a production database rather than a toy? The field has learned that these are not the same problem, and that solving one does not solve the other. Only together do they produce a checker that people can use daily.

Mistakes are inevitable, and they are silent

Two forces are pushing consistency checking from a niche concern to a central one.

The first is compounding complexity. Consistency levels got weaker and stranger because weaker sells performance; implementations grew sophisticated because fault tolerance and optimization demand it. A modern distributed database is a weak guarantee implemented by an intricate protocol, which is precisely the configuration in which mistakes are inevitable and tricky to detect.

The second is automation, and it worries me more. As AI writes more of the code, fewer people will carry a working understanding of what concurrency does—the reasoning that says why this interleaving is fine and that one is a disaster. And consistency bugs are exactly the class that such reasoning used to catch, because a consistency violation does not crash anything. There is no stack trace. The system stays up, serves traffic, and quietly holds a state that no correct execution could have produced. Losing the people who can spot that, while multiplying the code that causes it, is not a combination that ends well without machines that check.

If consistency violations sound like an academic worry, the keynote was the answer to it. Alexey Gotsman, of IMDEA and part-time at AWS, spoke about testing the consistency of distributed databases inside Amazon—including replaying the runs of a production system like Aurora Limitless against a non-distributed reference. The largest operators of databases in the world are checking them, in production, right now.

From a few hundred transactions to (near) production speed

The arc is short enough: before 2020, black-box isolation checkers were evaluated on histories of a few hundred transactions. That is a research prototype’s scale, not a database’s. Then consistency checking crossed into practicality: Cobra (OSDI’20), work I was part of, verified serializability for black-box databases at a couple of thousand transactions per second—close to the rate at which a real system produces them.

What happened next is why I think this is a real field. A dozen groups are advancing the frontier of consistency checking, and I asked Claude to compile a matrix of the results. Reading it back, the striking thing is how ordinary progress has become. The weak levels now have sound and complete checkers. The NP-hard ones are handled at real scale by solvers, by grey-box designs that ask the database for its own timestamps, and by workload restrictions that buy linear time. Throughput has climbed from a few hundred transactions per history to tens of thousands per second. And the assumptions that kept these tools away from real workloads—no predicates, no duplicate values, no range queries—are being addressed one paper at a time, and speedups of a few orders of magnitude over the previous generation are now happening. That is what a field looks like when it starts building.

Two directions: deepen, and broaden

I see two directions for this community, and they need different people.

Deepen. Any system with shared state is in scope, and the nearest edge is databases with real SQL: predicates make even the cheap levels expensive, and the black-box checker that handles a genuine query workload does not quite exist yet. Behind that queue up file systems, whose interface and consistency model are both awkward; object stores, which have no transactions and weak guarantees; CRDTs; and the unglamorous middle of the cloud—queues, message passing, metadata services—which nobody checks and everybody trusts.

Broaden. Agent workloads are going to be concurrent and collaborative, and they arrive with a nasty twist: there is no specification to check against. Multiple agents will read and write shared context, tools, and memory, and “correct” for that setting is not yet defined. The community has already noticed—two of the ten papers were about LLM agents, including the best paper, “Notified Serializability,” which proposes a consistency model for concurrent agents. The instinct here will be to reach for serializability and its relatives, and that instinct is a good start and certainly not the end.

Consistency checking is the new verifier

I believe consistency checking is a far broader thing than it looks today, and here is the argument. In machine learning, the technique that works right now is reinforcement learning with verifiable rewards (RLVR)—train against a deterministic checker instead of a learned reward model, which is why math and code improved first. They had verifiers. Systems correctness mostly does not, and concurrency correctness is the most challenging case: a property no test suite reliably catches, on code that machines increasingly write. A consistency checker is a verifier for concurrency correctness, and the moment one is fast enough to sit in a loop, it stops being a debugging tool and becomes a correctness signal.

Looking forward, if systems become automated and tailored—AI-native in the sense that the system regenerates its own implementation, each one built for its own workload, with its own protocol and its own weakened guarantee—then generic checkers will not fit them, and checking will have to be tailored too. Checkers generated per system, by the same machines that write the systems, and themselves in need of checking. The field that just held its first workshop may find that its real job is not building the checker, but building the thing that builds them.

References