形式化验证与 Coalgebra 理论

介绍

引言

在我写这篇文章时，这里正在努力使 Anoma 及其组件更加形式化。纯英文规范至少是模糊的，而使事物在数学上更加精确对于 Anoma 的理解和实现都是至关重要的。这其中包括一个名为 Heterogeneous Paxos 的算法的形式化，这是一种去中心化共识算法，旨在允许类似 Paxos 的共识实现，而不对配额做出相同的假设。

异构 Paxos：艾萨克·谢夫、王新文、罗伯特·范·伦塞斯、安德鲁·C·迈尔斯的技术报告

我们使用 TLA+进行了形式化，但我们已转向使用 Isabelle 以更方便地证明定理。你可以在以下链接找到形式化内容：

TLA+形式化

• •Isabelle 形式化
• •在我进行这个项目时，我的核心目标之一是理解如何将并发程序进行数学形式化。一般来说，这会是什么样子？我原本预期这会与更常见的算法形式化有显著不同，但实际上，它并没有我想象的那么新颖。在这篇文章中，我想描述并发程序形式化的基本思想、一些不同的方法以及与更抽象数学的联系。对于这篇文章，我不会详细解释 HPaxos，但我会使用其实现的一些细节来展示一些普遍的观点。你不需要理解分布式共识来理解这篇文章；它只是我的灵感来源。

详情查看[https://anoma.net/research/formalizing-concurrent-programs-the-generalities]