# Revisited Convergence of a Self-stabilizing BFS Spanning Tree Algorithm

Karine Altisen, Marius Bozga

► To cite this version:

Karine Altisen, Marius Bozga. Revisited Convergence of a Self-stabilizing BFS Spanning Tree Algorithm. Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2025), Jun 2025, Lille, France. pp.154-170, 10.1007/978-3-031-95497-9_9. hal-05113962

HAL Id: hal-05113962

https://hal.science/hal-05113962v1

Submitted on 16 Jun 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Revisited Convergence of a Self-Stabilizing BFS
Spanning Tree Algorithm*

Karine Altisen[0000-0001-8344-1853] and Marius Bozga[0000-0003-4412-5684]

Univ. Grenoble Alpes, CNRS, Grenoble INP*,*, VERIMAG, 38000 Grenoble, France
[Karine.Altisen,Marius.Bozga]@univ-grenoble-alpes.fr
http://www-verimag.imag.fr/

**Abstract.** We provide a constructive proof for the convergence of Dolev *et al*. BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq/Rocq-based framework for certification of self-stabilization algorithms.

**Keywords:** spanning tree algorithm, self-stabilization, constructive proof, proof assistant, Coq/Rocq

# 1 Introduction

To obtain properties about distributed systems is a difficult task. Indeed, such
systems generally involve an arbitrary number of participants, interconnected
and communicating according to arbitrary or specific topologies. Their execu-
tion could be subject to various assumptions about the degree of asynchro-
nism between participants. The context in which those systems are considered
is increasingly complex, for example, large scale distributed systems, made of
heterogeneous devices, running in highly dynamic networks. Above all, every
distributed system nowadays requires some fault tolerance properties which are
particularly difficult to handle. Therefore, the proofs for distributed algorithms
quickly become complex and may lead to errors [24].

In this context, the common practice for establishing the correctness of dis-
tributed algorithms was to provide proofs on paper. But, computer-aided val-
idation tools are being developed as a method to improve those practices. In
particular, many approaches are based on model-checking (see e.g., [8], [28]) or
controller synthesis (see e.g., [19], [29]). However, those methods usually face the
large execution space, restricting their applicability. Furthermore, they either re-
quire a complete definition of the full context of execution (such as the number

<footnote>*** Institute of Engineering Univ. Grenoble Alpes</footnote>

<footnote>* This research has been partially supported by the French ANR projects ADAPT ANR-23-CE25-0004, SKYDATA ANR-22-CE25-0008 and PAVEDYS ANR-23-CE48-0005</footnote>
of participants, the topology of the network, etc) or provide parametric solutions (e.g., for N participants where N is a parameter) which are often restricted due to undecidability limitations [9].

On the other hand, the use of a proof assistant such as Coq/Rocq [27] allows to formalize the proofs and automatically check (or certify) their correctness for a given distributed algorithm, for every instantiation of the parameters such as the topology or the number of participants. Note that a proof assistant is not meant to derive any proof: the proof designer comes with (at least) a sketch of the proof and the tool is used as a guidance to enumerate cases, avoid flaws and clarify the assumptions. Once completed, the proof has been fully checked by the tool and its soundness is guaranteed. Many frameworks have been developed to certify the proof of some distributed algorithms using various proof assistant such as Coq/Rocq [1,13,6], TLA+ [15,23] or Isabelle/HOL [11,21,22].

We focus here on distributed self-stabilizing algorithms. Self-stabilization [17] is a lightweight fault tolerance property to withstand transient faults: once such faults hit a self-stabilizing system, it is guaranteed to recover a correct behavior within finite time. Note that no assumption is made on the nature of the transient faults (memory corruption, topology changes, etc). But, once those faults cease, there is a finite period — the stabilization time — during which the system may misbehave (notably its safety guarantees are no longer ensured during this recovery period). In this paper, we are interested in the proof of self-stabilization of a BFS spanning tree algorithm by Dolev et al. [18].

*Related Work* The correctness of several non fault-tolerant distributed algorithms has been certified, (see e.g., [10,20]). Certification of fault-tolerant, yet non self-stabilizing, distributed systems has been addressed using various proof assistants, e.g, in Isabelle/HOL [12,21,11,22], TLA+ [15,16], Coq/Rocq [26], NuPRL [25]. This approach is called *robust* fault tolerance; it masks the effect of the faults (whereas self-stabilization is non-masking by essence). In the robust approach, many results are related to agreement problems, such as consensus or state-machine replication, in fully connected networks. Moreover, many works only certify the safety property of the considered problem (see e.g., [15,16,25,26]). However, both liveness and safety properties are certified in [12,22,11]. Finally, robust fault tolerance has also been considered in the context of mobile robot computing: using the PACTOLE Coq/Rocq framework, impossibility results for swarms of robots that are subjected to Byzantine faults have been certified [6,14].

Several frameworks to certify self-stabilizing algorithms using the Coq/Rocq proof assistant have been proposed, e.g., [13,1]. In particular, the PADEC Coq/Rocq library provides a framework to develop proofs of self-stabilizing algorithms written in the atomic state model [17], and allows various assumptions defined in the literature. For instance, the asynchronism of the system can be defined using several levels of fairness. Notably, it includes use cases and support to prove the composition of self-stabilizing algorithms [2], their time complexity in steps [3] and rounds [4] (Rounds provide a measure of time taking into account the parallelism of the system whereas steps provide a sequential measure).
The research on proving termination (i.e. convergence) of distributed algorithms is extremely vast. Usually, formal techniques such as ranking/potential functions (e.g., [3]), well-founded orders (e.g., [1]) provide direct means to prove the termination over all executions. Alternatively, by the principle of the excluded middle, termination follows from a proof of the absence of non-terminating runs. That is, proofs of termination by contradiction usually exhibit contradictions in the case non-terminating executions are presumed possible. The principle of the excluded middle is, however, not allowed in intuitionistic logics and hence impossible to use in the constructive proof assistant Coq/Rocq [7] (unless changing the basic set of axioms).

