[tlaplus] vertical paxos proof/TLA+ spec?

["j.e....@xxxxxxxxx" <j.e.aten@xxxxxxxxx>]

I'm researching reconfiguration (reliable membership) protocols, and

Vertical Paxos comes up often in the literature.

However, when I read this paper, which seems to be the definition

of Vertical Paxos,

https://www.microsoft.com/en-us/research/publication/vertical-paxos-and-primary-backup-replication/

I don't see a correctness (safety) proof at all. I feel like

I must be missing something. Was it proved elsewhere?

Is there a TLA+ spec I can read?  Implementing it correctly

seems fraught without having at least a machine checked,

or even better, a hand written proof.

Thanks for any pointers!

Jason

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9939a649-3d21-489a-aee4-b25afa6e4568n%40googlegroups.com.