From the article:

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.

[...]

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)

[...]

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.