*Contributions* In this paper, we revisit the proof of convergence of the self-stabilizing Dolev *et al.* BFS spanning tree algorithm [18]. The first proof of convergence of this algorithm has been provided in [18], that is, the same paper where the algorithm has been introduced; but this proof is restricted to some restricted fairness assumptions. Since then, other proofs have been proposed. As [18], [5] proves the self-stabilization of the algorithm under the mild assumption of a weakly fair daemon, that is, by restricting the asynchronism along the executions of the algorithm; this proof has been formalized, developed and mechanically checked in PADEC [4]. While relaxing the fairness assumption, [5] also provides a non-constructive proof, by contradiction, working under the explicit assumption that the diameter of the graph is a priori known and used as a bound on some of the variables of the algorithm.

In this paper, still with no fairness assumption, we provide, a contrario, a constructive proof of the result which has been fully formalized and mechanically checked in PADEC. Our contribution is twofold:

- We provide the first constructive proof of the convergence of the Dolev *et al.* BFS spanning tree algorithm under the most general execution assumptions (i.e., unfair daemon, unbounded variables). The proof exploits a novel potential function, allowing for a more refined understanding of the system executions towards convergence.

- The convergence proof has been fully formalized and automatically checked using the PADEC framework. The result can therefore be fully trusted and moreover, illustrates the capabilities of the PADEC framework to formally handle distributed algorithms and their properties.

*Coq/Rocq Development.* The development for this contribution represents about 5,155 lines of Coq/Rocq code (#loc, as measured by coqwc), precisely #loc: spec = 1,111; proof = 3,662; comments = 382. It is available as an online browsing documentation at https://www-verimag.imag.fr/PADEC-1063.html. We encourage the reader to visit this web-page for a deeper understanding of our work.

*Organization.* The paper is organized as follows. Section 2 recalls the Dolev *et al.* algorithm for the construction of BFS spanning trees. Section 3 provides a
brief overview of the PADEC framework and the formal encoding of the above-
mentioned algorithm. Section 4 provides the proof of convergence. Section 5
elaborates on the definition of the potential function over system configurations,
that is, the key ingredient ensuring that the proof is constructive and therefore
representable in PADEC. Finally, Section 6 concludes and provides directions
for future work.

## 2 Dolev et al. BFS Spanning Tree Algorithm

The Dolev *et al.* BFS spanning tree algorithm [18] is a self-stabilizing distributed algorithm that computes a BFS spanning tree in an arbitrary rooted, connected, and bidirectional network. By "bidirectional", we mean that each node can both transmit and acquire information from its adjacent nodes in the network topology, i.e., its neighbors. The algorithm being distributed, these are the only possible direct communications. "Rooted" indicates that a particular node, called the root and denoted by $r$, is distinguished in the network. As in the present case, algorithms for rooted networks are usually semi-anonymous: all nodes have the same code except the root.

This algorithm was initially written in the Read/Write atomicity model. We study, here, a straightforward translation into the *atomic-state model*, denoted *BFS*, and presented as Algorithm 1. Notice that, as in the original presentation [18] and contrarily to other adaptations (see e.g., [5]), the variables are not assumed to be bounded.

In the *atomic-state model*, nodes communicate through locally shared variables: a node can read its variables and the ones of its neighbors, but can only write to its own variables. Every node can access the variables of its neighbors through local channels, denoted by the set *Channels* in Algorithm 1. The network is locally defined at each node *p* using constant local inputs. The fact that the network is rooted is implemented using a constant Boolean input called *proot* which is false for every node except *r*. The input *pneighbors* is the set of channels linking *p* to its neighbors. When it is clear from the context, we do not distinguish a neighbor from the channels to that neighbor.

The code of Algorithm 1 is given as three locally-mutually-exclusive actions
written as: **if condition then statement**. We say that an action is *enabled* when
its condition is true. By extension, a node is said to be enabled when at least
one of its actions is enabled. The *semantics of the system* defines an execution
as follows. The system current *configuration* is given by the current value of all
variables at each node. If no node is enabled in the current configuration, then
the configuration is said to be *terminal* and the execution is over. Otherwise,
a *step* is performed: a *daemon* (an oracle that models the asynchronism of the
system) *activates* a non-empty set of enabled nodes. All activated nodes choose
one of their enabled actions in the current configuration and then, *atomically
execute* the associated statements, leading the system to a new configuration.

Assumptions can be made about the daemon. Here, we consider the most
general asynchrony assumption, namely the *unfair daemon*, meaning that it can
**Algorithm 1** Algorithm *BFS*, code for each node *p*.

**Constant Local Inputs:**

*p-neighbors* ⊆ *Channels*; *proot* ∈ {*true*, *false*}

/* *p-neighbors*, as other sets below, are implemented as lists */

**Local Variables:**

*p.d* ∈ N; *p.par* ∈ *Channels*

**Macros:**

*Dist*<sub>*p*</sub> = min{*q.d* + 1 | *q* ∈ *p.neighbors*}

*Par*<sub>dist</sub> returns the first channel in the list {*q* ∈ *p.neighbors* | *q.d* + 1 = *p.d*}

**Action for the root, i.e., for *p* such that *proot* = true**

Action *Root*: if *p.d* ≠ 0 then *p.d* := 0

**Actions for any non-root node, i.e., for *p* such that *proot* = false**

Action *CD*: if *p.d* ≠ *Dist*<sub>*p*</sub> then *p.d* := *Dist*<sub>*p*</sub>

Action *CP*: if *p.d* = *Dist*<sub>*p*</sub> and *p.par.d* + 1 ≠ *p.d* then *p.par* := *Par*<sub>dist</sub>

choose any non-empty subset of the enabled nodes for execution. In contrast, *fair daemons* would guarantee additional properties. For example, a *strongly* (resp. *weakly*) *fair daemon* ensures that every node that is enabled infinitely (resp. continuously) often is eventually chosen for execution by the daemon.

In Algorithm *BFS*, each node *p* maintains two variables. First, it evaluates in *p.d* its distance to the root. Then, it maintains *p.par* as a pointer to its *parent* in the tree under construction: *p.par* is assigned to a neighbor that is closest to the root (*n.b.*, *r.par* is meaningless). Algorithm *BFS* is a self-stabilizing BFS spanning tree construction in the sense that, regardless the initial configuration, it makes the system converge to a terminal configuration where *par*-variables describe a BFS spanning tree rooted at *r*. To that goal, nodes first compute into their *d*-variable their distance to the root. The root simply forces the value of *r.d* to be 0; see Action *Root*. Then, the *d*-variables of other nodes are gradually corrected: every non-root node *p* maintains *p.d* to be the minimum value of the *d*-variables of its neighbors incremented by one; see *Dist*<sub>*p*</sub> and Action *CD*. In parallel, each non-root node *p* chooses as parent a neighbor *q* such that *q.d* = *p.d* − 1 when *p.d* is locally correct *i.e.*, *p.d* = *Dist*<sub>*p*</sub>) but *p.par* is not correctly assigned *i.e.*, *p.par.d* is not equal to *p.d* − 1); see Action *CP*.

