TigerBeetle’s deterministic simulator is protocol-aware, which enables us to test safety and liveness invariants not just at the database level, but also at the level of each individual replica.

if (replica.status == .recovering_head) assert(fault);

In this post, we cover the mechanics, method, and merits of going beyond traditional, black-box methods of testing distributed systems – generative testing (for example, Jepsen), and deterministic hypervisors (for example, Antithesis) – to deeply test safety and liveness invariants using protocol-aware DST. If you prefer, watch a talk in which I cover this and more.

To begin, some background on safety and liveness invariants, consensus protocols, and deterministic simulation testing. For those who don’t require a refresher, feel free to jump to Protocol-Aware DST!

Distributed systems, i.e. systems with multiple interacting nodes, are notoriously hard to get right, as they require developers to reason about concurrent execution on multiple machines, and the state space of their interleavings is vast. Now, we can attack testing such a system from multiple angles, but today, let’s start with invariants. While testing your distributed system, it is crucial you identify two sets of invariants:

• Safety: which means nothing bad ever happens. For example, two nodes never return different results for the same request.
• Liveness: which means something good eventually happens. For example, a request will eventually be responded to provided enough nodes are online.

Your testing must then attempt to ascertain whether your system upholds these safety and liveness invariants.

Let us consider a specific distributed system: a consensus-based system. In this system, a consensus protocol is what turns durability into availability, safely. Put simply, a consensus protocol uses the redundancy in the system to provide fault tolerance, while maintaining the illusion of a single node. At a high level, a consensus protocol guarantees the following:

Fault Tolerance

This entails ensuring that faults like process crashes, network partitions, and storage corruptions are tolerated and masked. This is typically achieved via replication, i.e. maintaining multiple copies of the data for redundancy. Algorithms of the Viewstamped Replication flavor guarantee responsiveness as long as a majority of replicas are online. For example, in a system with 3 replicas (where the majority is 2 replicas), they can tolerate up to 1 fault.

This is the liveness invariant of a consensus protocol.

Agreement

This entails ensuring that the multiple copies of the data in the system are consistent with one another. One way to achieve this is by electing a primary replica. All requests flow through the primary, and the order in which the primary executes operations is the order all backups follow, ensuring data consistency.

This is the safety invariant of a consensus protocol.

TigerBeetle is a distributed database that uses VSR for fault tolerance and agreement. Routing all requests through the primary guarantees strict serializability, which is the strongest level of isolation a database can guarantee. Simply put, strict serializability posits that if one operation completes before another begins, the database must reflect that order.

Therefore, we can say that the safety invariant of our distributed database under test is strict serializability, and the liveness invariant is simply the liveness property of VSR, i.e. staying responsive as long as a majority of nodes are online.

Now, one way to test these invariants is using black-box generative testing, coupled with fault injection, Jepsen-style. Jepsen tests the system from the outside in, using user-visible APIs, embracing the inherent asynchrony and non-determinism in the system. This involves:

• Generating random inputs to probe the vast state space
• Subjecting the system to faults
• Asserting whether the safety and liveness invariants are upheld

Last year, we did do that, and here is an excerpt from our Jepsen report:

Integrating Viewstamped Replication with flexible quorums and protocol-aware recovery does not appear to have compromised the key invariant of Strong Serializability.

That’s wonderful news! As per our Jepsen evaluation, we were still upholding our guarantees to our users, which is crucial because the financial applications that are typically developed on top of TigerBeetle are developed assuming these strong guarantees. These applications rely on the strict serializability we promise them.

However, Jepsen-style generative testing and Antithesis-style deterministic hypervisors test the system from the outside in, via user-visible APIs. What about the invariants that aren’t visible at the API boundary? For foundational infrastructure, we must do better. We must test not only from the outside in… but also from the inside out.

TigerBeetle is explicitly designed as a deterministic distributed database. The idea of deterministic execution in databases isn’t new: FoundationDB and Dropbox’s Sync Engine are known to have taken advantage of determinism in their design, alongside deterministic simulation testing.

So, like FoundationDB, TigerBeetle has logical determinism, where all database code is deterministic and multithreaded concurrency is avoided in the control plane.

However, we go further and also ensure physical determinism, where replicas in a TigerBeetle cluster converge to a byte-by-byte identical state. In other words, across all the replicas in the cluster, the same physical location corresponds to the same content.

This logical and physical determinism makes TigerBeetle amenable to Deterministic Simulation Testing, which helps us run the real consensus and storage engine code in a simulator, which we call the VOPR. Inside the VOPR, non-deterministic, physical interactions like storage and network are replaced with controllable versions, and time is simulated. This allows us to run our distributed database on a single machine, in a single process, with time sped up by orders of magnitude.

We generate random scenarios to explore the state space of the database: network partitions, disk corruptions, and replica crashes all in the presence of concurrent client operations, and test for various safety and liveness invariants throughout.

Because time is simulated, exploring scenarios that would take months to encounter in production takes mere minutes. This means that you can quickly find subtle interleavings of events where bugs typically like to hide, and once a bug is found, it can be reproduced over and over again deterministically. Therefore, DST allows developers to test and debug faster, which in turn means that they can build faster.

But today, I want to talk about a slightly different aspect of DST. We use DST to test TigerBeetle from the inside out, which means that it has complete visibility into each replica’s consensus and storage-level state. With this protocol-awareness, we can peek under the hood of the system and start asking it the hard questions.

