Introduction

TW Lim Technical Writer

The Raft consensus protocol is one of the foundations of the internet. Raft offers a formal specification in TLA+ and a concrete, detailed implementation guide, and hundreds of groups have created open-source implementations of the algorithm by following the instructions in the guide. It is, by far, the most widely used consensus algorithm in production systems.

Despite the paper’s famously accessible style, we’ve found bugs in every Raft implementation we’ve tested, including HashiCorp Raft, Aeron Cluster, OpenRaft, and MicroRaft — despite the investment in formal methods, careful code review, unit testing, and years of testing in production. The bugs we found manifest as violations of Raft’s main invariant (called state machine safety in the paper, commonly referred to elsewhere as total order delivery). If you’re using a Raft implementation, you might want to check it for bugs.

We’ve sent bug reports upstream. This isn’t intended as a critique of Raft, its authors, its implementers, or any particular implementation. Raft implementations, even with a formal specification and a detailed implementation guide, are not easy to write.

Rather, this is a story about correctness in distributed systems — the inevitability of bugs, the inadequacy of any single approach, and the high cost of learned helplessness.

This is a long post. The first section is a position paper, but the rest is a detailed analysis of the issues we found, using one implementation as an example, a discussion of how we found them, and why we think they’re there.

Why this matters

If you’ve worked on distributed systems, you’ve been part of a war room at some point (if you haven’t, don’t worry, you will be), dealing with an outage like this one, or this one — both of which were caused by consensus failures. When a consensus issue results in an incident, it’s inevitably far reaching and extremely painful to root cause, replicate, and fix. Many consensus issues remain “unsolved”, because they evade reproduction.

It’s hard to know exactly what the real world consequences of these problems are, because consensus protocols sit so low in the stack. Are they corrupting the archive of someone’s personal D&D game? Security risks at a nuclear plant? Delaying trains in Germany? It all depends on where the protocol’s deployed.

What’s certain is that these bugs are a colossal waste of developer time, and affect millions, if not hundreds of millions, of users.

Yet we accept consensus issues and other deep distributed systems bugs as a fact of life — but once upon a time we accepted cholera, and waiting for your turn on the mainframe, as facts of life as well. Developers deserve something better. Everyone who depends on the software we write deserves something better.

Bugs are not a fact of life

We have long accepted consensus bugs as inevitable because consensus protocols are just really, really hard to test properly. To really, thoroughly test a Raft implementation — or any distributed system — you effectively need to imagine every possible thing that could go wrong in your entire stack, and write a test to see if it will break your consensus protocol. It’s virtually impossible to write enough tests to provide this kind of assurance in critical systems.

We get around this in two ways. First, we inflict the testing on our users, in the form of outages, downstream bugs, war rooms, and so on. It’s impossible for a team of developers to write enough tests, but with enough deployments and enough users across enough system configurations, you’re eventually going to find all the problems.

Second, we rely on formal verification, and this is how consensus algorithms are built today. We define a model that we can mathematically prove to be correct, and then we… translate this perfect, platonic thing into code. Most Raft implementations are built this way.

Specifications are not code

Formal verification is a great starting point, in that it helps confirm that a core design is sound. Implementing a distributed consensus protocol without starting from a formal spec would result in many orders of magnitude more bugs than any Raft implementation has.

But the issues here demonstrate the difficulties inherent in going from a formal specification to actual production code. As long as the implementations are being done by unreliable, imperfect programmers (whether humans or LLMs), the actual code, and the systems using it, will only be as solid as the implementors’ assumptions — not the formally verified model.

Furthermore, formal specifications are rarely truly complete — in the case of Raft, the TLA spec covers the core protocol, but doesn’t speak to details like installSnapshot, or replica replacement, or handling network packet corruption.

Testing can actually be simple

Surfacing these bugs didn’t require particularly deep knowledge of consensus or distributed systems. We found these using a simple approach, which a junior engineer could implement in less than a day, literally the simplest state-machine replication workload we could come up with. The key is that this is happening while the system is running in Antithesis, subject to the kind of faults that happen in a real world environment.

