Formally verified asymptotic consensus in robust networks

TL;DR

This paper provides the first formal proof of an asymptotic consensus algorithm, verifying its correctness using Coq and clarifying previous ambiguities in the proof.

Contribution

It formalizes and verifies the weighted-mean subsequence reduced (W-MSR) asymptotic consensus algorithm in Coq, addressing challenges and correcting imprecisions in prior proofs.

Findings

Formal proof of the W-MSR algorithm in Coq

Clarification of conditions for resilient asymptotic consensus

Identification and correction of imprecisions in previous proofs

Abstract

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.