We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.

翻译：我们阐述了如何将分布式算法形式化地表示为模态逻辑中的声明式公理化理论，并以简单投票协议、简单广播协议（Bracha Broadcast）和简单共识协议（Crusader Agreement）作为示例进行说明。该方法具有良好的可扩展性，并已用于发现某工业协议提案中的错误。其核心创新在于利用模态逻辑捕获系统关键属性的声明式高层表示——即算法的逻辑本质——同时抽象掉实现该算法的抽象机器的显式状态转移。这类似于用函数式或逻辑编程语言指定代码与用命令式语言指定代码之间的区别。因此，我们提出了声明式Bracha广播和声明式Crusader协议的公理化表述。我们提出的这种逻辑公理化风格提供了一种精确、紧凑、人类可读的规范，抽象地捕捉了系统的关键属性，同时省略了底层实现细节；它比自然语言描述更精确，又比源代码或其逻辑规范更抽象。这为推理正确性、鲁棒性和故障创造了新的机会，并可作为人机验证工作、设计改进乃至替代协议实现的基础。本文中的证明已在Lean 4中形式化验证。