We want to emphasize this point because all too often, we encounter a learned helplessness around testing complex systems. Our profession thinks (with some justification) that writing tests for distributed systems requires more expertise, time, or tokens than we have. This results in a state of perpetual under-testing, which in turn results in extraordinary amounts of developer time being wasted on firefighting (to say nothing of the mental and emotional exhaustion).

Developers deserve something better. Everyone who depends on the software we write deserves something better.

Testing Raft

Marco Primi Distributed Systems Engineer

About Antithesis

Antithesis is an autonomous testing platform that runs distributed systems in a deterministic simulation environment, with randomly generated inputs, under aggressive fault injection. To use Antithesis, you deploy a full distributed system to the simulation environment along with a workload — a client that drives the system under test.

Antithesis exposes the system under test to the kind of unpredictable turbulence it will experience in production, within the safety of a simulation environment. By randomizing the inputs and faults, and intelligently searching the state space of the system to see if system invariants are ever violated.

We maintain an internal curriculum of systems and bugs we use to benchmark Antithesis’ bug-finding performance. We’ve been adding consensus benchmarks to the curriculum, so we’ve been testing a lot of Raft implementations.

About Raft

A common architectural pattern in distributed systems is state machine replication (SMR): all replicas in the system run copies of the same deterministic state machine, and the same sequence of commands is delivered to all of them to transform the data/state. This causes the replicas to progress in soft-lockstep — the state after applying N commands is consistent across all replicas, and all replicas eventually apply all commands.

Distributed databases (FoundationDB, Aerospike, etc.), message queues (Kafka, NATS, etc.), key-value stores (etcd, Zookeeper), blockchains (Bitcoin, Ethereum), and many other systems are based on SMR.

A fundamental requirement for implementing SMR is that all replicas must receive the same set of commands in the same order — total order delivery. Total order delivery is simple to describe, but hard to architect in the face of network turbulence, process crashes, and disk failures.

Because total order delivery needs to be guaranteed for SMR to work, most systems rely on one of a handful of messaging abstractions, with atomic broadcast, also known as total order broadcast, being the most common. Raft is viewed as the friendliest atomic broadcast protocol, Paxos and viewstamped replication are also in wide use.

Our testing approach

To test a Raft implementation, we run a 3-node Raft cluster in Antithesis with a simple workload we call Chain of Blocks.

Chain of Blocks tests Raft’s most important invariant: after N commands are applied, the state of all replicas matches. It consists of two trivially simple components:

• A single-state state machine that just hashes the bytes of incoming commands. After each applied command, the state consists of <number of commands applied, current hash>. This is sufficient to allow us to observe state divergence between replicas.
• A stateless client whose only responsibility is submitting new commands that consist of random arrays of bytes.

You can read more about this workload, and see a sample implementation, here.

Components like Raft are developed and reviewed by experts and battle-hardened by years of exposure. So it’s striking to us that this single, simple testing strategy — that a junior engineer could write in an afternoon (or Claude could write for a handful of tokens) — still finds bugs when it’s run in Antithesis.

Results

In all cases, network partitions and turbulence were sufficient to surface examples of divergence (i.e. no node kill/restart required, or disk corruption, or other faults)

Here’s an example snippet from logs that shows a state machine divergence:

[node1]: Applied block 244 (2ad8d...) state: 01fd753a => faf6ba1e
[node2]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c
[node3]: Applied block 244 (c92fb...) state: 01fd753a => dab0977c

After applying 243 blocks, the hashes of all replicas matched (0x01fd753a). Node1 then applies a different 244th command from Node2 and Node3 (0x2ad8d… vs 0xc92fb…). This results in a different state hash after 244 commands applied (0xfaf6ba1e vs 0xdab0977c), violating the primary safety property of Raft (and the underlying atomic broadcast): that all replicas apply the same sequence of command in the same order.

