Anatoliy Bilenko and Alberto Carretero: Making Database Protocols Reliable with Formal Methods and AI

Anatoliy Bilenko opens with the methods Canonical uses to design protocols and build confidence in their correctness: state machines, formal specifications and verification, TLA+, Antithesis, Jepsen, global state reconstruction, model-based testing, and property-based testing. These are parts of a development process, rather than a single verification step performed after the implementation is finished.

Bilenko is a staff engineer at Canonical and leads the Dqlite distributed database team. He also leads a performance and correctness academy that trains engineers and managers in performance analysis and formal verification. Before Canonical, he spent a decade at Seagate working on distributed storage, performance, and transaction management. His co-presenter, Alberto Carretero, is a software engineer and Dqlite contributor whose work focuses on correctness, formal methods, design verification, and distributed algorithms, with a background in mathematics and computer science.

Writing a protocol is an unusual assignment for many engineers. People are not necessarily taught how to do it at university or in their everyday work. The happy path is usually the easy part: send messages between network processes using the available libraries. The difficulty emerges when the environment stops behaving as expected. Failures introduce more states, and those states must remain manageable in code, traces, and every other representation of the protocol.

Consider transferring a file from one process to another. A message might be dropped or duplicated, or a process might crash. Handling any one of those cases is already more work than the happy path; handling their possible interleavings is harder still. Suppose the receiver makes a persistent change in response to a message, but the acknowledgement disappears. The sender and receiver no longer have the same knowledge of what happened. The design must answer what state the system is now in.

The possible failures extend across networks, disks, processes, and time. Bilenko also raises Byzantine failures, such as memory corruption or deliberately unexpected behavior. The point is not that every protocol must solve every imaginable problem in the same way. It is that the designer must reason about the relevant failure model instead of letting those cases remain implicit.

There is a social dimension as well. Protocol implementations can live for decades, while the engineers who understood their assumptions leave or retire. If the design drifts away from the code, assumptions that were once explicit become knowledge that only a few people remember. Keeping the design connected to the implementation is therefore a maintenance problem as much as a mathematical one.

Distributed teams also need a shared way of discussing the system. At a company such as Canonical, engineers may work remotely and think in different abstractions: one prefers interfaces, another state machines, another sequence diagrams, while someone else works through successive experiments. Bilenko argues for a common language that lets those people approach protocol and distributed-systems problems together. His starting point is the state machine.

For a protocol that sends a large file in chunks, the first instinct may be to define messages and draw a sequence diagram. That diagram can illustrate an exchange, but it does not usually reveal all the interleavings that can lead to failure. When investigating a catastrophe, engineers need the sequence of states and transitions that produced it, not just a picture of one intended conversation.

Bilenko replaces that view with a state machine for the sender. The example comes from an introductory protocol exercise in the performance and correctness academy and contains six states, with actions such as send, receive, and timeout. This representation makes the atomic changes in the sender’s state explicit. It also makes clear that the sender is only one part of the distributed system: there is still a receiver and a network to model.

As state machines grow, decomposition becomes essential. A component can be treated as a box with input actions or events, output events, and its internal state. Combining such components gives a hierarchical view of the whole system. For the file-transfer example, that means separating the sender, receiver, and network behavior while preserving the actions that connect them. The abstraction provides a way to control complexity without abandoning the state-machine language.

Record each component’s actions along its own timeline and combine them, and the result becomes a history of the system’s events. Record causal relationships between transitions on different processes as well, and that history becomes useful for explaining what happened. Bilenko does not cover the mechanics of capturing those relationships in this talk, but emphasizes their role in connecting otherwise separate timelines.

A realistic execution history contains many timelines, state transitions, labels, and causal links. The details can quickly become too dense to inspect visually. To reason about that history, engineers define properties: perhaps one action must never overlap another, or a protocol must eventually progress to completion. The history supplies the concrete execution against which those expectations can be examined.

Two familiar classes of properties are safety and liveness. Safety expresses that something bad never happens: for example, there is at most one outstanding request, or a reply corresponds to an earlier request in the state machine. Liveness expresses that something good eventually happens. A delivery guarantee might require a message sent between the appropriate processes eventually to arrive. These properties give precise meaning to claims that would otherwise remain informal.

For a sufficiently complicated system, a graph of states and transitions becomes awkward to write and maintain. A specification language provides another representation. Bilenko uses TLA+, introduced by Leslie Lamport, to express states, events, and the system’s evolution. In the example on screen, sending and delivering messages are explicit, and an output event can be modeled through a state change. The benefit is a more manageable specification with its assumptions stated clearly.

