Formally verified asymptotic consensus in robust networks

TL;DR

This work provides the first machine-checked formal proof of resilient asymptotic consensus for the Weighted-Mean Subsequence Reduced (W-MSR) algorithm under the $F$-total malicious model, using the Coq proof assistant. It proves that resilient asymptotic consensus holds iff the network is $(F+1,F+1)$-robust, and it identifies and clarifies imprecisions in the original paper, including quantifier order, while delivering a formal proof of the safety condition and a strengthened sufficiency result. The authors construct formal proofs of sufficiency and necessity, including a counterexample to necessity, and discuss the challenges of modeling limits and real analysis for asymptotic properties in distributed controls. The work advances formally verified distributed control by enabling rigorous reasoning about robust consensus and lays groundwork for verified implementations under real-number arithmetic and future extensions to time-varying graphs and finite-precision environments.

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.

Figures (3)

• Figure 1: Illustration for $(2,2)$ robustness. In the illustration $(a)$, every node of the set $S_2$ has $2$ neighboring nodes outside $S_2$. Similarly every node in the set $S_1$ has at least $2$ neighboring nodes outside $S_1$. In the illustration $(b)$, there are $2$ nodes in the union $S_1 \cup S_2$ that have $2$ neighbors outside the set. Note that the sets $S_1$ and $S_2$ are disjoint.
• Figure 2: Schematic of the W-MSR update. At time $t$, the node $i$ obtains values from its neighbors and forms a sorted list. The algorithm then removes the largest and the smallest $F$ nodes in the sorted list, or if there are less than $F$ nodes with values strictly greater than or less than the value of $i$, the algorithm removes all those nodes.
• Figure 3: Illustration of the tube of convergence bounded above by $A_M + \epsilon$ and bounded below by $A_m - \epsilon$. We observe the behavior of functions $M(t)$ and $m(t)$ inside this tube of convergence $\forall t \geq t_\epsilon$. We prove that $M(t)$ and $m(t)$ are monotonous $\forall t \geq t_\epsilon$, and they approach the limits $A_M$ and $A_m$, respectively. We start by assuming that $A_M \neq A_m$, but later prove that $A_M = A_m$ by contradiction, thereby proving asymptotic consensus.

Theorems & Definitions (13)

• definition thmcounterdefinition: Malicious node leblanc2013resilient
• definition thmcounterdefinition: F-total set leblanc2013resilient
• definition thmcounterdefinition: F-totally bounded leblanc2013resilient
• definition thmcounterdefinition: $(r,s)$-robustness leblanc2013resilient
• theorem thmcountertheorem
• lemma thmcounterlemma: Safety condition
• proof
• lemma thmcounterlemma
• proof
• lemma thmcounterlemma