As an example, here’s a detailed look at the bugs we’ve found in one notable open-source Raft implementation during this process. We emphasize that we’ve found similar bugs in other implementations as well, but are going deep rather than broad here and only presenting one set of bugs to keep the length of this post somewhat manageable.

We plan to update this post with details of bugs in the other Raft implementations we’ve worked with.

HashiCorp Raft

Rohan Padhye Research Fellow

HashiCorp Raft is a mature, popular open-source Raft implementation, and the foundational consensus engine underpinning widely-used production infrastructure tools like Consul, Nomad, and Vault.

We do not believe HashiCorp Raft is any less reliable than the other implementations we tested, or that the bugs in HashiCorp Raft are more serious than the bugs in other implementations — they all violate the same core property of state machine safety.

We found three distinct bugs in total: one causes numerous safety violations (i.e., data divergence as described above) and two cause liveness violations (where some nodes or the whole cluster cannot make progress unless an operator intervenes). Our bug report, along with the Chain of Blocks implementation we used, is here.

When run with Antithesis for just one hour of testing, we see a report that looks like this:

Bug 1 - Broken Consensus due to Async Heartbeats

This is the most serious bug we have found. It can affect four of the five safety properties from the Raft paper (Figure 3):

• Log Matching (violated through mechanism A - seen in the report above)
• Leader Completeness (violated through mechanism A - seen in the report above)
• State Machine Safety (violated through mechanism A - seen in the report above)
• Election Safety (violated through mechanism B - not in the report shown above)
• Leader Append-Only (not violated)

Root Cause and Trigger

• The Raft paper assumes that all the operations (handling RPCs, client requests, elections, etc.) are atomic and don’t interleave with each other. Essentially, every node in the protocol is a finite-state machine.
• In HashiCorp raft, most state-changing operations are handled by a big switch-loop in the main thread, with several other floating goroutines doing async work that should not affect protocol state (e.g., peer-peer “replication” routines for dispatching append-entries, and per-connection “transport” goroutines that listen for incoming RPCs and hand them off to the main thread for processing).
• EXCEPT there is an optimization that diverges from the protocol: incoming heart-beat messages (i.e., AppendEntries without an entry) are handled on the I/O “transport” thread itself, instead of queuing it up for the main thread’s loop like with other RPCs. Presumably, this is to quickly reset the keep-alive timers and reduce spurious re-elections.
• CAVEAT is that an incoming heart-beat message (like any other AppendEntries RPC) can change the state if it carries a new term when someone else was elected leader, and this bumps up the global currentTerm which everything else in the main thread relies on, and also sets the current state to be FOLLOWER. It is definitely not sound to perform these state changes concurrently with the main thread, and it can lead to different types of race condition bugs.

Mechanism A - Incoming heartbeat races with dispatchLogs() on main thread

Here’s how the bug causes divergence in a 3-node setup A/B/C:

• Assume the network link between node A and node B is down.
• Node A becomes candidate for term T, requests votes (eventually gets it from Node C)
• Node B also runs for term T but no votes
• Node B becomes candidate for term T+1, requests votes (gets it from Node C)
• Node B wins election for term T+1
• Node A wins election for term T (just received the old vote from Node C)
• Node B sends out heart-beat AppendEntries with term=T+1, which Node A doesn’t immediately receive
• Node A gets a client request to apply a new data entry X, and it still thinks it is a leader for term T, so on the main thread it prepares to create a log entry (data=X, term=T) and send out AppendEntries to peers.
  • HOWEVER: Just before it can create the log entry, the heart-beat from Node B sent in step 7 above reaches, setting currentTerm=T+1. Because this is done on the fast-path on the network-transport thread, it races with the main thread.
  • The main thread ends up preparing a log entry (data=X, term=T+1) and also dispatching AppendEntries with these values before the next main-loop iteration where it realizes it is actually now a follower for term T+1.
