> Paxos is one of the most important examples of the category
>“Most—if not all—consensus algorithms fundamentally derive concepts from Paxos,” Goel said.
A lot of burying the lede here, trying to imply Paxos powers many more applications than it actually does. While Paxos is in decent widespread use, and influential, I find some of the verbiage here lying by omission.
Next, the result is entirely unsurprising. Paxos is proved correct since its construction was formally derived[1] to be so.
Finally, this is a nice opportunity to highlight the distinction between program verification and program derivation. In general, it's considerably easier to derive a program that has a property than it is to verify that an arbitrary program has a property. For example the halting problem is uncomputable in general and yet it's easy for a competent programmer to derive loops that always terminate. This is analogous to how it's much easier to determine that some large number is the product of two primes when you yourself produced it by multiplying those same two primes than it is to factor the product when the multiplier and multiplicand are not already known.
[1] https://www.microsoft.com/en-us/research/uploads/prod/2016/1...
As for the actual research, it probably needs much closer reading, but if they can automatically infer nontrivial inductive invariants that's huge for automatic verification, since this is the usual stumbling block for those kinds of tools.
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.