## 3 The PADEC Framework

PADEC [1] is a general framework, written in Coq/Rocq [7], to develop mechanically checked proofs of self-stabilizing algorithms. It includes the definition of the atomic-state model and its semantics, tools for the definition of the algorithms and their properties, lemmas for common proof patterns, and case studies. Definitions in PADEC are designed to be as close as possible to what is common practice in the self-stabilizing research community. Moreover, it is made general enough to encompass many usual hypothesis (e.g., about topologies or daemons).

In PADEC, the finite network is described using types *Nodes* and *Channels*, which respectively represent the nodes and the links between nodes. The dis-
tributed algorithm is defined by providing a local algorithm at each node. This
latter is defined using a type *States* that represents the local state of a node
*i.e.*, the values of its local variables and a function *run* that encodes the local
algorithm itself and computes a new state depending on the current state of the
node and that of its neighbors.<fnref n="1" />

The model semantics defines a *configuration* as a function from *Nodes* to *States* that provides the local state of each node. The type of a configuration is given by $\Gamma \stackrel{def}{=} \textit{Nodes} \to \textit{States}$. An *atomic step* of the distributed algorithm is encoded as a binary relation over configurations, denoted by **Step** $\subseteq \Gamma \times \Gamma$, that checks the conditions given in the informal model; see Section 2. An *execution* *e* is a finite or infinite stream of configurations, which models a *maximal* sequence of configurations where any two consecutive configurations are linked by the **Step** relation. “Maximal” means that *e* is finite if and only if its last configuration is terminal. We use the coinductive<fnref n="2" /> type *Exec* to represent an execution stream along with a coinductive predicate *isExec* to check the above condition. Daemons are also defined as predicates over executions (in the case of the unfair daemon, this predicate is simply equal to *true*).

Self-stabilization in PADEC is defined according to the usual practice: the
property is formalized as a predicate (*selfStabilization SPEC*) where *SPEC* is
a predicate over executions that models the specification of the algorithm. An
algorithm is *self-stabilizing w.r.t. the specification SPEC* if there exists a set
of legitimate configurations that satisfies the following three properties in every
execution *e*:

- *Closure*: if *e* starts in a legitimate configuration then *e* contains only legitimate configurations;

- *Convergence*: *e* eventually reaches a legitimate configuration; and

- *Specification*: if *e* starts in a legitimate configuration then *e* satisfies the intended specification w.r.t. *SPEC*.

An algorithm is said to be silent when each of its executions eventually reaches a terminal configuration; in such a case, the set of legitimate configurations can be chosen as the set of terminal configurations. The closure, convergence, and silent properties are expressed using Linear Time Logic operators provided in the PADEC library.

The BFS Algorithm in PADEC

For the *BFS* Algorithm and its specification, we use the formal encoding provided in [4]; in particular, the algorithm is a straightforward faithful translation in Coq/Rocq of Algorithm 1. Notably, an element of *States*, namely a state of a given node, is a tuple (*d*, *par*, *root*, *neighbors*) representing the variables of the node as in Algorithm 1.

<footnote n="1">¹ Note that PADEC is restricted to deterministic local algorithms.</footnote>

<footnote n="2">² Coinduction allows to define and reason about potentially infinite objects.</footnote>
As the constant variables *root* and *neighbors* represent the network, the assumptions that this network is static, rooted, bidirected and connected is encoded in a predicate on a configuration using only those variables. This predicate, in particular uses the set of edges of the network *Edges* $\stackrel{def}{=}$ $\{(p, q) | p, q \in \text{Nodes} \wedge (p \in q.\text{neighbors} \lor q \in p.\text{neighbors})\}$. Globally in this predicate, the neighbor links represent a bidirected connected graph and the Boolean *root* should be true for a unique node. We will assume moreover that this predicate holds for any configuration, even if this is no more mentioned in the sequel.

In [4], the *BFS* Algorithm was proven using PADEC to be self-stabilizing and silent for the specification *SPEC* of a BFS spanning tree, under the assumption of a weakly fair daemon. We extend here this result to the *unfair daemon*. Note that, the properties of closure and specification hold regardless the type of the daemon. The property of convergence is however lost when relaxing the assumption from a weakly fair to an unfair daemon. The rest of the paper therefore focuses on proving the convergence of the *BFS* Algorithm under an unfair daemon in PADEC, i.e., providing a constructive proof under the form of a potential function and its corresponding order.

# 4 Overview of the Proof

An execution is fully defined by the *Step* relation, as the *unfair daemon* does not add any other restriction. As a consequence, the convergence property can be expressed by the fact that the *Step* relation is well-founded:

$$ \text{WellFounded Step} \qquad (1) $$

This means that any execution $e \stackrel{def}{=} \gamma_0 \xrightarrow{\text{Step}} \gamma_1 \xrightarrow{\text{Step}} \dots$ is finite. WellFounded comes from the Coq/Rocq standard library where it is expressed as

$$ (\text{WellFounded } R) \stackrel{def}{=} (\forall x. \text{Acc } R x) $$

for a given relation *R*. *Acc* is an inductive predicate from the Coq/Rocq standard library as well, and (*Acc* *R* *x*) means that every sequence of elements starting from *x* and linked by *R* is finite.

In the following, we will prove the assertion (1). To this end, we will consider the partitioning of the *Step* relation as $\text{Step}^{(r)} \cup \text{Step}^{(d)} \cup \text{Step}^{(p)}$ denoting respectively *root steps*, *d-steps* and *par-steps* defined as follows:

- $\text{Step}^{(r)}$ holds for any step $\gamma \xrightarrow{\text{Step}} \gamma'$ in which the root executes i.e., such that $\gamma.r.d \neq \gamma'.r.d$. Note that any subset of non-root nodes may also execute during this step.