• Things get really bad from here. Some nodes apply this bogus data=X, term=T+1 to their logs, while others follow whatever Node B (the true leader for term T+1) says, e.g., they might apply data=Y at the same index with term=T+1. Logs diverge in data but get committed since all say term T+1 for the same index. State machines diverge.

Mechanism B - Incoming heartbeat races with requestVote() on main thread

The same bug can cause another kind of safety violation when the async heartbeat handler races with a concurrent handler for the RequestVote RPC on the main thread. If both the incoming heartbeat and the RequestVote carry higher-numbered but different terms T1 and T2 respectively — this is possible when the receiver just recovers from a fault and is catching up to queued messages from peers — and if T1 is less than T2, then it is possible for the receiver to (i) realize the heartbeat’s term T1 is higher than its current term, then (2) on the main thread processing RequestVote realize that T2 is higher than its current term and so set its current term to T2 and then grant a vote; and then (3) back on the heartbeat handler’s thread set its current term to the lower value T1. Needless to say, it should never be possible for a node that has granted a vote for term T2 to regress its current term back down to a lower value T1! When this node at some later point increments its term to T2 again, it has no memory of the fact that it has already voted in this term.

In summary, the race can eventually cause a node to grant two votes in the same term (T2 above), which in the worst case can lead to two different nodes being elected as leader in the same term! Here are some sample log messages from HashiCorp Raft when we have observed this race condition and its violation of election safety:

  20:11:59.941133 [DEBUG] node-1: vote granted: from="node-2" tally=2 term=286
  [...]
  20:11:59.941133 [INFO]  node-1: election won: tally=2 term=286
  [...]
  20:11:59.944273 [DEBUG] node-0: vote granted: from="node-2" tally=2 term=286
  [...]
  20:11:59.944274 [INFO]  node-0: election won: tally=2 term=286

Bug 2 - Deadlock after Leadership Transfer

This bug causes a liveness issue — a leader node is unable to service client requests or commit new entries while the cluster is healthy. The root cause is a deadlock during a leadership transfer operation (a Raft protocol extension used by Consul where you can ask a current leader to transfer leadership to someone else, say for upgrades) that does not immediately signal any warnings but bites you way into the future by getting the whole cluster stuck.

• When you initiate a leadership transfer from A to B the current leader A first tries to get B’s logs up to date via an async replication thread.
• The leadership transfer logic is a separate goroutine that waits for this replication before telling B to take over.
• While all this is happening, A might have to step-down as leader for unrelated reasons (e.g., the lease timer runs out, or it cannot reach a quorum due to network) and say another node C becomes leader.
• When A steps-down as leader, it aborts all replication threads (including the A—>B catchup) but the leadership transfer goroutine is still blocked waiting for it to complete (an implementation bug).

There is no problem so far, because C is the new leader and it does its job for a while.

• Unfortunately, the leadership transfer goroutine in A has set a global flag “leadership transfer in progress” and this flag cannot be unset until it is unblocked… but it never will be!!!
• Crucially, this flag does not prevent it from participating in elections and the flag does not get reset if it wins a future election.
• So in the future, A can legitimately get re-elected as leader but it will refuse to accept any client requests and stall on future commits with the reason “leadership transfer in progress”.
• When the network is healthy and A is a leader, there is no way to get out of this other than rebooting the node A to clear the flag.

We caught this using an Antithesis eventually test command that checks for commit progress after fault injection is turned off.

Bug 3 - Livelock in Snapshot Installation

This bug causes a liveness issue: a follower node becomes unable to replicate log entries and is effectively not able to participate in the consensus protocol. The bug can also cause resource exhaustion, where the node starts creating a potentially unbounded number of temporary snapshot files on disk.

The root cause for this bug is painfully simple: in the version of HashiCorp Raft we tested, the implementation of the InstallSnapshot RPC simply does not follow Rule 7 from Figure 13 in the Raft paper which handles the case when an incoming snapshot represents a state that diverges from the receiver’s uncommitted log entries. In the paper, Rule 7 says:

“discard the entire log”

