With Cláudio Lourenço I am investigating the use of Why3 to verify safety properties of TLA+ specifications (without temporal operators). We have successfuly verified the Paxos consensus algorithm, following Lamport’s refinement of the abstract Voting protocol. We will report on this soon.
Verifying Paxos by Refinement with Why3
|
Oct 11, 2022