- $\text{Step}^{(d)}$ holds for any step $\gamma \xrightarrow{\text{Step}} \gamma'$ in which the root does not execute and at least one non-root node executes a *CD*-action i.e., $\gamma.r.d = \gamma'.r.d$ and $\exists p. \gamma.p.d \neq \gamma'.p.d$. Note that any subset of non-root nodes may also execute either *Action CD* or *CP*.
- Step<sup>(p)</sup> holds for any step $\gamma \xrightarrow{\text{Step}} \gamma'$ where d variables are left unchanged i.e., $\forall p. \gamma.p.d = \gamma'.p.d$. This implies that a node which executes is not the root and executes its CP-action.

In addition, we will use the following general result, (developed as a tool in PADEC), which gives sufficient conditions ensuring the union of two relations is well-founded. This tool has first been developed in PADEC for algorithms with prioritized rules (as Actions CD and CP) and has been enhanced for this proof.

**Proposition 1.** Let $R_1, R_2$ be relations, $x$ an element. Assume that (1) $R_2$ is well-founded and (2) there exist a set $B_1$ and relations $R'_1$ well-founded, $E_1$ transitive such that

(2.i) $x \in B_1$ and for all elements $a, b$ if $a \in B_1$ and $a \xrightarrow{R_1 \cup R_2} b$ then $b \in B_1$,

