search

raft / raft.github.io

website at https://raft.github.io
1.38k stars 215 forks source link

An formally verified specification of Raft in SPIN #151

Closed namasikanam closed 3 years ago

namasikanam commented 3 years ago

Hi, Raft community!

I write a formally verified specification of Raft in SPIN model checker, based on the TLA+ model by Diego Ongaro, which actually cannot be verified by TLA checker. The hyperparameter used in my specification must be constrained very small because of the limited ability of model checking. But it does enable automatic verification.

Thus, I submit my project here and hope it helpful for others.

ongardie commented 3 years ago

Thanks @namasikanam. check.py failed because it expects the implementations to be sorted in order of repoURL. Do you mind updating this?

I don't know how many others watch these PRs. If you're looking to get the word out to other people, I suggest posting to the raft-dev mailing list.

namasikanam commented 3 years ago

I've sorted the implementations.

Thanks for the suggestion. I'm considering writing a more detailed introduction and posting it later.

ongardie commented 3 years ago

Thanks, merged. I think your paragraph above or just a little bit more would be enough to catch the right people's attention on raft-dev.