Distributed architectures are used to improve performance and reliability of various systems. Examples include drone swarms and load-balancing servers. An important capability of a distributed architecture is the ability to reach consensus among all its nodes. Several consensus algorithms have been proposed, and many of these algorithms come with intricate proofs of correctness, that are not mechanically checked. In the controls community, algorithms often achieve consensus asymptotically, e.g., for problems such as the design of human control systems, or the analysis of natural systems like bird flocking. This is in contrast to exact consensus algorithm such as Paxos, which have received much more recent attention in the formal methods community. This paper presents the first formal proof of an asymptotic consensus algorithm, and addresses various challenges in its formalization. Using the Coq proof assistant, we verify the correctness of a widely used consensus algorithm in the distributed controls community, the Weighted-Mean Subsequence Reduced (W-MSR) algorithm. We formalize the necessary and sufficient conditions required to achieve resilient asymptotic consensus under the assumed attacker model. During the formalization, we clarify several imprecisions in the paper proof, including an imprecision on quantifiers in the main theorem.

翻译：分布式架构被用于提升各类系统的性能与可靠性，例如无人机集群与负载均衡服务器。分布式架构的核心能力之一在于其所有节点间达成共识的能力。目前已有多种共识算法被提出，其中许多算法虽附有精巧的正确性证明，但未经过机械验证。在控制论社区中，算法通常以渐近方式达成共识（例如人类控制系统设计与鸟群等自然系统分析），这与Paxos等精确共识算法形成对比——后者在形式化方法领域近年获得更多关注。本文首次提出对渐近共识算法的形式化证明，并解决了其形式化过程中的多项挑战。我们借助Coq证明助手，验证了分布式控制社区广泛使用的加权均值子序列缩减（W-MSR）算法的正确性，并形式化推导了在假定攻击者模型下达成弹性渐近共识的充要条件。在形式化过程中，我们澄清了原论文证明中的若干不精确之处，包括主定理中量词使用的不严谨表述。