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形式化验证。