我想证明我对多paxos的实现是正确的。是否有任何有效的示例可供我测试？ 或者可以有一些其他方法可以说服其他人我的实现是正确的。
我试图找到一些包含示例的论文，但大多数论文只是指定了算法。
Elasticsearch 背后的公司希望加强对他们是否有设计错误的关注。他们在GitHub上构建了所有算法的TLA+模型，证明算法可以带来安全。然后他们需要检查他们的代码是否偏离模型。他们写了一篇关于以这种方式查找和修复旧错误的博客。这种方法可以防止设计错误，因为您知道预期的实现是正确的。然后，您必须担心佣金错误，这是代码偏离模型的实现错误。显然，这是一项非常重要的工作投资，远远大于实际编写您正在证明的代码。
相比之下，如果你看看谷歌关于使用Paxos的著名谷歌胖乎乎的论文，他们没有使用正式的证明。他们通过测试进行了压力测试，这些测试注入了很长时间的随机消息丢弃和崩溃，以摆脱错误。然后，您没有证据证明它是正确的，只有一些证据表明在数千小时的崩溃和网络错误模拟中没有观察到错误。这种建立信心的练习是编写实现的单个人可以设置和运行的。
Kyle Kingsbury的Jepson项目展示了他如何在其他人的实现中发现和证明错误。他仔细研究了人们声称的安全属性，然后设计了一个测试客户端，并在虚拟机上运行系统并注入网络分区、消息丢失和崩溃。然后，他有一个检查器，用于检查所有搜索不一致的测试客户端看到的所有响应。他在很多系统中发现了很多错误。所以公司现在雇用他来寻找错误。如果他没有发现错误，那不是没有错误的证据，只是让人们感到更自信的东西(通常发现错误！聘请编写开源检查器的人花几个月的时间尝试使您的代码出现故障是一项重大投资。Kyle 教授面对面的培训课程，向您展示如何运行他的开源软件，并练习代码在旧版本的 SQL 数据库中查找错误。我参加了该课程，我强烈推荐它。
在编写自己的实现的情况下，这是一个您将花费多少精力的问题。Paxos被证明是正确的，实现困难是你需要添加到核心算法中的所有现实世界的东西，以创建一个实用的系统。例如，您可能会在一段时间无法访问节点后如何追赶方面遇到错误。运行实验来长时间模拟大量错误，验证所有节点保持不变，并且没有客户端看到不稳定状态，这可能是最可行的方法。检查所有节点是否经历了相同的状态是微不足道的。证明没有客户端观察到节点从未进入的状态更难编码。你可以使用Knassos，这是Kyle用Clojure编写的开源检查器。
最后，华盛顿大学有一门在线课程，在GitHub上编写代码，称为DSLabs，学生必须在一个项目中编写自己的Paxos实现，该项目链接到大学开源检查器，该检查器将检查客户端在模拟网络错误和崩溃期间看到的不一致。由于它都是开源的，您可以使用它来检查自己的实现。你可以阅读一篇关于它的comsci论文，标题为"使用高效的模型检查教授严格的分布式系统"。DSLabs 是用 Java 编写的，所以如果不用 jvm 语言编写，插入你自己的实现可能就不那么容易了。然后，你可以让Java调用以其他语言运行的任何其他进程，所以理论上你可以编写一个Java填充程序，调用在另一个进程中运行的实现。
更新：人们可能对这篇论文感兴趣，它提到证明算法正确的成本需要人数年时间，并且可能比它证明的代码大十倍 https://blog.acolyer.org/2019/11/13/scaling-symbolic-evaluation-serval/
你不能通过例子或测试来证明任何事情。你只能通过证明来证明某事。
所以，为了证明你的多paxos实现是正确的，你需要首先写下一个严格的数学规范，说明什么是"正确的"，然后证明你的实现符合这个规范。