The same language also expresses the properties that the model is intended to satisfy. In the link example, one liveness property says that every message sent between correct processes will eventually be delivered, under an assumption of fair delivery by the lower network layer. Temporal operators let the specification distinguish what must always hold from what must eventually occur. For Bilenko’s team, this is also a shared language for discussing design and implementation details.

Once the team has a TLA+ specification and its properties, it uses TLC, the model checker in the TLA+ toolset. TLC explores transitions in the model, including behaviors involving message delivery, timeouts, and crashes. It checks whether the explored model satisfies the stated properties. The state space can be pictured as a large graph: each node is a system state and each edge is an action that leads to another state.

TLC can also generate traces. A trace is a particular path through that graph—a sequence of events that occurred in the modeled distributed system. Those traces are useful beyond inspecting the specification itself. They can become inputs to model-based tests, allowing the implementation to be exercised against behaviors derived from the design rather than only against examples an engineer wrote by hand.

In a real program, some properties can be checked locally. Each transition of the sender’s state machine has preconditions. In the example, a file must be closed before the relevant transfer loop starts; once chunks are being sent, the file must be open and a timeout must be set. Similar conditions apply in other sender states. These checks concern information that a single process can observe directly.

Global properties are more difficult because a single process cannot observe all the relevant events in a distributed execution. A consensus protocol such as Raft has properties that can readily be stated and checked inside a model or simulator, where the system state is available. The harder question is how to evaluate those same expectations against a real, running protocol whose information is spread across processes.

The team’s answer starts with histories. If the system records states and causal relationships, a reconstruction algorithm can produce an ordering of events suitable for analysis. Bilenko mentions Chandy–Lamport and other approaches while acknowledging that they have limitations. One possible step is a topological ordering of the recorded causal relationships, after which a property can be evaluated across the resulting sequence of states.

This is how the team approaches distributed postmortems in its database. Rather than knowing only that the database failed, it tries to establish the sequence of steps that led to the failure. Bilenko presents history reconstruction as a practical connection between the abstract properties of the design and the concrete execution that produced a problem.

There is another connection between models and code: replaying model-generated traces in a test environment. After writing the protocol’s state machines, the team can export traces from the model and feed them to the implementation’s test harness. When the implementation behaves consistently with the model, those tests succeed. The purpose is to keep the code and design synchronized as both evolve.

Bilenko summarizes one development path as an executable design. Start with a TLA+ specification, use TLC to check the model, generate traces, and feed those traces into model-based tests. The tests then provide evidence about whether the implemented protocol corresponds to the model. This workflow makes the design something the team can execute and test against, rather than a document that gradually loses contact with the code.

A second path starts with an actual cluster—for example, three nodes—and collects logs from its execution. The team reconstructs a trace and sends that trace to a property checker, bringing global properties into the testing process. This does not remove the limitations of distributed snapshot or reconstruction algorithms. Bilenko notes that their implementation targets a particular protocol, which allows protocol-specific heuristics to help where a general solution would be more difficult.

Existing or legacy systems need a similar workflow even when they did not start from an executable specification. Tools such as Jepsen and Antithesis can exercise distributed scenarios and expose corner cases. Canonical uses both for testing, and also uses Antithesis to explore states and help reconstruct a global execution trace. The exploration is useful as evidence about how the running protocol actually behaves.

In that workflow, the team runs the protocol under an exploration framework, reconstructs global state, identifies properties, and assembles a browsable history. An agent can receive that history alongside the protocol’s codebase. The investigation then informs improvements to instrumentation, so distributed properties can be expressed and checked more accurately. The loop repeats until the team has a clearer account of the system’s behavior.

Carretero takes over to examine the limits of this toolbox. The process can sound as though applying the right collection of tools will automatically produce a working protocol. In practice, each method introduces difficult questions of its own. TLC is useful for model checking and model-based testing, but the team still needs to decide when the exploration has provided enough reassurance to stop.

Line coverage gives a misleading answer to that question. Imagine two processes that read a shared counter, update local copies, and write back to the shared counter. Running process A and then process B can execute every line while never exercising the interleavings that lose an update. For a protocol, the meaningful complexity lies in the ordering and interaction of operations, not merely in whether each statement ran.

The state-space graph provides a better way to think about coverage, but raw counts still do not settle the matter. TLC might report that it checked 50 million states. Those states could cover an important part of the algorithm—or could consist largely of repeated elections or cycles of sending and dropping messages. A high number says little unless the engineers understand which behaviors the search actually reached.

The simplest response is to constrain the model to a smaller region. An engineer might decide that two elections are enough to expose the relevant corner cases, or that three replicated entries allow the important permutations to be tested. These bounds reduce the search, but they leave the same question inside the constrained region: has the tool exercised the interesting behavior, or spent its effort on uninformative details such as the network implementation?