HashiCorp Raft does not discard the existing log, and so after installing the snapshot its state machine can, in some cases, disagree with the data in its own (stale) log entries.

At first, this might sound benign because the state machine should be the final source of truth. However, when the node receives a subsequent AppendEntries RPC from the leader, it faithfully implements a part of the protocol (Rule 2) that says: “[reject AppendEntries] if log doesn’t contain an entry at prevLogIndex whose term matches prevLogTerm”. So, because of the stale logs, the follower rejects subsequent AppendEntries, causing the leader to respond with a new InstallSnapshot, and this cycle goes on forever.

We caught this using an Antithesis eventually test command that checks for state-machine convergence after fault injection is turned off. Sample logs from a test run look like this:

2026-07-07T17:17:13.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:17:15.954Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:48504->10.89.0.4:8300: i/o timeout"
2026-07-07T17:17:23.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:17:26.038Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29848]: read tcp 10.89.0.7:35706->10.89.0.4:8300: i/o timeout"
2026-07-07T17:17:33.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:17:36.135Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30394]: read tcp 10.89.0.7:37032->10.89.0.4:8300: i/o timeout"`
2026-07-07T17:17:43.072Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:17:46.249Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 29575]: read tcp 10.89.0.7:54324->10.89.0.4:8300: i/o timeout"`
2026-07-07T17:17:53.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:17:56.381Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30303]: read tcp 10.89.0.7:57842->10.89.0.4:8300: i/o timeout"`
2026-07-07T17:18:03.072Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:18:06.626Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31122]: read tcp 10.89.0.7:46978->10.89.0.4:8300: i/o timeout"
2026-07-07T17:18:13.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:18:17.032Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 30758]: read tcp 10.89.0.7:54192->10.89.0.4:8300: i/o timeout"
2026-07-07T17:18:23.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:18:27.745Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 31850]: read tcp 10.89.0.7:36218->10.89.0.4:8300: i/o timeout"
2026-07-07T17:18:33.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:18:39.083Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 33943]: read tcp 10.89.0.7:53700->10.89.0.4:8300: i/o timeout"
2026-07-07T17:18:43.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"
2026-07-07T17:18:51.725Z [ERROR] node-1: failed to appendEntries to: peer="{Voter node-0 raft-node-0:8300}" error="msgpack decode error [pos 38402]: read tcp 10.89.0.7:52390->10.89.0.4:8300: i/o timeout"
2026-07-07T17:18:53.073Z [INFO]  node-0: snapshot network transfer progress: read-bytes=0 percent-complete="0.00%"

2026-07-07T17:18:55.497Z [ERROR] eventually-fsm-convergence: convergence-check give-up; cluster healthy but did not converge: attempts_taken=24 per_node="map[raft-node-0:8400:map[applied_index:534 last_index:535 reachable:true state:Follower term:74 value:23641] raft-node-1:8400:map[applied_index:569 last_index:569 reachable:true state:Leader term:74 value:25232] raft-node-2:8400:map[applied_index:569 last_index:569 reachable:true state:Follower term:74 value:25232]]"

Reflections

TW Lim Technical Writer

If there is a single lesson to be learned here, it’s that formal methods alone cannot ensure that software works, because the formal specification still needs to be implemented, and even if you have mechanized verification, you’re verifying the model and not the implementation itself.

We believe formal methods are useful and necessary — they can confirm the basic soundness of a design, and provide a map that saves engineers from many of the errors that can arise in the implementation of a complex system.

But as these bugs show, errors continue to arise when translating the formal specification to production code. In the course of our work with various Raft implementations, we identified a number of assumptions in the Raft paper that remain implicit. An implementer who misses any of these details is likely to run into trouble.

Assumption 1: Each node is a synchronous process

Marco Primi Distributed Systems Engineer

The paper implicitly assumes that each node is a synchronous process, performing atomic state transitions when handling RPCs and updating its own internal state. The TLA+ spec is designed as such.

At the same time, none of the implementations we’ve looked at have actually been a synchronous process, and there’s no explicit guidance in the implementation guide as to whether and how one can deviate from the synchronous design.

