Paxos automatically determined safe and secure

Re:Paxos automatically determined safe and secure by ummonk on Wednesday October 27, 2021 @08:28PM (#29020861)

Has anyone done the same for raft consensus?

[ Parent | on HN ]

Re:Paxos automatically determined safe and secure by _r2gl on Wednesday October 27, 2021 @08:49PM (#29021003)

The conclusion in the paper states it's left as future work.

"Future work also includes automatically inferring inductive proofs for other distributed protocols, such as Byzantine Paxos [15], Raft [90], etc., and exploring the verification of consensus algorithms in blockchain applications. "

https://arxiv.org/pdf/2108.08796.pdf

[ Parent | on HN ]

Re:Paxos automatically determined safe and secure by johnbender on Wednesday October 27, 2021 @09:46PM (#29021366)

Raft has been manually verified which was the hurdle here that makes the result interesting:

https://github.com/uwplse/verdi-raft

[ Parent | on HN ]

Re:Paxos automatically determined safe and secure by baby on Wednesday October 27, 2021 @09:10PM (#29021135)

or for byzantine-fault tolerant consensus like hotstuff?

[ Parent | on HN ]