群体协作，用得着高效的分布式协议。然而，开发可靠的分布式协议是一个艰巨的任务，因为一旦协议打破，就会导致灾难性的结果。为了解决这个问题，我们很高兴地宣布，RAFT.TLA现在已经以开放源码的形式公布，提供了一个一流的分布式协议验证工具。
RAFT.TLA是由Leslie Lamport和TAO xie设计的分布式协议RAFT的交互机制和安全证明的高精度模型检查器。RAFT通过引入“领导者”这个概念，解决了分布式系统中困难的一致性问题。而RAFT.TLA通过模拟RAFT的各个阶段，能够抽象出所涉及的具体变量和任务，并验证它们的正确性。这项工具支持 集群大小、失败检测器类型 和 超时类型 的调整，并通过运行测试用例进行测试，验证了它们的正确性。
这个解决方案的重要性非常明显。当一个公司在举行全员会议或者进行最终决策的时候，如果消息中断，或者领导者无法提供有保障的一致性保证，那么将会有大量的人和资源浪费。同时，任何成功的公司都需要一个支持高效协作的强大基础设施，而这项工具提供了这个保障。
我们希望，这个开放源码的工具能够对我们所有的客户和合作伙伴开发更好的分布式系统提供有力帮助。它的目标不仅是在衡量一个协议是否可靠时为我们提供帮助，而且还可以防止一些灾难性的副作用。我们相信，它将成为一个优秀的贡献，为分布式系统的开发提供更可靠的解决方案。
了解更多有趣的事情：https://blog.ds3783.com/