[Jweb_Guru]

Raft is more or less a Paxos variant with good marketing. Sure, the proof for vanilla Paxos won't directly apply, but it's not inaccurate to say that it derives heavily from Paxos, which is all the quote above was saying. See https://emptysqua.re/blog/paxos-vs-raft/.

[ncmncm]

...which is what I just said: the proof is about Paxos, not Raft, and so applies to relatively rarebsystems that do rely directly

[ncmncm]

[Buggy HN.] ... relatively rare systems that do rely directly on Paxos, not Raft.

[Jweb_Guru]

If you read the article, you can see that there are barely any material differences between Paxos and Raft. Certainly no more than there are between the description of a program as an abstract state machine and its actual implementation (and based on our other comment thread, you seem to be under the impression that there is not much difference there).

[ncmncm]

I don't need to read the article to know that Paxos and Raft have substantial commonality. That does not make them the same. That does not make a proof about one a proof about the other. That does not make a program that implements one a program that implements the other.

An abstract state machine, such as defines a version of Paxos, maps trivially one-to-one to parts of a program that implements it. A different abstract state machine, such as one that implements Raft, maps trivially one-to-one to a different program.

You might reasonably demonstrate that two different state machines define the same system behavior, but you would need to provide that demonstration. That has not been reported.