(2.ii) for all elements $a, b$ if $a \in B_1$ and $a \xrightarrow{R_1} b$ then $a \xrightarrow{R'_1} b$,

(2.iii) for all elements $a, b, c$, if $a \xrightarrow{R'_1} b$ and $b \xrightarrow{E_1} c$ then $a \xrightarrow{R'_1} c$,

(2.iv) for all elements $a, b$ if $a \xrightarrow{R_2} b$ then $a \xrightarrow{E_1} b$.

We can conclude that $(\mathbf{Acc}(R_1 \cup R_2)x)$ holds.

*Proof.* Intuitively, the set $B_1$ represents an over-approximation of the elements reachable from $x$ through $R_1 \cup R_2$ (2.i). The relation $R'_1$ represents an abstraction of the relation $R_1$ when restricted to the set $B_1$ (2.ii). The relation $E_1$ can be understood as an equality with respect to $R'_1$ (2.iii) which moreover abstracts the relation $R_2$ (2.iv). Usually, $R'_1$ and $E_1$ can be derived from a potential function on the set of elements and its induced partial order and equality.

The result is then directly obtained by considering the relation $<_{lex}$ defined on pairs of elements by

$$ (a, b) <_{lex} (c, d) \stackrel{\text{def}}{=} a \xrightarrow{R'_1} c \text{ or } (a \xrightarrow{E_1} c \text{ and } b \xrightarrow{R_2} d) $$

and the key observations that:

- $<_{lex}$ is a well-founded lexicographic order since $R'_1$ and $R_2$ are well-founded;

- for all elements $a, b$, if $a \in B_1$ and $a \xrightarrow{R_1 \cup R_2} b$ then $(a, a) <_{lex} (b, b)$. $\square$

As a corollary, using the same notations as in Proposition 1, being given two relations $R_1$ and $R_2$, if for every $x$ we can effectively construct the set $B_1$ and the relations $R'_1$, $E_1$ such that all assumptions are met (1, 2.i to 2.iv), then we can conclude that $R_1 \cup R_2$ is well-founded.

We now proceed to the core of the convergence proof and show progressively that Step<sup>(p)</sup>, Step<sup>(d)</sup> ∪ Step<sup>(p)</sup> and Step<sup>(r)</sup> ∪ Step<sup>(d)</sup> ∪ Step<sup>(p)</sup> are well-founded.

**Lemma 1.** WellFounded Step<sup>(p)</sup>.
*Proof.* We use the potential function denoted $\#CP(\gamma)$ which counts for a given configuration $\gamma$ the number of nodes for which the guard of their CP-action is enabled. We say that such a node is CP-enabled, otherwise it is CP-disabled.

Considering par-steps only i.e., the values of d-variables are left unchanged then either (i) a node is CP-disabled and will remain so or (ii) it is CP-enabled and if it executes, it becomes CP-disabled, otherwise it remains CP-enabled.

Hence, for every two configurations $\gamma$ and $\gamma'$ such that $\gamma \xrightarrow{Step^{(p)}} \gamma'$ we have $\#CP(\gamma') < \#CP(\gamma)$, namely $\#CP$ is decreasing. As $\#CP$ is obviously lower-bounded by 0, this ensures that $Step^{(p)}$ is well-founded. $\square$

To proceed on the next phase of the convergence proof, we will use a result about executions consisting of d-steps only. The next proposition guarantees the well-foundedness of the relation $Step^{(d)}$ through the existence of an effectively constructive potential function and its ordering:

**Proposition 2.** Given a configuration $\gamma_0$, we can effectively construct:

(a) a set of configurations $B(\gamma_0)$ containing $\gamma_0$ and closed by taking d- or par-steps,

(b) a potential function on configurations from $\Gamma$ to a domain $D(\gamma_0)$, $\pi_{\gamma_0}: \Gamma \to D(\gamma_0)$, independent of par-variables, and

(c) a well-founded order $\prec_d$ on $D(\gamma_0)$, such that for all $\gamma \in B(\gamma_0)$ and $\gamma \xrightarrow{Step^{(d)}} \gamma'$, it holds that $\pi_{\gamma_0}(\gamma') \prec_d \pi_{\gamma_0}(\gamma)$.

The technical details and the proof of Proposition 2 are presented in Section 5.

**Lemma 2.** WellFounded ($Step^{(d)} \cup Step^{(p)}$).

*Proof.* We must prove $(\text{Acc} (Step^{(d)} \cup Step^{(p)}) \gamma_0)$ for an arbitrary configuration $\gamma_0$. Therefore, we use Proposition 1 by taking $R_1 \stackrel{def}{=} Step^{(d)}$, $R_2 \stackrel{def}{=} Step^{(p)}$ and $x \stackrel{def}{=} \gamma_0$. First, Lemma 1 ensures that $R_2$ is well-founded. Using the Proposition 2 above, we define the set $B_1$, and the relations $R'_1$ and $E_1$ as follows:

$$ 
\begin{align*}
B_1 \stackrel{def}{=} B(\gamma_0) \\
\gamma \xrightarrow{R'_1} \gamma' \stackrel{def}{=} \pi_{\gamma_0}(\gamma') \prec_d \pi_{\gamma_0}(\gamma) \\
\gamma \xrightarrow{E_1} \gamma' \stackrel{def}{=} \pi_{\gamma_0}(\gamma') = \pi_{\gamma_0}(\gamma)
\end{align*}
$$

The guarantees of Proposition 2 allow to fulfill the assumptions of Proposition 1. Indeed, the relation $R'_1$ is well-founded, see Proposition 2(c). The relation $E_1$ is transitive by its definition (based on equality of potentials). The assumption (2.i), that is, $B_1$ contains $x$ and is closed by $R_1$ or $R_2$ steps follows from Proposition 2(a). Assumption (2.ii), that is, $R'_1$ is an abstraction of $Step^{(d)}$ on the set $B_1$ holds because of Proposition 2(c). Assumption (2.iii) holds trivially by the construction of $R'_1$ and $E_1$. Last, assumption (2.iv) holds as the potential function $\pi_{\gamma_0}$ is not depending on the par variables, that is, remains insensitive to par-steps. This proves $(\text{Acc} (Step^{(d)} \cup Step^{(p)}) \gamma_0)$ and finally, as the choice of $\gamma_0$ was arbitrary, we prove that WellFounded ($Step^{(d)} \cup Step^{(p)}$). $\square$
It remains to take into account the root steps from Step(\(r\)). Recall that the root **r** can execute at most once in any execution: either its *d*-variable is 0 from the beginning and **r** never executes; or it is positive and then **r** is enabled. If it executes, the variable is set to 0 and **r** is then disabled forever. The fact that Step(\(r\)) is well-founded is therefore trivial to obtain.

**Theorem 1.** WellFounded (Step(\(r\)) ∪ Step(\(d\)) ∪ Step(\(p\))).

*Proof.* We use Proposition 1 by taking $R_1 \stackrel{\text{def}}{=} \text{Step}^{(r)}$, $R_2 \stackrel{\text{def}}{=} \text{Step}^{(d)} \cup \text{Step}^{(p)}$, and an arbitrary configuration $\gamma_0$. First, Lemma 2 ensures that $R_2$ is well-founded. Second, we define the set $B_1 \stackrel{\text{def}}{=} \Gamma$ and the relations $R'_1$ and $E_1$ as follows:

$$ \gamma \xrightarrow{R'_1} \gamma' \stackrel{\text{def}}{=} \gamma'.\mathbf{r}.d < \gamma.\mathbf{r}.d $$

$$ \gamma \xrightarrow{E_1} \gamma' \stackrel{\text{def}}{=} \gamma'.\mathbf{r}.d = \gamma.\mathbf{r}.d $$

Obviously, $R'_1$ is well-founded as observed above, and $E_1$ is transitive by definition. Since $B_1$ contains all configurations, the assumption (2.i) is trivially satisfied. Also, $R_1 \subseteq R'_1$ holds by definition of $R'_1$, hence, it implies assumption (2.ii). Assumption (2.iii) follows from definitions as well and assumption (2.iv) holds because $\gamma.\mathbf{r}.d$ is not changing for any non-root step. □

# 5 A Decreasing Potential Function for d-steps

This section is concerned with the proof of Proposition 2 stated in Section 4. To this end, we proceed in three steps. First, we establish a finite over-approximation on the set of the *d* values that could be possibly reached in an execution involving *d*-steps only from some initial configuration $\gamma_0$. Second, we introduce a partitioning of edges and prove some preservation properties on this partitioning along *d*-steps. Third, we combine the above results to effectively construct a potential function for *d*-steps and a well-founded order on the co-domain of this function, ultimately proving Proposition 2.

For the sake of readability, we denote *d*-steps $\gamma \xrightarrow{\text{Step}^{(d)}} \gamma'$ shortly by $\gamma \to_d \gamma'$.

## 5.1 Bounds on Distance Values

For a configuration $\gamma$, we define the non-negative integers $\text{max}_d \gamma \stackrel{\text{def}}{=} \max\{\gamma.q.d \mid q \in \text{Nodes}\}$, $\text{min}_d \gamma \stackrel{\text{def}}{=} \min\{\gamma.q.d \mid q \in \text{Nodes}\}$, $\text{sum}_d \gamma \stackrel{\text{def}}{=} \sum\{\gamma.q.d \mid q \in \text{Nodes}\}$.<fnref n="3" /> We also define $\gamma^\perp$, $\gamma^\top$ respectively a *bottom* and a *top* configuration associated to $\gamma$. These are identical to $\gamma$ except for *d* values, defined for every node *p* as follows:

$$ \begin{array}{l} \gamma^{\perp}.p.d \stackrel{\text{def}}{=} \min_d \gamma \\ \gamma^{\top}.p.d \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \gamma.p.d \qquad \text{if } p=r \\ \max\{\gamma.p.d, 1 + \min\{\gamma^{\top}.q.d \mid (p,q) \in \text{Edges}, \text{dist}(p, \mathbf{r}) = 1 + \text{dist}(q, \mathbf{r})\}\} \text{ otherwise,} \end{array} \right. \end{array} $$

<footnote n="3">³ The sum is taken on the multiset of *d* values</footnote>
where $\text{dist}(q, r)$ represents the distance of some node $q$ to the root $r$. Note that the recursive definition of $\gamma^\top.p.d$ is well-defined as the recursion is limited to neighbors $q$ of $p$ located at a smaller distance to the root $r$ than $p$. Intuitively, the maximal $d$ value of a non-root node $p$ in some configuration reachable from $\gamma$ is either its value in $\gamma$ (i.e., it can be the case when $p$ does not execute) or 1 plus the minimum of the maximal $d$ values of its neighbors $q$ closer to the root (see Action CD when $p$ executes). We define the partial order $\le_d$ on configurations by taking

$$ \gamma_1 \le_d \gamma_2 \stackrel{\text{def}}{=} \forall q \in \text{Nodes} : \gamma_1.q.d \le \gamma_2.q.d $$

The next lemma states basic properties of the $(.)^\perp$, $(.)^\top$ operators, namely their idempotence and their monotonicity with respect to $\le_d$. The proof follows from definitions and uses induction on nodes according to their distance to the root.

**Lemma 3.** For all configurations $\gamma, \gamma_1, \gamma_2$:

$$ (i) \quad \gamma^\perp \le_d \gamma \le_d \gamma^\top, (\gamma^\perp)^\top = \gamma^\perp, (\gamma^\top)^\top = \gamma^\top, $$

$$ (ii) \quad \text{if } \gamma_1 \le_d \gamma_2 \text{ then } \gamma_1^\perp \le_d \gamma_2^\perp, \gamma_1^\top \le_d \gamma_2^\top. $$

The next lemma relates the bottom and top configurations to $d$-steps. The proof is done by induction respectively, on the set of nodes according to their distance to the root (i) and on the length of an execution sequence from $\gamma_0$ (ii).$^4$

**Lemma 4.** For all configurations $\gamma, \gamma', \gamma_0$:

$$ (i) \quad \text{if } \gamma \to_d \gamma' \text{ then } \gamma^\perp \le_d \gamma'^\perp, \gamma'^\top \le_d \gamma'^\top, $$

$$ (ii) \quad \text{if } \gamma_0 \to_d^* \gamma \text{ then } \gamma_0^\perp \le_d \gamma \le_d \gamma_0^\top. $$

## 5.2 Smooth and Non-smooth $d$-steps

We say that an edge $(p, q) \in \text{Edges}$ is smooth (resp. non-smooth) in a configuration $\gamma \in \Gamma$ if the difference (in absolute value, $\text{abs}$) between the $d$-values at its endpoints $p, q$ is at most 1 (resp. at least 2). Formally, consider the predicate

$$ \text{smooth}_\gamma((p, q)) \stackrel{\text{def}}{=} (\text{abs}(\gamma.p.d - \gamma.q.d) \le 1). $$

We say that a $d$-step $\gamma \to_d \gamma'$ is smooth if all the nodes $p$ changing their values from $\gamma$ to $\gamma'$ are connected to smooth edges only in $\gamma$, formally:

$$ \text{smooth}(\gamma \to_d \gamma') \stackrel{\text{def}}{=} \forall p \in \text{Nodes} : (\gamma'.p.d \neq \gamma.p.d) \Rightarrow (\forall q \in p.\text{neighbors} : \text{smooth}_\gamma((p, q))) $$

We define the rank of an edge $(p, q) \in \text{Edges}$ in a configuration $\gamma \in \Gamma$ as $\text{rank}_\gamma((p, q)) \stackrel{\text{def}}{=} \min(\gamma.p.d, \gamma.q.d)$.

For illustration, consider the three configurations $\gamma_1, \gamma_2, \gamma_3$ depicted in Fig. 1. We represented the $d$ values of the nodes by their positioning on the horizontal

<footnote>$^4$ $\gamma_0 \to_d^* \gamma$ means that $\gamma$ is reachable from $\gamma_0$ using a finite number of $d$-steps.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. Smooth and non-smooth steps</figcaption></figure>

lines e.g., $\gamma_1 \cdot r \cdot d = 10$, $\gamma_1 \cdot p_1 \cdot d = 9$, $\gamma_2 \cdot p_1 \cdot d = 10$, etc. Edges are represented by lines connecting nodes: smooth (resp. non-smooth) edges are depicted in blue (resp. red). Configuration $\gamma_2$ is the successor of $\gamma_1$ by a smooth step. That is, only $p_1$ and $p_6$ have been executed and these nodes were connected only to smooth (blue) edges in $\gamma_1$. Configuration $\gamma_3$ is the successor of $\gamma_2$ by a non-smooth step. That is, $p_3$ and $p_4$ have been executed along the step, and these nodes were connected to some non-smooth edges.

The next lemmas provide key properties for understanding the execution of $d$-steps, depending if they are smooth or not. Lemma 5 basically states that partitioning between smooth and non-smooth, as well as the rank of every non-smooth edge is preserved by smooth steps. In addition, the total sum of $d$ values is increasing along such a step.

**Lemma 5.** Consider a smooth $d$-step $\gamma \to_d \gamma'$. Then,

(i) $\forall e \in \text{Edges} : \neg \text{smooth}_{\gamma}(e) \Leftrightarrow \neg \text{smooth}_{\gamma'}(e),$

(ii) $\forall e \in \text{Edges} : \neg \text{smooth}_{\gamma}(e) \Rightarrow (\text{rank}_{\gamma}(e) = \text{rank}_{\gamma'}(e)),$

(iii) $\text{sum}_d \gamma' > \text{sum}_d \gamma.$

*Proof.* The proof follows immediately from the definition of smooth steps and/or edges. First, the fact that non-smooth edges are preserved along with their rank in a smooth $d$-step directly comes from the definition of a smooth step: since no node connected to a non-smooth edge can execute, non-smooth edges remain unchanged. Second, we obtain the increasing of the sum of all $d$-values by observing that when a node executes in a smooth $d$-step, its $d$ value increases by one or two (due to its neighbors which are either above by one or at the same level of $d$ value). As a smooth $d$-step involves at least one such executing node, $\text{sum}_d$ necessarily increases (since nodes that do not increase $d$ leave it unchanged). $\square$

For illustration, consider the smooth step depicted in Fig. 1, i.e., between $\gamma_1$ and $\gamma_2$. It is rather trivial that, as long as the nodes executing were connected to
smooth edges only (in blue), their execution has no impact on the non-smooth edges i.e., they remain non-smooth and preserve their rank. Yet, the overall sum of the d values increases, here because at least the values of the two moving nodes have increased (by 1 for $p_1$ and by 2 for $p_6$).

Lemma 6 provides a similar preservation result for non-smooth steps. In this case, the key property is that one can effectively compute a bound $k^*$ such that (i) all non-smooth edges with rank lower than $k^*$ remain non-smooth and preserve their rank and (ii) the set of non-smooth edges with rank $k^*$ is strictly decreasing along the step. The lemma provides both the explicit definition of $k^*$ as well as the identification of a non-smooth edge at level $k^*$ which either becomes smooth or gets a reduced rank after the step, that is, some edge $(p, q)$ for which the minimum is achieved in the definition of $k^*$.

**Lemma 6.** Consider a non-smooth d-step $\gamma \to_d \gamma'$. Let

$$k^* \stackrel{\text{def}}{=} \min\{\text{rank}_\gamma((p,q)) \mid (p,q) \in \text{Edges} : \neg \text{smooth}_\gamma((p,q)), \\ \gamma'.p.d \neq \gamma.p.d \text{ or } \gamma'.q.d \neq \gamma.q.d\}$$

Then,

$$(i) \forall e \in \text{Edges} : (\text{rank}_{\gamma'}(e) \le k^* \wedge \neg \text{smooth}_{\gamma'}(e)) \Rightarrow (\text{rank}_{\gamma}(e) = \text{rank}_{\gamma'}(e) \wedge \neg \text{smooth}_{\gamma}(e)),$$

$$(ii) \forall e \in \text{Edges} : (\text{rank}_{\gamma}(e) < k^* \wedge \neg \text{smooth}_{\gamma}(e)) \Rightarrow (\text{rank}_{\gamma'}(e) = \text{rank}_{\gamma}(e) \wedge \neg \text{smooth}_{\gamma'}(e)),$$

$$(iii) \exists e \in \text{Edges} : (\text{rank}_{\gamma}(e) = k^* \wedge \neg \text{smooth}_{\gamma}(e)) \wedge (\neg \text{smooth}_{\gamma'}(e) \Rightarrow \text{rank}_{\gamma'}(e) > \text{rank}_{\gamma}(e)).$$

*Proof.* (i) The proof is done by case splitting, considering which endpoints of non-smooth edges e execute. In fact, the only feasible case is when none of them executes. In all other cases, by choosing the node which gives a new value to its d variable, we obtain a contradiction, either with the minimality of $k^*$ or with the non-smoothness of e in $\gamma'$.

(ii) By definition of $k^*$, no node involved in a non-smooth edge can execute if the rank is below $k^*$, hence rank and non-smoothness are left unchanged.

(iii) Note here that, using Coq/Rocq, to be able to prove “$\exists e \in \text{Edges} : ...$”, we have to effectively construct such an edge. In our case, it is chosen as one of the edges that achieves the minimum rank value when computing $k^*$: a non-smooth edge $e^*$ such that $\text{rank}_\gamma(e^*) = k^*$, and one of its end nodes executes during the step (such an edge can be computed using the computation of the minimum value over a finite set). Now, consider the case where $e^*$ remains non-smooth in $\gamma'$. We note $e^* = (p, q)$ with $\text{rank}_\gamma((p, q)) = \gamma.p.d$. We can prove that if $p$ executes then $\gamma'.p.d > \gamma.p.d$ and that if $q$ executes then $\gamma'.q.d = \gamma.p.d + 1$ (see Fig. 2 for an illustration). In any case, we obtain $\text{rank}_{\gamma'}(e) > \text{rank}_\gamma(e)$ and the result is then easy to conclude. □

For illustration also, consider the non-smooth step depicted in Fig. 1 between $\gamma_2$ and $\gamma_3$. In this case, the bound value is $k^* = 8$. The lemma ensures that the
We are now ready to complete the proof of Proposition 2, restated hereafter for the sake of readability.

**Proposition 2.** Given a configuration $\gamma_0$, we can effectively construct:

(a) a set of configurations $B(\gamma_0)$ containing $\gamma_0$ and closed by taking d- or par-steps,

(b) a potential function on configurations from $\Gamma$ to a domain $D(\gamma_0)$, $\pi_{\gamma_0} : \Gamma \to D(\gamma_0)$, independent on par-variables, and

(c) a well-founded order $\prec_d$ on $D(\gamma_0)$, such that for all $\gamma \in B(\gamma_0)$ and $\gamma \xrightarrow{\text{Step}^{(d)}} \gamma'$, it holds that $\pi_{\gamma_0}(\gamma') \prec_d \pi_{\gamma_0}(\gamma)$.

*Proof.* (a) We define $B(\gamma_0) \stackrel{\text{def}}{=} \{\gamma \mid \gamma_0^{\perp} \le_d \gamma \le_d \gamma_0^{\top}\}$. From Lemma 3(i) we obtain immediately $\gamma_0 \in B(\gamma_0)$. The set $B(\gamma_0)$ is obviously closed by taking par-steps, as these steps do no change the values of d-variables. The closure of $B(\gamma_0)$ by d-steps can be understood by the $\le_d$ inequalities depicted below:

$$ \begin{array}{ccccccc} \gamma_0^{\perp} & \le_d & \gamma^{\perp} & \le_d & \gamma & \le_d & \gamma_0^{\top} \\ |\Lambda| & & |\Lambda| & & |\Lambda| & & |\Lambda| \\ \gamma'^{\perp} & \le_d & \gamma' & \le_d & \gamma' & \le_d & \gamma'^{\top} \end{array} $$

Knowing $\gamma \in B(\gamma_0)$, that is, $\gamma_0^{\perp} \le_d \gamma \le_d \gamma_0^{\top}$ we obtain the inequalities from the top line by using the idempotence and monotonicity of $(.)^{\perp}$, $(.)^{\top}$ with respect to $\le_d$ (Lemma 3). The same lemma ensures the inequalities of the bottom line. Finally, the inequalities across the two lines hold because of Lemma 4. All over, they ensure that $\gamma_0^{\perp} \le_d \gamma' \le_d \gamma_0^{\top}$ for any d-step $\gamma \to_d \gamma'$.

(b) We define the interval of non-negative integers $K_0 \stackrel{\text{def}}{=} [\min_d \gamma_0^{\perp}, \max_d \gamma_0^{\top}]$, that is, the interval of possible d-values in the configurations reachable from $\gamma_0$. We define the domain $D(\gamma_0) \stackrel{\text{def}}{=} (2^{\text{Edges}})^{K_0} \times [\text{sum}_d \gamma_0^{\perp}, \text{sum}_d \gamma_0^{\top}]$. That is, $D(\gamma_0)$ consists of pairs $(\mathcal{E}, s)$ where $\mathcal{E} : K_0 \to 2^{\text{Edges}}$ is a $K_0$-indexed sequence of sets of edges and $s$ is a bounded non-negative integer. In particular, note that $D(\gamma_0)$ is finite. We define the potential function $\pi_{\gamma_0} : \Gamma \to D(\gamma_0)$ by taking $\pi_{\gamma_0}(\gamma) \stackrel{\text{def}}{=} ((E_{\gamma,k})_{k \in K_0}, \text{sum}_d \gamma)$. Remark that $\pi_{\gamma_0}$ is not dependent on par variables in $\gamma$.

(c) We define the relation $\prec_d$ on $D(\gamma_0)$ by taking $(\mathcal{E}_1, s_1) \prec_d (\mathcal{E}_2, s_2) \stackrel{\text{def}}{=} \mathcal{E}_1 \prec_{\text{setlex}} \mathcal{E}_2 \lor (\mathcal{E}_1 = \mathcal{E}_2 \land s_2 < s_1)$. That is, $\prec_d$ is actually a strict lexicographic order on pairs $(\mathcal{E}, s)$ which combines the well-founded order $\prec_{\text{setlex}}$ on finite sequences of finite sets and a well-founded order $<$ on bounded integers. It remains to prove that

$$ \forall \gamma, \gamma' \in \Gamma, \gamma \in B(\gamma_0) \text{ and } \gamma \to_d \gamma' \Rightarrow \pi_{\gamma_0}(\gamma') \prec_d \pi_{\gamma_0}(\gamma) $$

Let respectively $(\mathcal{E}, s) \stackrel{\text{def}}{=} \pi_{\gamma_0}(\gamma)$, $(\mathcal{E}', s') \stackrel{\text{def}}{=} \pi_{\gamma_0}(\gamma')$. Note that from $\gamma \in B(\gamma_0)$ and the previous point (a) we obtain that $\gamma' \in B(\gamma_0)$ as well. In particular, this ensures the ranks of non-smooth edges of $\gamma, \gamma'$ are contained in $K_0$ and
respectively $s, s'$ are contained in the interval $[\text{sum}_d \gamma_0^\perp, \text{sum}_d \gamma_0^\top]$. Lemma 7 and Lemma 5(iii) provide the conditions ensuring that $\pi_{\gamma_0}$ is indeed a decreasing potential function with respect to $\prec_d$ as expected. For non-smooth steps, we observe the strict inequality $\mathcal{E}' \prec_{\text{setlex}} \mathcal{E}$. For smooth $d$-steps we observe the equality $\mathcal{E} = \mathcal{E}'$ and the strict inequality $s < s'$. $\square$

# 6 Conclusion

In this paper, we provide the first constructive proof for the convergence of the Dolev et al. BFS spanning tree algorithm under the most general execution assumptions (i.e., unfair daemon, unbounded variables). The convergence proof has been fully formalized and automatically checked using the PADEC framework. Contrarily to many papers about formal certified proofs of distributed algorithms, we do not formalize and validate an existing proof. Rather, due to the constructive aspect of the proofs allowed in Coq/Rocq, we had to develop a new proof: we have defined a novel potential function, allowing a finer comprehension of the system executions towards terminal configurations. We believe that, even though the algorithm time complexity is exponential, this potential function will open the door to a tighter complexity analysis.

# References

1. Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. Log. Methods Comput. Sci. 13(4) (2017)

2. Altisen, K., Corbineau, P., Devismes, S.: Squeezing streams and composition of self-stabilizing algorithms. In: FORTE. Lecture Notes in Computer Science, vol. 11535, pp. 21–38. Springer (2019)

3. Altisen, K., Corbineau, P., Devismes, S.: Certification of an exact worst-case self-stabilization time. In: ICDCN. pp. 46–55. ACM (2021)

4. Altisen, K., Corbineau, P., Devismes, S.: Certified round complexity of self-stabilizing algorithms. In: DISC. LIPIcs, vol. 281, pp. 2:1–2:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

5. Altisen, K., Devismes, S., Dubois, S., Petit, F.: Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2019)

6. Auger, C., Bouzid, Z., Courtieu, P., Tixeuil, S., Urbain, X.: Certified impossibility results for byzantine-tolerant mobile robots. In: SSS. Lecture Notes in Computer Science, vol. 8255, pp. 178–190. Springer (2013)

7. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004)

8. Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. Int. J. Softw. Tools Technol. Transf. 23(5), 797–821 (2021)

9. Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015)
10. Castéran, P., Filou, V.: Tasks, types and tactics for local computation systems. Stud. Inform. Univ. 9(1), 39–86 (2011)

11. Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: SSS. Lecture Notes in Computer Science, vol. 6976, pp. 120–134. Springer (2011)

12. Charron-Bost, B., Merz, S.: Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Software and Informatics 3(2-3), 273–303 (2009)

13. Courtieu, P.: Proving self-stabilization with a proof assistant. In: IPDPS. IEEE Computer Society (2002)

14. Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115(3), 447–452 (2015)

15. Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: FM. Lecture Notes in Computer Science, vol. 7436, pp. 147–154. Springer (2012)

16. Delporte-Gallet, C., Fauconnier, H., Gafni, E., Lamport, L.: Adaptive register allocation with a linear number of registers. In: DISC. Lecture Notes in Computer Science, vol. 8205, pp. 269–283. Springer (2013)

17. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)

18. Dolev, S., Israeli, A., Moran, S.: Self-stabilization of dynamic systems assuming only Read/Write atomicity. Distributed Computing 7(1), 3–16 (1993)

19. Ebnenasir, A.: Synthesizing self-stabilizing parameterized protocols with unbounded variables. In: FMCAD. pp. 245–254. IEEE (2022)

20. Hesselink, W.H.: Mechanical verification of Lamport’s Bakery algorithm. Science of Computer Programming 78(9), 1622–1638 (2013)

21. Jaskelioff, M., Merz, S.: Proving the Correctness of Disk Paxos. Archive of Formal Proofs 2005 (2005)

22. Küfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms - from pseudo code to checked proofs. In: IFIP TCS. Lecture Notes in Computer Science, vol. 7604, pp. 209–224. Springer (2012)

23. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2002)

24. Lamport, L.: How to write a 21st century proof. Journal of Fixed Point Theory and Applications 11(1), 43–63 (2012)

25. Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148, 26–48 (2017)

26. Rahli, V., Vukotic, I., Völp, M., Veríssimo, P.J.E.: Velisarios: Byzantine fault-tolerant protocols powered by coq. In: ESOP. Lecture Notes in Computer Science, vol. 10801, pp. 619–650. Springer (2018)

27. Rocq Team: The Rocq Prover (January 2025), https://rocq-prover.org/

28. Tsuchiya, T., Nagano, S., Paidi, R.B., Kikuno, T.: Symbolic model checking for self-stabilizing algorithms. IEEE TPDS 12(1), 81–95 (2001)

29. Volk, M., Bonakdarpour, B., Katoen, J., Aflaki, S.: Synthesizing optimal bias in randomized self-stabilization. Distributed Comput. 35(1), 37–57 (2022)