search

dranov / raft-tla

Other
19 stars 3 forks source link

Inductive invariant for Raft using Apalache #1

Open heidihoward opened 2 years ago

heidihoward commented 2 years ago

It's my understanding that I might find an inductive invariant for the safety of Raft (checked using Apalache) in this TLA+ spec but I cannot seem to find one. Is there one in this repo?

will62794 commented 2 years ago

Hi @heidihoward, sorry to jump in randomly here, but if you are working on an inductive invariant for a Raft TLA+ spec, you may also be interested in this TLA+ inductive invariant that was developed for proving safety of a dynamic (i.e. reconfigurable) version of MongoDB replication's Raft based consensus protocol. The invariant has been formally proven in TLAPS, discussed in more detail here (pdf).

MongoDB's replication protocol differs from standard Raft in subtle ways, so there will not be an exact mapping to Ongaro's original Raft spec, but it may be a helpful foundation to look at, since the underlying protocol is heavily based on Raft. Note that the TLA+ protocol specification is also written at a higher level of abstraction than Ongaro's original spec, but this may also make it easier to understand in some sense. Just thought I would drop a note here about this in case it would be helpful to you!

heidihoward commented 2 years ago

That's very helpful. Thanks so much for the pointer!

The only other inductive invariant in TLA+ for a consensus algorithm that I know of is the work by the @informalsystems team on tendermint using Apalache instead of TLAPS.

Personally, I'm familiar with model checking TLA+ using TLC (and more recently Apalache) but I've never had much success at learning TLAPS so I'm very impressed by what you have achieved!