First, automatically checking Paxos is very cool. Nothing I'm saying in any way diminishes that achievement.
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.
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...