Raft / Paxos算法的伊莎贝尔正确性证明

Question

伊莎贝尔能帮助证明筏或帕克斯共识算法的正确性吗？什么地方有正式证据吗？

Answer 1

正式证明档案中的这个条目可能很有用：https://www.isa-afp.org/entries/DiskPaxos.html

Answer 2

Isabelle/HOL (和类似的定理证明器)适用于验证Raft和Paxos等分布式协议。

通常，形式化会涉及系统模型(消息或共享状态、故障？)、状态空间的归纳定义、时间正确性属性的描述以及证明这些属性的相关(归纳)不变量。

在这里可以找到一个教程视频：https://www.youtube.com/watch?v=Uav5jWHNghY

正如lsf37所指出的，2005年起对贾斯基利奥夫和梅兹在形式证明档案中的磁盘帕克斯进行了验证。

经典帕克斯的伊莎贝尔/霍尔形式化已经由Küfner等人“分布式算法的形式化验证:从伪码到校验证明”完成(2012年，更多细节在库夫纳博士论文中)。

此外，有一个伊莎贝尔的证明，在异步设置的一个错误的进程(所谓的“FLP结果”)由Bisping等人从2016年开始协商一致的理论不可能。

对于筏子，有一个Coq/Verdi形式化