We can deeply check safety invariants not just at the database level, but also across consensus and storage. Testing these safety invariants is crucial because safety is hierarchical. Violation of a safety invariant in consensus or storage can ultimately lead to the database violating its core safety invariant of strict serializability.

Because of this, we enforce these safety invariants both in production and in testing. We run with assertions enabled in production that simply crash the replica if a violation is detected, downgrading a catastrophic safety violation to an availability violation. However, gathering global, cluster-level context in production can be expensive, so we leave these expensive checks to our protocol-aware DST.

Consensus Safety

For the consensus protocol, the safety invariant is agreement, i.e. making sure that requests are committed through the write-ahead-log (WAL) in the same order across all replicas.

In production, we validate the consistency of the WAL when a backup receives a commit message from the primary. If we observe that a backup’s WAL diverges from the primary’s, we crash the backup, as this means we’ve violated the protocol’s safety invariant. This is something that should never happen, so we downgrade a safety violation into unavailability.

fn on_commit(self: *Replica, message: *const Message.Commit) void {
    assert(message.header.command == .commit);
    if (self.journal.header_with_op(message.header.commit)) |commit_entry| {
        if (commit_entry.checksum == message.header.commit_checksum) {
            log.debug("{}: on_commit: checksum verified", .{self.log_prefix()});
        } else if (self.valid_hash_chain_between(message.header.commit, self.op)) {
            @panic("commit checksum verification failed");
        }

With protocol-aware DST, we validate this invariant even more deeply. Every time a new request is committed on a replica, our simulator asserts that if that request was committed on another replica, their checksums must match. Effectively, we check that every committed request in the WAL is consistent across all replicas.

    assert((commit_a == commit_b) == (checksum_a == checksum_b));

At runtime in production, we logically check whether our storage is deterministic or not, using the primary replica’s checkpoint_id (the checksum over the references to our index data structures). If we observe that the backup’s checkpoint_id diverges from the primary’s, we crash the backup, downgrading a safety violation to unavailability.

if (message.header.checkpoint_id != self.superblock.working.checkpoint_id() and
    message.header.checkpoint_id !=
        self.superblock.working.vsr_state.checkpoint.parent_checkpoint_id)
{
    @panic("checkpoint diverged");
}

With protocol-aware DST, we take this logical check further by digging deeper into these indexes. For example, for the Manifest, which is an index over the on-disk LSM tree, we checksum the metadata of all tables, across all levels, and assert that the structure of the tree is completely consistent across all replicas.

fn manifest_levels_checksum(forest: *const Forest) u128 {
    var checksum_stream = vsr.ChecksumStream.init();
    for (0..constants.lsm_levels) |level| {
        checksum_stream.add(std.mem.asBytes(&level));

        inline for (Forest.tree_id_range.min..Forest.tree_id_range.max + 1) |tree_id_u16| {
            const tree_id: Forest.TreeID = @enumFromInt(tree_id_u16);
            const tree_level = forest.tree_for_id_const(tree_id).manifest.levels[level];
            var tree_tables = tree_level.tables.iterator_from_index(0, .ascending);

            checksum_stream.add(std.mem.asBytes(&tree_id));
            checksum_stream.add(std.mem.asBytes(&tree_level.table_count_visible));
            while (tree_tables.next()) |tree_table| {
                checksum_stream.add(std.mem.asBytes(&tree_table.encode(.{
                    .tree_id = tree_id_u16,
                    .event = .insert, // (Placeholder event).
                    .level = @intCast(level),
                })));
            }
        }
    }
    return checksum_stream.checksum();
}

checkpoint.put(
    .superblock_checkpoint,
    vsr.checksum(std.mem.asBytes(&superblock.working.vsr_state.checkpoint)),
);
checkpoint.put(.client_replies, checker.checksum_client_replies(superblock));
checkpoint.put(.grid, checker.checksum_grid(Forest, forest, .free_set_from_disk));

So, we assert that if there are no corruptions in the WAL, replicas should never wind up in a state where they need to coordinate. And this is crucial, because imagine a scenario where all replicas crash and restart together, and then unnecessarily coordinate. The cluster would then be stuck; that’s a serious liveness issue!

if (replica.status == .recovering_head) {
    // Even with faults disabled, a replica may wind up in
    // status=recovering_head, in case of a header-prepare view mismatch.
    assert(fault or header_prepare_view_mismatch);
}

This is a scenario where most consensus protocols, including the original VSR, typically assume that recovery happens by copying the full state over from an intact replica. But TigerBeetle’s protocol does things a bit differently. We’re able to recover all copies, even if there’s only 1 remaining copy of the block in the cluster. Each replica takes advantage of the physical storage determinism and fetches only individual, intact blocks from the other replicas, as opposed to copying over the entire state.

And with protocol-aware DST we can test that replicas can recover in these scenarios! In other words, we can assert that each replica repairs its missing blocks from the intact copies on other replicas. If any blocks do remain missing, they must be missing on all replicas.

while (blocks_missing.next()) | block_missing | {
    for (simulator.cluster.replicas) |replica| {
        const storage = &simulator.cluster.storages[replica.replica];

        if (storage.area_faulty(.{
            .grid = .{ .address = block_missing.address },
        })) continue;

        const block = storage.grid_block(block_missing.address) orelse continue;
        const block_header = schema.header_from_block(block);
        if (block_header.checksum == block_missing.checksum) {
            @panic("block found");
        }
    }
}

These are covered in my talk at BugBash ’26, should you wish to dig deeper!