:) I'm only using "seem" to indicate the limits of my knowledge.
I was just hoping someone would chime in with a
link to stronger/formal proof for VSR. Are you aware of any?
So, yes, to my limited knowledge, I've not found any
existing formal proofs for VSR.
The 2012 VSR revisited clearly labels their arguments informal;
in section 8: "In this section we provide an informal discussion of the correctness of the protocol."
I'd be delighted to learn of any formal / machine checked
proofs of VSR ; equivalent to the Verdi project for Raft.
These are elaborate and subtle protocols, easy
to get wrong.
In particular when it comes to things like
reconfiguration, even Raft had the famous 2016
bug in the simpler of its two reconfiguration protocols.
Note that Verdi did not attempt to verify the reconfiguration
protocol; apparently it was too difficult.
There was an attempt earlier this year to give a
proven reconfiguration protocol for Raft called Recraft[1],
based on an earlier paper called Adore[2]. They
discuss why reconfiguration is so difficult to prove.
It has to do with circularity.
"ReCraft: Self-Contained Split, Merge, and Membership Change of Raft Protocol" by Kezhi Xiong, Soonwon Moon, Joshua Kang, Bryant Curto, Jieung Kim, Ji-Yong Shin. last revised 28 Apr 2025, v2.
I'm not completely convinced yet that ReCraft works;
at one point I thought they assumed away certain
scenarios -- but I need to revisit it with a close reading.
At a minimum, reading the Adore paper's discussion of
how much subtlety is involved is pretty compelling.
My conclusion is that formal
proof is an absolute necessity to have a fighting
chance at a correct implementation--especially when
it comes to reconfiguration.
I don't mean to trap you, my anonymous friend :) but does the formal proof for Raft in Coq via Verdi not apply—at least in spirit—to the essential view change and SMR protocol for Viewstamped Replication? And, similarly, would you say that Viewstamped Replication's core view change and SMR protocol is really that different from Multi-Paxos as a superset—such that that proof also wouldn’t carry over?
I agree that proofs are sensitive to modeling choices. But the reason I ask is that the literature generally treats the core of these protocols (view change + SMR—reconfiguration aside for now) as essentially equivalent.
For example, I'm sure you're aware of Heidi Howard's work here, which unifies consensus under one framework, the main differences being election style (i.e. Raft does random, VSR does round-robin) and terminology, not fundamental mechanics. The upside being that optimizations and sub-protocols, such as reconfiguration, can then be shared across protocols.
To your point about reconfiguration, reconfiguration sub-protocols are a field in themselves, and here it’s common to mix and match. To be clear, I'm not aware of a proof for the reconfiguration sub-protocol in '12 VRR (and I've found a bug in its client crash recovery sub-protocol—with Dan Ports finding another in its recovery sub-protocol), but again, as Howard notes, since the SMR cores are equivalent, you can adopt a reconfiguration sub-protocol or session sub-protocol that has been proven—at least this is common practice in production systems.
I hope the spirit of the argument is clear. And trust that none of this changes the OP point: that VSR pioneered the field and that Raft (in the authors' own words) is "most notably" similar to Viewstamped Replication.
(Let's not get into the subject of actual implementation correctness, which is orders of magnitude harder than formal design proofs, or the fact that the formal proofs in question still lack for a storage fault model—for example, many Raft implementations violate the findings of “Protocol-Aware Recovery for Consensus-Based Storage”)
Are you intending to suggest there are no formal proofs since?
For example, you compare ‘14 Raft against ‘88 VSR, ignoring the interim progress made by MIT with ‘12 VSR?
It would seem fair to compare the latest version of both, no?