[tlaplus] Re: vertical paxos proof/TLA+ spec?

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

For anyone else with the same questions, these guys did

a machine checked proof of Vertical Paxos in 2017; they say it was the first

time it is was machine checked, and that the algorithm is challenging for TLA+. 

They used "EPR", a different logic/model checker. (See abstract below)

- Jason

https://arxiv.org/pdf/1710.07191

See Figure 9, page 35 of "Paxos Made EPR: Decidable Reasoning about Distributed

Protocols", by PADON, LOSA, SAGIV,  SHOHAM, 2017 OOPSLA.

Abstract:

Distributed protocols such as Paxos play an important role in many computer systems. Therefore, a bug

in a distributed protocol may have tremendous effects. Accordingly, a lot of effort has been invested in
verifying such protocols. However, checking invariants of such protocols is undecidable and hard in practice,
as it requires reasoning about an unbounded number of nodes and messages. Moreover, protocol actions
and invariants involve both quantifier alternations and higher-order concepts such as set cardinalities and
arithmetic.

This paper makes a step towards automatic verification of such protocols. We aim at a technique that
can verify correct protocols and identify bugs in incorrect protocols. To this end, we develop a methodology
for deductive verification based on effectively propositional logic (EPR)—a decidable fragment of first-order
logic (also known as the Bernays-Schönfinkel-Ramsey class). In addition to decidability, EPR also enjoys
the finite model property, allowing to display violations as finite structures which are intuitive for users.
Our methodology involves modeling protocols using general (uninterpreted) first-order logic, and then
systematically transforming the model to obtain a model and an inductive invariant that are decidable to
check. The steps of the transformations are also mechanically checked, ensuring the soundness of the method.
We have used our methodology to verify the safety of Paxos, and several of its variants, including Multi-Paxos,
Vertical Paxos, Fast Paxos, Flexible Paxos and Stoppable Paxos. To the best of our knowledge, this work is the
first to verify these protocols using a decidable logic, and the first formal verification of Vertical Paxos, Fast
Paxos and Stoppable Paxos. (emphasis mine)

On Monday, April 14, 2025 at 3:45:47 PM UTC+1 I wrote wrote:

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/4633f161-331b-445a-81f9-a38333e879efn%40googlegroups.com.