Consider the following situation: Can a leader with an outstanding RPC request respond to a vote, or does it need to wait for a response||timeout? Or should it respond, shut down the request and disregard a future response in order to stay correct?

HashiCorp Raft is mostly synchronous in handling RPCs, with a single thread in a select loop, except when it isn’t — it does asynchronous heartbeat handling, bypassing its main loop, and this is what allows Bug #1 to creep in.

Assumption 2: Each response can be mapped to a request

In the Raft paper, every call is made using RPC, which means that every response can be mapped to a request.

If one implements Raft on top of simple TCP or UDP, and doesn’t realize that request/response correlation is a crucial part of correctness, bad stuff can easily happen.

If you’re not working in a language with a nice RPC library, it’s not obvious how to establish this correspondence. For example, the Raft authors have a simulation on their website, which for obvious reasons is often considered a demo/canonical implementation even though they’ve never described it as such. But even their own implementation deviates from the protocol and includes an extra matchIndex field in the AppendEntries response in order to avoid matching requests to responses.

Assumption 3: currentTerm and votedFor are consistent

Rohan Padhye Research Fellow

Figure 2 of the Raft paper states:

One key assumption is that currentTerm and votedFor are consistent, because the latter records the vote in the current term. If these go out of sync bad things can happen, especially if votedFor is null.

For safety, the writing of these values to persistent storage should be done atomically. But in the protocol, these values actually change at different places, so ensuring that both values are updated together is subtle.

The online simulator in JavaScript does not actually distinguish persistent state from in-memory state, so there is no “reference implementation” of how to do this.

HashiCorp Raft, for instance, deviates from the protocol and non-atomically stores three separate values for currentTerm, lastVoteTerm and lastVoteCand, with a worst-case risk to performance but not safety (i.e., it might persist an updated lastVoteTerm and then crash before updating lastVoteCand, but when it restarts it will just have a pre-determined vote for that term instead of choosing a candidate as normal).

Assumption 4: The entire protocol is formally verified

Figures 2 and 13 in the Raft paper state, respectively:

Rule 2 for AppendEntries and Rule 6 for InstallSnapshot creates a potential pitfall. If you implement this naively when you have discarded your log because of a previous InstallSnapshot, you end up doing the wrong thing (most likely creating infinite loops of RPCs between leader and follower, as I have painfully discovered).

The Raft TLA+ spec and the authors’ simulation don’t actually include InstallSnapshot (though Diego Ongaro’s PhD thesis does discuss the nuances in more depth), so different implementations use different workarounds. HashiCorp Raft, for instance, just avoids discarding logs altogether — which led to Bug #3 above.

Bug #2 above, the deadlock, is in a feature called “leadership transfer” which is an extension to the core protocol. Like InstallSnapshot, this feature was never formally verified in the TLA+ spec.

Conclusion

TW Lim Technical Writer

We have long accepted bugs as inevitable. Distributed systems are almost impossible to test thoroughly because their state spaces are so large, and as our stacks get more complex, the problem only gets worse.

But technological progress also moves the frontier of what’s possible. We ended cholera in the developed world by building water treatment plants and sewage systems. We no longer wait for mainframes because we’ve made computing power cheap and abundant.

The abundance of compute is a recent phenomenon. It’s held true for maybe the last 15 years, less than a tenth of the history of computing. It’s spurred, among other things, the recent surge of interest in formal verification — the hope that mechanized proof and model checking can finally become easy enough, and cheap enough, that we’ll be able to apply these approaches wherever we need. But what our experience with Raft has shown is that implementations of even mechanically proven models can have flaws, because there’s no mechanical way to check the implementors’ assumptions.

Fortunately, cheap and abundant compute has also made it possible to test software in ways we couldn’t before. And the other thing our testing of Raft has shown is that when you run systems under fault, even basic testing methods reveal issues that would once have taken months of manual testing to find.

Developers deserve something better, and so does everyone who depends on our software.