Another response is to define interesting predicates. Instead of asking only for line coverage or a state count, ask whether the model reached an election with two candidate nodes, or a conflict in replicated data. That at least confirms that specific cases occurred. The weakness is the manual bias: engineers must already know which cases to name. If they knew every important corner case in advance, ordinary tests would be much closer to sufficient.

The team can also choose interesting starting states. Rather than waiting for the checker to reach a two-candidate election, start there and explore nearby states. Several starting points can open up several neighborhoods of behavior. This directs effort toward cases the team considers promising, but still does not prove that the explored neighborhoods contain all the important failures—or that the tool is spending its time meaningfully within them.

A further step is to guide the exploration itself, expressing which behaviors look more interesting. Carretero mentions Apalache’s JSON-RPC interface and exploration strategies for TLC as ways to influence the search. At that point the process starts to resemble fuzzing. The team considered building its own simulator and fuzzer, then recognized that existing systems could provide much of the machinery it needed.

Carretero distinguishes Antithesis from Jepsen because the two are sometimes treated as interchangeable. In his account, Antithesis provides guided exploration in a deterministic environment. It can snapshot execution, return to an earlier point, and support debugging a failure by moving through the execution again. That combination lets the team direct the search toward interesting behavior and obtain useful coverage.

Jepsen offers a different strength: flexible randomized failure injection. It is well known for testing distributed-system correctness, but random configurations do not tell the team whether a run is exploring a meaningful scenario. Faults might simply prevent elections and leave the protocol making no progress. The contrast is about how the tools search for behavior, and why using one does not eliminate every limitation of the other.

Instead of exploring an enormous state space, another approach is to prove a property. A formal argument could establish that a particular aspect of a TLA+ model is safe. Historically, constructing such proofs might take an expert days or weeks. Carretero says LLMs can now help write proofs for some theorems and use a checker to test whether the proposed proof is accepted. The attraction is the checked result, rather than the prose of the proof itself.

Even a perfect proof does not close the whole correctness problem. It proves something about the specification, not automatically that the code implements the specification. The team still needs a connection back to the implementation, such as generated traces and tests. That can bring it straight back to state-space exploration and tools such as Antithesis or Jepsen. Formal proof changes the kind of evidence available; it does not erase the model-to-code gap.

LLMs also have uneven abilities within proof work. Carretero finds them effective on familiar proofs but less reliable when the task calls for a new or simpler argument. A model may repeatedly attempt the full problem and fail. It can search history or online material, and it may introduce assumptions that make the final result look valid while removing the substance of what was supposed to be proved. Knowing enough TLA+ to inspect and guide that work remains necessary.

Specification size is another obstacle. In the team’s experience with TLAPS, adding actions and moving the model closer to the implementation makes proof complexity grow rapidly. A small specification can sometimes be proved with AI assistance almost autonomously; a larger one is much harder. Yet a specification intended to resemble real code tends to need more detail. Precision and tractability pull against one another.

The team reduces that burden by starting with a model that already has an established proof, using Raft as an example. Carretero is explicit that the baseline is not perfect, but it can serve as a practical ground truth. Instead of rebuilding the entire model and proof, the engineers add their modifications on top and try to establish that those changes preserve the guarantees of the original.

Reasoning about that delta is much easier for an LLM than inventing an argument for the entire system. The task becomes narrower and more mechanical: identify what changed and show that the change maintains the baseline’s guarantees. This does not make the broader correctness problem disappear, but it gives AI-assisted proof work a more tractable scope.

Carretero closes with the opposite end of the workflow: checking global invariants in a running or legacy system. The team might want to establish that there is only one leader or that data is not lost. Failures complicate the observation itself. It is easy enough to reason about an action when the process successfully records it, but the action and the log entry are not necessarily atomic.

Suppose a process commits data and then crashes before logging the commit. A reconstructor cannot simply infer the missing state from the events it saw. The system may need to emit information again, and the engineers must account for what is unknown. General distributed reconstruction algorithms have limitations here. A test environment tailored to the protocol can simplify the problem, and the team finds that useful even though it does not yield a universal solution.

The final summary returns to complementary tools. Models, state machines, and properties document the design and help distinguish valid behavior from invalid behavior. Properties and proofs support formal reasoning, while traces and reconstructed histories help inspect the running system. Testing remains central: model-based testing, deterministic simulation, property-based testing, randomized testing such as Jepsen, and fuzzing such as Antithesis all contribute different kinds of evidence.

There is no silver bullet, Carretero concludes. A team cannot start at the beginning, apply every technique in a checklist, and assume the resulting protocol will work. The practical task is to mix and match these methods, understand the limitations of each, and use their combined evidence to build confidence that the protocol is correct.