  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.
