# Tutorial: Parameterized Verification with Byzantine Model Checker

Igor Konnov, Marijana Lazić, Ilina Stoilkovska, Josef Widder

► To cite this version:

Igor Konnov, Marijana Lazić, Ilina Stoilkovska, Josef Widder. Tutorial: Parameterized Verification with Byzantine Model Checker. 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2020, Valletta, Malta. pp.189-207, 10.1007/978-3-030-50086-3_11. hal-03283235

HAL Id: hal-03283235

https://inria.hal.science/hal-03283235

Submitted on 9 Jul 2021

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
# Tutorial: Parameterized Verification with Byzantine Model Checker

Igor Konnov¹, Marijana Lazić², Ilina Stoilkovska¹,³, and Josef Widder¹ *

¹ Informal Systems, Vienna, Austria
{igor,ilina,josef}@informal.systems

² TU Munich, Munich, Germany
lazic@in.tum.de

³ TU Wien, Vienna, Austria

**Abstract.** Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems of distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as Tendermint consensus. In this tutorial, we give an overview of the techniques implemented in Byzantine Model Checker (ByMC). ByMC implements several techniques for automatic verification of threshold-guarded distributed algorithms. These algorithms have the following features: (1) up to *t* of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least *t* + 1; (3) the number *n* of processes in the system is a parameter, as well as *t*; (4) and the parameters are restricted by a resilience condition, e.g., *n* > 3*t*. Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.

## 1 Introduction

The recent advent of blockchain technologies [68,30,2,20,82,23] has brought fault-tolerant distributed algorithms to the spotlight of computer science and software engineering. In particular, due to the huge amount of funds managed by blockchains, it is crucial that their software is free of bugs. At the same time, these systems are characterized by a large number of participants. Thus, automated verification methods face the well-known state space explosion problem. Furthermore, the well-known undecidability results for the verification of parameterized systems [4,80,37,38,15] apply in this setting. One way to circumvent

<footnote>* Supported by Interchain Foundation (Switzerland) and by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS). Partially supported by the Austrian Science Fund (FWF) via the Doctoral College LogiCS W1255.</footnote>
these problems is to develop domain specific methods that work for a specific subclass of systems.

In this tutorial, we consider verification techniques for fault-tolerant distributed algorithms. As an example, consider a blockchain system, where a blockchain algorithm ensures coordination of the processes participating in the system. We observe that to do so, the processes need to solve a coordination problem called *atomic (or, total order) broadcast* [43], that is, every process delivers the same transactions in the same order. To achieve that, we typically need a *resilience condition* that restricts the fraction of processes that may be faulty [70]. The techniques we survey in this tutorial deal with the concepts of broadcast and atomic broadcast under resilience conditions.

While Bitcoin [68] was a new approach to consensus, several Blockchain systems like Tendermint [20] and HotStuff [82] are modern implementations that are built on these classic Byzantine fault tolerance concepts. While the techniques we describe here address in part the challenges for the verification of such systems. We discuss open challenges in Section 5.

In addition to practical importance, the reasons for the long-standing interest [61,58,70,39] in distributed systems is that distributed consensus is non-trivial in two aspects:

1. Most coordination problems are impossible to solve without imposing constraints on the environment, e.g., an upper bound on the fraction of faulty processes, assumptions on the behavior of faulty processes, or bounds on message delays and processing speeds (i.e., restricting interleavings) [70,39,33].

2. Designing correct solutions is hard, owing to the huge state and execution space, and the complex interplay of assumptions mentioned in Point 1. Thus, even published protocols may contain bugs, as reported, e.g., by [62,64].

Due to the impossibility of asynchronous fault-tolerant consensus [39], much of the research focuses one what kinds of problems are solvable in asynchronous systems (e.g., some forms of reliable broadcast) or what kinds of systems allow to solve consensus. In Section 2 we will survey some of the most fundamental system assumptions that allow to solve problems in the presence of faults and example algorithms, and in Section 3 we will discuss how these algorithms can be modeled and how they can be automatically verified.

## 2 Threshold-guarded distributed algorithms

In a classic survey, Schneider [73] explains replicated state machines by the following notion of replica coordination that consists of two properties:

**Agreement.** "Every non-faulty state machine replica receives every request."

**Order.** "Every non-faulty state machine replica processes the requests it receives in the same relative order."

In Schneider's approach [73], the specification of *Agreement* can be solved using an algorithm for reliable broadcast [43]. The processes can use a consensus algorithm [35,27,25] to establish the *Order* property. For instance, the atomic broadcast algorithm from [25] contains these two sub-algorithms.
```c
1 int v:=input({0, 1})
2 bool accept:=false
3 while (true) do { // in one synchronous step
4   if (v == 1) then send <ECHO> to all;
5   receive messages from other processes;
6   if received <ECHO> from ≥ t + 1 processes
7     then v:=1;
8   if received <ECHO> from ≥ n − t processes
9     then accept:=true;
10 }
```

<figure><img src="image_2.png" /><figcaption>Fig. 1. Pseudo code of reliable broadcast à la [77] and its threshold automaton.</figcaption></figure>

The simplest canonical system model that allows one to solve consensus is the synchronous one, and we discuss it in Section 2.1. A second elegant way to circumvent the impossibility of [39] is by replacing liveness with almost sure termination, that is, a probabilistic guarantee. We review this approach in Section 2.3. In fact, reliable broadcast can be solved with an asynchronous distributed algorithm. We discuss their characteristics in Section 2.2.

## 2.1 Synchronous algorithms

A classic example of a fault-tolerant distributed algorithm is the broadcasting algorithm by Srikanth & Toueg [76]. The description of its code is given in Figure 1. As is typical for distributed algorithms, the semantics are not visible from the pseudo code. In fact, we use the same pseudo-code to describe its asynchronous variant later in Section 2.2.

The algorithm satisfies the Agreement property mentioned above. In a distributed system comprising reliable servers, which do not fail and do not lose messages, this property is easy to achieve. If a server receives a requests it sends the request to all other servers. As messages are delivered reliably, every request will eventually be received by every server. The problems comes with faults. Srikanth and Toueg studied Byzantine failures, where faulty servers may send messages only to a subset of the servers (or even send conflicting data). Then two servers may receive different requests. The algorithm in Figure 1 addresses this problem, by forwarding message content received from other servers and only accepting a message content when it was received from a quorum of servers. For each message content *m*, one instance of this algorithm is executed. Initially the variable *v* captures whether a process has received *m*, it is 1 if this is the case. Then a process sends ECHO to all. In an implementation, the message would be of the form (*ECHO*,*m*), that is, it would be tagged with ECHO, and carry the content *m* to distinguish different instances running in parallel; also it would suffice to send the message once instead of sending it in each iteration. Then if the second guard in line 6 evaluates to true at a server *p*, then *p* has received *t*+1 ECHO messages, which means that at least one correct process has forwarded
```
best := input_value
for each round 1 through ⌊t/k⌋ + 1 do {
    broadcast best;
    receive values b₁, ..., b_ℓ from others;
    best := min {b₁, ..., b_ℓ};
}
choose best
```

<caption>**Fig. 2.** Pseudo code of FloodMin from [28]</caption>

the message, so it also forwards it. If a server receives $n-t$ ECHO messages, it finally accepts the request stored in $m$ due to line 8. The reason this algorithm works is that the combination of $n-t$, $t+1$, and $n > 3t$ ensures that if one correct processes has $n-t$ ECHO messages, every other correct process will eventually received at least $t+1$ (there are $t+1$ correct processes among any $n-t$ processes) so that every correct process will forward, and since there are at least $n-t$ correct processes, every one will accept. However, this arithmetics over parameters is subtle and error-prone. To this end, our verification techniques focus on threshold expressions and resilience conditions.

In the above discussion, we were imprecise about the code semantics. In this section we consider the synchronous semantics: All correct processes execute the code line-by-line in lock-step. One loop iteration is called one *round*. A message sent by a correct process to a correct process is received within the same round. Then after sending and receiving messages in lock-step, all correct processes continue by evaluating the guards, before they all proceed to the next round. Because this semantics ensures that all processes move together, and all messages are received within the next rounds, no additional fairness needed to ensure liveness. In practice, this approach is often considered slow and expensive, as it has to be implemented with timeouts that are aligned to worst case message delays (which can be very slow in real networks). However, synchronous semantics offers a high-level abstraction that allows one to design algorithms easier.

Figure 2 shows an example of another synchronous algorithm. This algorithm is run by $n$ replicated processes, up to $t$ of which may fail by crashing, that is, by prematurely halting. It solves the $k$-set agreement problem, that is, out of the $n$ initial values each process decides on one value, so that the number of different decision values is at most $k$. By setting $k=1$, we obtain that there can be exactly one decision value, which coincides with the definition of consensus. In contrast to the reliable broadcast above, it runs for a finite number of rounds. The number of loop iterations ⌊$t/k$⌋ + 1 of the FloodMin algorithm has been designed such that it ensures that there is at least one clean round in which at most $k-1$ processes crash. When we consider consensus, this means there is a round in which no process crashes, so that all processes receive the same values $b_1, ..., b_ℓ$. As a result, during that round all processes set best to the same value.
1
bool v := input_value({0, 1});
10
    if received at least t + 1
2
int r := 1;
11
    messages (P,r,w,D) then {
3
    while (true) do
12
        v := w;
4
        send (R,r,v) to all;
13
        if received at least (n + t) / 2
5
        wait for n - t messages (R,r,*);
14
        messages (P,r,w,D)
6
        if received (n + t) / 2 messages (R,r,w)
15
            then decide w;
7
            then send (P,r,w,D) to all;
16
            } else v := random({0, 1});
8
else send (P,r,?) to all;
17
            r := r + 1;
9
        wait for n - t messages (P,r,*);
18
    od

<caption>Fig. 3. Pseudo code of Ben-Or’s algorithm for Byzantine faults</caption>

## 2.2 Asynchronous algorithms

We now discuss the asynchronous semantics of the code in Figure 1: at each time, exactly one processes performs a step. That is, the steps of the processes are interleaved. In the example one may interpret this as one code line being an atomic unit of executions at a process. In the “receive” statement, a process takes some messages out of the incoming message buffer: possibly no message, and not necessarily all messages that are in the buffer. The “send to all” then places one message in the message buffers of all the other processes. Often asynchronous semantics is considered more coarse-grained, e.g., a step consists of receiving, updating the state, and sending one or more messages.

As we do not restrict which messages are taken out of the buffer during a step, we cannot bound the time needed for message transmission. Moreover, we do not restrict the order, in which processes have to take steps, so we cannot bound the time between two steps of a single process. Typically, we are interested in verifying safety (nothing bad ever happens) under these conditions.

However, for liveness this is problematic. We need messages to be delivered eventually, and correct processes to take steps from time to time. So liveness is typically preconditioned by fairness guarantees: every correct processes takes infinitely many steps and every message sent from a correct process to a correct process is eventually received. For broadcast these constraints are sufficient, while for consensus they are not.

## 2.3 Randomized algorithms

A prominent example is Ben-Or's fault-tolerant binary consensus [7] algorithm in Figure 3. It circumvents the impossibility of asynchronous consensus [39] by relaxing the termination requirement to almost-sure termination, i.e., termination with probability 1. Here processes execute an infinite sequence of asynchronous rounds. While the algorithm is executed under asynchronous semantics, the processes have a local variable *r* that stores the round number. Processes tag messages that they send in round *r* with the round number. Observe that the algorithm only operates on messages from the current round (the guards only count messages tagged with *r*). Asynchronous algorithms with this feature are
called communication closed [36,29]. Each round consists of two stages where the processes first exchange messages tagged with $R$, wait until the number of received messages reaches a certain threshold (the expression over parameters in line 5) and then exchange messages tagged with $P$. As in the previous examples, $n$ is the number of processes, among which at most $t$ may crash or be Byzantine. The thresholds $n-t$, $(n+t)/2$ and $t+1$ in combination with the resilience condition $n > 5t$ ensure that no two correct processes ever decide on different values. If there is no “strong majority” for a value in line 13, a process chooses a new value by tossing a coin in line 16.

# 3 Parameterized verification

## 3.1 Synchronous algorithms

In [78], we introduced the synchronous variant of threshold automata, and studied their applicability and limitations for verification of synchronous fault-tolerant distributed algorithms. We showed that the parameterized reachability problem for synchronous threshold automata is undecidable. Nevertheless, we observed that counter systems of many synchronous fault-tolerant distributed algorithms have bounded diameters, even though the algorithms are parameterized by the number of processes. Hence, bounded model checking can be used for verifying these algorithms. We briefly discuss these results in the following.

*Synchronous Threshold Automata.* In a synchronous algorithm, the processes execute the send, receive, and local computation steps in lock-step. Consider the synchronous reliable broadcast algorithm from [77], whose pseudocode is given in Figure 1 (left). A synchronous threshold automaton (STA) that encodes the pseudocode of this algorithm is given in Figure 1 (right). The STA models the loop body of the pseudo code: one iteration of the loop is expressed as an STA edge that connects the locations before and after a loop iteration.

The semantics of the synchronous threshold automaton is defined in terms of a counter system. For each location $\ell_i \in \{v0, v1, se, ac\}$ (a node in the graph), we have a counter $\kappa_i$ that stores the number of processes located in $\ell_i$. The counter system is parameterized in two ways: (i) in the number of processes $n$, the number of faults $f$, and the upper bound on the number of faults $t$, (ii) the expressions in the guards contain $n$, $t$, and $f$. Every system transition moves all processes simultaneously; potentially using a different rule for each process (depicted by an edge in the figure), provided that the rule guards evaluate to true. The guards compare a sum of counters to a linear combination of parameters. Processes send messages based on their current locations. Hence, we use the number of processes in given locations to test how many messages of a certain type have been sent in the previous round. However, the pseudo code in Figure 1 is predicated by received messages rather than by sent messages. This algorithm is designed to tolerate Byzantine-faulty processes, which may send corrupt messages to some correct processes. Thus, the number of received messages may deviate from the number of correct processes that sent a message. For example,
<table><caption>**Table 1.** A long execution of reliable broadcast and the short representative.</caption><thead><tr><th>Process</th><th>σ<sub>0</sub></th><th>σ<sub>1</sub></th><th>σ<sub>2</sub></th><th>...</th><th>σ<sub>t+1</sub></th><th>σ<sub>t+2</sub></th><th>σ<sub>t+3</sub></th></tr></thead><tbody><tr><td>1</td><td>v1</td><td style="background-color: #f8d7da;">SE</td><td>SE</td><td>...</td><td>SE</td><td>SE</td><td>AC</td></tr><tr><td>2</td><td>v0</td><td>v0</td><td style="background-color: #f8d7da;">SE</td><td>...</td><td>SE</td><td>SE</td><td>AC</td></tr><tr><td>...</td><td></td><td></td><td></td><td>...</td><td></td><td></td><td></td></tr><tr><td>t + 1</td><td>v0</td><td>v0</td><td>v0</td><td>...</td><td style="background-color: #f8d7da;">SE</td><td>SE</td><td>AC</td></tr><tr><td>...</td><td></td><td></td><td></td><td>...</td><td></td><td></td><td></td></tr><tr><td>n - f</td><td>v0</td><td>v0</td><td>v0</td><td>...</td><td>v0</td><td style="background-color: #f8d7da;">SE</td><td>AC</td></tr></tbody></table><table><thead><tr><th>Process</th><th>σ'<sub>0</sub></th><th>σ'<sub>1</sub></th><th>σ'<sub>2</sub></th></tr></thead><tbody><tr><td>1</td><td>v1</td><td style="background-color: #f8d7da;">SE</td><td>AC</td></tr><tr><td>2</td><td>v0</td><td style="background-color: #f8d7da;">SE</td><td>AC</td></tr><tr><td>...</td><td></td><td></td><td></td></tr><tr><td>t + 1</td><td>v0</td><td style="background-color: #f8d7da;">SE</td><td>AC</td></tr><tr><td>...</td><td></td><td></td><td></td></tr><tr><td>n - f</td><td>v0</td><td style="background-color: #f8d7da;">SE</td><td>AC</td></tr></tbody></table>

if the guard in line 6 evaluates to true, the $t+1$ received messages may contain up to $f$ messages from the faulty processes. If $i$ correct processes send <ECHO>, for $1 \le i \le t$, the faulty processes may “help” some correct processes to pass over the $t+1$ threshold. That is, the effect of the $f$ faulty processes on the correct processes is captured by the "$-f$" component in the guards. As a result, we run only the correct processes, so that a system consists of $n-f$ copies of the STA.

For example, in the STA in Figure 1, processes send a message if they are in a location v1, se, or ac. Thus, the guards compare the number of processes in a location v1, se, or ac, which we denote by $\#\{v1, se, ac\}$, to some linear expression over the parameters, called a threshold. The assignment $v:=1$ in line 6 is modeled by the rule $r_2$, guarded with $\phi_1 \equiv \#\{v1, se, ac\} \ge t+1-f$. This guard evaluates to true if the number of processes in location v1, se, or ac is greater than or equal to $t+1-f$. The implicit “else” branch between lines 6 and 8 is modeled by the rule $r_1$, guarded with $\phi_3 \equiv \#\{v1, se, ac\} < t+1$. The effect of the faulty processes is captured by both the rules $r_1$ and $r_2$ being enabled. Similarly, the rules $r_5, r_7, r_8$ are guarded with the guard $\phi_2 \equiv \#\{v1, se, ac\} \ge n-t-f$, which is true when the number of process in one of v1, se, or ac is greater or equal to $n-t-f$, while the rules $r_3, r_4$ are guarded with $\phi_4 \equiv \#\{v1, se, ac\} < n-t$. The rule $r_6$ is unguarded, i.e., its guard is $\top$.

**Bounded Diameter.** An example execution of the synchronous reliable broadcast algorithm is depicted in Table 1 on the left. Observe that the guards of the rules $r_1$ and $r_2$ are both enabled in the configuration $\sigma_0$. One STA uses $r_2$ to go to se while the others use the self-loop $r_1$ to stay in v0. As both rules remain enabled, in every round one copy of STA can go to se. Hence, the configuration $\sigma_{t+1}$ has $t+1$ correct STA in location se and the rule $r_1$ becomes disabled. Then, all remaining STA go to se and then finally to ac. This execution depends on the parameter $t$, which implies that the length of this execution grows with $t$ and is thus unbounded. (We note that we can obtain longer executions, if some STA use the rule $r_4$). On the right, we see an execution where all copies of STA immediately move to se via rule $r_2$. That is, while the configuration $\sigma_{t+3}$ is reached by a long execution on the left, it is reached in just two steps on the right (observe that $\sigma'_2 = \sigma_{t+3}$). We are interested in whether there is a natural number $k$ (independent of $n, t$ and $f$) such that we can always shorten executions to executions of length $\le k$. (By length, we mean the number of transitions in an execution.) In such a case, we say that the STA has *bounded diameter*. We adapt
the definition of diameter from [14], and introduce an SMT-based procedure
for computing the diameter of the counter system. The procedure enumerates
candidates for the diameter bound, and checks (by calling an SMT solver) if the
number is indeed the diameter; if it finds such a bound, it terminates.

*Bounded Model Checking.* The existence of a bounded diameter motivates the use of bounded model checking, as safety verification can be reduced to checking the violation of a safety property in executions with length up to the diameter. Crucially, this approach is complete: if an execution reaches a bad configuration, this bad configuration is already reached by an execution of bounded length. Thus, once the diameter is found, we encode the violation of a safety property using a formula in Presburger arithmetic, and use an SMT to check for violations.

The SMT queries that are used for computing the diameter and encoding
the violation of the safety properties contain quantifiers for dealing with the
parameters symbolically. Surprisingly, performance of the SMT solvers on these
queries is very good, reflecting the recent progress in dealing with quantified
queries. We found that the diameter bounds of synchronous algorithms in the
literature are tiny (from 1 to 8), which makes our approach applicable in practice.
The verified algorithms are given in Section 4.

*Undecidability.* In [78], we showed that the parameterized reachability problem is in general undecidable for STA. In particular, this implies that some STA have unbounded diameters. We identified a class of STA which in theory have bounded diameters. For some STA outside of this class, our SMT-based procedure still can automatically find the diameter. Remarkably, the SMT-based procedure gives us the diameters that are independent of the parameters.

## 3.2 Asynchronous algorithms

*Asynchronous threshold automata.* Similarly as in STAs, nodes in asynchronous threshold automata (TAs) represent locations of processes, and edges represent local transitions. What makes a difference between an STA and a TA are shared variables and labels on edges that have a form $\gamma \mapsto \mathbf{act}$. A process moves along an edge labelled by $\gamma \mapsto \mathbf{act}$ and performs an action $\mathbf{act}$, only if the condition $\gamma$, called a *threshold guard*, evaluates to true.

We model reliable broadcast [76] using the same threshold automaton from
Figure 1 but with different edge labels in comparison to the STA. We use a shared
variable $x$ to capture the number of `<ECHO>` messages sent by correct processes.
We have two threshold guards: $\gamma_1: x \ge (t+1)-f$ and $\gamma_2: x \ge (n-t)-f$.
Depending on the initial value of a correct process, 0 or 1, the process is initially
either in location v0 or in v1. If its value is 1 a process broadcasts `<ECHO>`, and
executes the rule $r_3: \text{TRUE} \mapsto x++$. This is modelled by a process moving from v1
to sE and increasing the value of $x$. If its value is 0, it has to wait to receive
enough messages, i.e., it waits for $\gamma_1$ to become true, and then it broadcasts the
<ECHO> message and moves to location sE. Thus, $r_2$ is labelled by $\gamma_1 \mapsto x++$.
Finally, once a process has $\gamma_2$-enough <ECHO> messages, it sets accept to true
and moves to aC. Thus, $r_5$ is labelled by $\gamma_2$, whereas $r_7$ and $r_8$ by $\gamma_2 \mapsto x++$.
**Counter systems.** The semantics of threshold automata is captured by counter systems. Instead of storing the location of each process, we count the number of processes in each location, as all processes are identical. Therefore, a configuration comprises (i) values of the counters for each location, (ii) values of the shared variables, and (iii) parameter values. A configuration is initial if all processes are in initial locations, here v0 or v1, and all shared variables have value 0 (here x = 0). A transition of a process along an edge from location $\ell$ to location $\ell'$ — labelled by $\gamma \mapsto \text{act}$ — is modelled by the configuration update as follows: (i) the counter of $\ell$ is decreased by 1, and the counter of $\ell'$ is increased by 1, (ii) shared variables are updated according to the action act, and (iii) parameter values are unchanged. The key ingredient of our technique is acceleration of transitions, that is, many processes may move along the same edge simultaneously. In the resulting configuration, counters and shared variables are changed depending on the number of processes that participate in the transition. It is important to notice that any accelerated transition can be encoded in SMT.

**Reachability.** In [49], we determine a finite set of execution “patterns”, and then analyse each pattern separately. These patterns restrict the order in which threshold guards become true (if ever). Namely, we observe how the set of guards that evaluate to true changes along each execution. In our example, there are two (non-trivial) guards, $\gamma_1$ and $\gamma_2$. Initially, both are false as $x = 0$. During an execution, none, one, or both of them become true, but note that once they become true, they never return to false, as the number of sent messages $x$ cannot decrease. Thus, there is a finite set of execution patterns.

For instance, a pattern $\{\}...\{\gamma_1\}...\{\gamma_1, \gamma_2\}$ captures all finite executions $\tau$ that can be represented as $\tau = \tau_1 \cdot t_1 \cdot \tau_2 \cdot t_2 \cdot \tau_3$, where $\tau_1, \tau_2, \tau_3$ are sub-executions of $\tau$, and $t_1$ and $t_2$ are transitions. No threshold guard is enabled in a configuration visited by $\tau_1$, and only $\gamma_1$ is enabled in all configurations visited by $\tau_2$. Both guards are enabled in configurations visited by $\tau_3$, and $t_1$ and $t_2$ change the evaluation of the guards. Another pattern $\{\}...\{\gamma_2\}...\{\gamma_1, \gamma_2\}$ enables $\gamma_2$ before $\gamma_1$. Third pattern $\{\}...\{\gamma_1\}$ never enables $\gamma_2$.

To perform verification, we have to analyse all execution patterns. For each pattern we construct a so-called schema: A sequence of accelerated transitions that have as free variables: the number of processes that execute the transitions and the parameter values. In Figure 1 transitions are modelled by edges denoted with $r_i$, $i \in 1..8$. For instance, the pattern $\{\}...\{\gamma_1\}$ produces the schema:

$$S = \{ \underbrace{r_1, r_3, r_3}_{\tau_1}, \underbrace{\} \} \{\gamma_1\} \underbrace{r_1, r_2, r_3, r_4}_{\tau_2} \{\gamma_1\}.$$

There are two segments $\tau_1$ and $\tau_2$ corresponding to $\{\}$ and $\{\gamma_1\}$, respectively. In each of them we list all the rules that can be executed according to the true guards, in a fixed natural order: only $r_1$ and $r_3$ can be executed if no guard is enabled, and $r_1, r_2, r_3, r_4$ if only $\gamma_1$ holds true. Additionally, we have to list all the candidate rules for $t_1$ that can change the evaluation of the guards. In our example only $r_3$ can enable the guard $\gamma_1$.
<figure><img src="image_3.png" /><figcaption>**Fig. 4.** Three out of 18 shapes of lassos that satisfy the formula $\mathbf{F}(a \wedge \mathbf{F}d \wedge \mathbf{F}e \wedge \mathbf{G}b \wedge \mathbf{G}Fc)$. The crosses show cut points for: (A) formula $\mathbf{F}(a \wedge \mathbf{F}d \wedge \mathbf{F}e \wedge \mathbf{G}b \wedge \mathbf{G}Fc)$, (B) formula $\mathbf{F}d$, (C) formula $\mathbf{F}e$, (D) loop start, (E) formula $\mathbf{F}c$, and (F) loop end.</figcaption></figure>

We say that an execution follows the schema $\mathcal{S}$ if its transitions appear in the same order as in $\mathcal{S}$, but they are accelerated (every transition is executed by a number of processes, possibly zero). For example, if $(r, k)$ denotes that $k$ processes execute the rule $r$ simultaneously, then the execution $\rho = (r_1, 2)(r_3, 3)(r_2, 2)(r_4, 1)$ follows $\mathcal{S}$, where the transitions of the form $(r, 0)$ are omitted. In this case, we prove that for each execution $\tau$ of pattern $\{\} \dots \{\gamma_1\}$, there is an execution $\tau'$ that follows the schema $\mathcal{S}$, and $\tau$ and $\tau'$ reach the same configuration (when executed from the same initial configuration). This is achieved by *mover analysis*: inside any segment in which the set of enabled guards is fixed, we can swap adjacent transitions (that are not in a natural order); in this way we gather all transitions of the same rule next to each other, and transform them into a single accelerated transition. For example, $\tau = (r_3, 2)(r_1, 1)(r_3, 1)(r_1, 1)(r_2, 1)(r_4, 1)(r_2, 1)$ can be transformed into $\tau' = \rho$ from above, and they reach the same configurations. Therefore, instead of checking reachability for all executions of the pattern $\{\} \dots \{\gamma_1\}$, it is sufficient to analyse reachability only for the executions that follow the schema $\mathcal{S}$.

Every schema is encoded as an SMT query over linear integer arithmetic with free variables for acceleration factors, parameters, and counters. An SMT model gives us an execution of the counter system, which typically disproves safety.

For example, consider the following reachability problem: Can the system reach a configuration with at least one process in $\ell_3$? For each SMT query, we add the constraint that the counter of $\ell_3$ is non-zero in the final configuration. If the query is satisfiable, then there is an execution where at least one process reaches $\ell_3$. Otherwise, there is no such execution following the particular schema, where a process reaches $\ell_3$. That is why we have to check all schemas.

*Safety and Liveness.* In [50] we introduced a fragment of Linear Temporal Logic called **ELTL<sub>FT</sub>**. Its atomic propositions test location counters for zero. Moreover, this fragment only uses only two temporal operators: **F** (eventually) and **G** (globally). Our goal is to check whether there exists a counterexample to a temporal property, and thus formulas in this fragment represent negations of safety and liveness properties.

Our technique for verification of safety and liveness properties uses the reachability method as its basis. As before, we want to construct schemas that we can translate to SMT queries and check their satisfiability. Note that violations of liveness properties are infinite executions of a lasso shape, that is, $\tau \cdot \rho^\omega$, where $\tau$ and $\rho$ are finite executions. Hence, we have to enumerate the patterns of lassos.
<figure><img src="image_4.png" /><figcaption>Fig. 5. Ben-Or’s algorithm as PTA with resilience condition $n > 3t \land t > 0 \land t \ge f \ge 0$.</figcaption></figure>

$$r_5: x_0+x_1 \ge n-t-f \land x_0 \ge (n+t)/2-f \mapsto y_0^{++}$$

$$r_6: x_0+x_1 \ge n-t-f \land x_1 \ge (n+t)/2-f \mapsto y_1^{++}$$

$$r_7: x_0+x_1 \ge n-t-f \land x_0 \ge (n-3t)/2-f \\ \land x_1 \ge (n-3t)/2-f \mapsto y_?^{++}$$

$$r_8: y_0+y_1+y? \ge n-t-f \land y? \ge (n-3t)/2-f \\ \land y_0 \ge t+1-f$$

$$r_9: y_0+y_1+y? \ge n-t-f \land y_0 \ge (n+t)/2-f$$

$$r_{10}: y_0+y_1+y? \ge n-t-f \land y? \ge (n-3t)/2-f \\ \land y? \ge n-2t-f-1$$

These shapes depend not only on the values of thresholds, but also on the evaluations of atomic propositions that appear in temporal properties. We single out configurations in which atomic propositions evaluate to true, and call them *cut points*, as they “cut” an execution into finitely many segments (see Figure 4).

We combine these cut points with those “cuts” in which threshold guards become enabled (as in the reachability analysis). All the possible orderings in which thresholds and formulas become true, give us a finite set of lasso patterns. We construct a schema for each shape by first defining schemas for each of the segments between two adjacent cut points. On one hand, for reachability it is sufficient to execute all enabled rules of that segment exactly once in the natural order. Thus, each sub-execution $\tau_i$ can be transformed into $\tau'_i$ that follows the segment’s schema, so that $\tau_i$ and $\tau'_i$ reach the same final configuration. On the other hand, safety and liveness properties reason about atomic propositions inside executions. To this end, we introduced a *property specific mover analysis* that allows us to construct schemas by executing all enabled rules a fixed number of times in a specific order. The number of rule repetitions depends on a temporal property; it is typically two or three.

For each lasso pattern we encode its schema in SMT and check its satisfiability. As ELTL<sub>FT</sub> formulas are negations of specifications, an SMT model gives us a counterexample. If no schema is satisfiable, the temporal property holds true.

### 3.3 Asynchronous randomized multi-round algorithms

*Probabilistic threshold automata.* Randomized algorithms typically have an unbounded number of asynchronous rounds and randomized choices. Probabilistic threshold automata (PTAs) are extensions of asynchronous threshold automata that allow formalizing these features. A PTA modelling Ben-Or’s algorithm from Figure 3 is shown in Figure 5. The behaviour of a process in a single round is modelled by the solid edges. Note that in this case threshold guards should be evaluated according to the values of shared variables, e.g., $x_0$ and $x_1$, in the observed round. The dashed edges model round switches: once a process reaches a final location in a round, it moves to an initial location of the next round. The coin toss is modelled by the branching rule $r_{10}$: a process in location *SP* by moving along this fork can reach either $CT_0$ or $CT_1$, both with probability 1/2.
*Unboundedly many rounds.* In order to overcome the issue of unboundedly many rounds, we prove that we can verify PTAs by analysing a one-round automaton that fits in the framework of Section 3.2. In [11], we prove that one can reorder transitions of any fair execution such that their round numbers are in a non-decreasing order. The obtained ordered execution is stutter equivalent to the original one. Thus, the both execution satisfy the same LTL<sub>x</sub> properties over the atomic propositions of one round. In other words, the distributed system can be transformed to a sequential composition of one-round systems.

The main problem with isolating a one-round system is that consensus spec-
ifications often talk about at least two different rounds. In this case we need to
use round invariants that imply the specifications. For example, if we want to
verify agreement, we have to check that no two processes decide different values,
possibly in different rounds. We do this in two steps: (i) we check the round
invariant that no process changes its decision from round to round, and (ii) we
check that within a round no two processes disagree.

*Probabilistic properties.* The semantics of a probabilistic threshold automaton is an infinite-state Markov decision process (MDP), where the non-determinism is traditionally resolved by an adversary. In [11], we restrict our attention to so-called *round-rigid adversaries*, that is, fair adversaries that generate executions in which a process enters round *r* + 1 only after all processes finished round *r*.

Verifying almost-sure termination under round-rigid adversaries calls for distinct arguments. Our methodology follows the lines of the manual proof of Ben Or's consensus algorithm by Aguilera and Toueg [3]. However, our arguments are not specific to Ben Or's algorithm, and apply to other randomized distributed algorithms (see Table 2). Compared to their paper-and-pencil proof, the threshold automata framework required us to provide a more formal setting and a more informative proof, also pinpointing the needed hypotheses. The crucial parts of our proof are automatically checked by the model checker ByMC.

4 ByMC: Byzantine model checker

*Overview of the techniques implemented in ByMC.* Table 2 shows coverage of various asynchronous algorithms with the techniques that are implemented in ByMC. In the following, we give a brief description of these techniques.

We started development of ByMC in 2012. We extended the classic {0, 1, ∞}-counter abstraction to threshold-guarded algorithms [47,46,41]. Instead of using the predefined intervals [0, 1) and [1, ∞), the tool was computing parametric intervals by simple static analysis, for instance, the intervals [0, 1), [1, t + 1), [t+1, n−t), and [n−t, ∞). ByMC was automatically constructing the finite-state counter abstraction from protocol specifications in Parameterized Promela. This finite abstraction was automatically checked with Spin [45]. As this abstraction was typically too coarse for liveness checking, we have implemented a simple counterexample-guided abstraction refinement loop for parameterized systems. This technique is called CA+SPIN in Table 2.
<table><caption>**Table 2.** Asynchronous fault-tolerant distributed algorithms that are verified by different generations of ByMC. For every technique and algorithm we show, whether the technique could verify the properties: safety (S), liveness (L), almost-sure termination under round-rigid adversaries (RRT), or none of them (-).</caption><thead><tr><th>Algorithm</th><th>CA+SPIN[47]</th><th>CA+BDD[55]</th><th>CA+SAT[55]</th><th>SMT-S[52]</th><th>SMT-L[50]</th><th>SMT+MR[11]</th></tr></thead><tbody><tr><td>FRB [26]</td><td>S+L</td><td>S+L</td><td>S</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>STRB [77]</td><td>S+L</td><td>S+L</td><td>S</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>ABA [18]</td><td>-</td><td>S+L</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>NBACG [42]</td><td>-</td><td>-</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>NBACR [71]</td><td>-</td><td>-</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>CBC [66]</td><td>-</td><td>-</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>CF1S [32]</td><td>-</td><td>S+L</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>C1CS [19]</td><td>-</td><td>-</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>BOSCO [75]</td><td>-</td><td>-</td><td>-</td><td>S</td><td>S+L</td><td>-</td></tr><tr><td>Ben-Or [7]</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>S+RRT</td></tr><tr><td>RABC [17]</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>S+RRT</td></tr><tr><td>kSet [65]</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>S+RRT</td></tr><tr><td>RS-BOSCO [75]</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>S+RRT</td></tr></tbody></table>

Spin scaled only to two broadcast algorithms. Thus, we extended ByMC with the abstraction/checking loop that used nuXmv [24] instead of Spin. This technique is called CA+BDD in Table 2. Although this extension scaled better than CA+SPIN, we could only check two more benchmarks with it. Detailed discussions of the techniques CA+SPIN and CA+BDD can be found in [41,53].

By running the abstraction/checking loop in nuXmv, we found that the bounded model checking algorithms of nuXmv could check long executions of our benchmarks. However, bounded model checking in general does not have completeness guarantees. In [51,55], we have shown that the counter systems of (asynchronous) threshold automata have computable bounded diameters, which gave us a way to use bounded model checking as a complete verification approach for reachability properties. This technique is called CA+SAT in Table 2. Still, the computed upper bounds were too high for achieving complete verification.

The SMT-based techniques of Section 3.2 are called SMT-S (for safety) and SMT-L (for liveness) in Table 2. These techniques accept either threshold automata or Parametric Promela on their input. As one can see, these techniques are the most efficient techniques that are implemented in ByMC. More details on the experiments can be found in the tool paper [54].

Finally, the technique for multi-round randomized algorithms is called SMT-MR in Table 2. This technique is explained in Section 3.3.

*Model checking synchronous threshold automata.* The bounded model checking approach for STA introduced in Section 3.1 is not yet integrated into ByMC. It is implemented as a stand-alone tool, available at [1]. In [78], we encoded multiple synchronous algorithms from the literature, such as consensus [63,72,10,9,13], k-set agreement (from [63], whose pseudocode is given in Figure 2 and [72]),
<table><caption>**Table 3.** Synchronous fault-tolerant distributed algorithms verified with the bounded model checking approach from [78]. With ✓ we show that: the SMT based procedure finds a diameter bound with Z3 (DIAM+Z3) and CVC4 (DIAM+CVC4); there is a theoretical bound on the diameter (DIAM+THM). We verify safety (S) by bounded model checking with Z3 (BMC+Z3) and CVC4 (BMC+CVC4).</caption><thead><tr><th>Algorithm</th><th>DIAM+Z3</th><th>DIAM+CVC4</th><th>DIAM+THM</th><th>BMC+Z3</th><th>BMC+CVC4</th></tr></thead><tbody><tr><td>FloodSet [63]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>FairCons [72]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>PhaseKing [10]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>PhaseQueen [9]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>HybridKing [13]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>ByzKing [13]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>OmitKing [13]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>HybridQueen [13]</td><td>–</td><td>–</td><td>–</td><td>–</td><td>–</td></tr><tr><td>ByzQueen [13]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>OmitQueen [13]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>FloodMin [63]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>kSetOmit [72]</td><td>✓</td><td>✓</td><td>–</td><td>S</td><td>S</td></tr><tr><td>RB [77]</td><td>✓</td><td>✓</td><td>✓</td><td>S</td><td>S</td></tr><tr><td>HybridRB [13]</td><td>✓</td><td>✓</td><td>✓</td><td>S</td><td>S</td></tr><tr><td>OmitRB [13]</td><td>✓</td><td>✓</td><td>✓</td><td>S</td><td>S</td></tr></tbody></table>

and reliable broadcast (from [77,13]) algorithms. We use Z3 [67] and CVC4 [6] as back-end SMT solvers. Table 3 gives an overview of the verified synchronous algorithms. For further details on the experimental results, see [78].

# 5 Towards verification of Tendermint consensus

Tendermint consensus is a fault-tolerant distributed algorithm for proof-of-stake blockchains [22]. Tendermint can handle Byzantine faults under the assumption of partial synchrony. It is running in the Cosmos network, where currently over 100 validator nodes are committing transactions and are managing the ATOM cryptocurrency [21]. Tendermint consensus heavily relies on threshold guards, as can be seen from its pseudo-code in [22][Algorithm 1]. For instance, one of the Tendermint rules has the following precondition:

$$ \begin{array}{l} \textbf{upon} \langle \text{PROPOSAL}, h_p, \text{round}_p, v, \ast \rangle \textbf{ from } \text{proposer}(h_p, \text{round}_p) \\ \textbf{AND} \ 2f + 1 \langle \text{PREVOTE}, h_p, \text{round}_p, \text{id}(v) \rangle \\ \textbf{while } \text{valid}(v) \land \text{step}_p \geq \text{prevote} \textbf{ for the first time} \end{array} \quad (1) $$

The rule 1 requires two kinds of messages: (1) a single message of type PRO-POSAL carrying a proposal *v* from the process *proposer*(*h*<sub>*p*</sub>, *round*<sub>*p*</sub>) that is identified by the current round *round*<sub>*p*</sub> and consensus instance *h*<sub>*p*</sub>, and (2) messages of type PREVOTE from several nodes. Here the term 2*f* + 1 (taken from the original paper) in fact does not refer to a number of processes. Rather each
process has a voting power (an integer that expresses how many votes a process
has), and $2f+1$ (in combination with $n = 3t+1$) expresses that nodes that have
sent **PREVOTE** have more than two-thirds of voting power. Although this rule
bears similarity with the rules of threshold automata, Tendermint consensus has
the following features that cannot be directly modelled with threshold automata:

1. In every consensus instance $h_p$ and round $round_p$, a single proposer sends a value that the nodes vote on. The identity of the proposer can be accessed with the function *proposer*($h_p$, *round*$_p$). *This feature breaks symmetry among individual nodes*, which is required by our modelling with counter systems. Moreover, the proposer function should be fairly distributed among the nodes, e.g., it can be implemented with round robin.

2. Whereas the classical example algorithms in this paper count messages, Tendermint evaluates the voting power of the nodes from which messages where received. This adds an additional layer of complexity.

3. Liveness of Tendermint requires the distributed system to reach a global stabilization period, when every message could be delivered not later than after a bounded delay. This model of partial synchrony lies between synchronous and asynchronous computations and requires novel techniques for parameterized verification.

As a first step towards parameterized verification, we are specifying Tender-
mint consensus in TLA⁺ [59] and check its properties with the symbolic model
checker APALACHE [48]. As Apalache currently supports only non-parameterized
verification — the specification parameters must be fixed — we are planning to
use automatic abstractions to build a bridge between Apalache and ByMC.

**6 Conclusions**

Computer-aided verification of distributed algorithms and systems is a lively
research area. Approaches range from mechanized verification [44,81,74] over
deductive verification [31,8,69,34,29] to automated techniques [16,56,5,40]. In
our work, we follow the idea of identifying fragments of automata and logic that
are sufficiently expressive for capturing interesting algorithms and specifications,
while these fragments are amenable for completely automated verification. We
introduced threshold automata for that and implemented our verification tech-
niques in the open source tool ByMC [54]. By doing so, we verified several
challenging distributed algorithms; most of them were verified for the first time.

The threshold automata framework has proved to be both of practical relevance as well as of theoretical interest. There are several ongoing projects that consider automatic generation of threshold automata from code, complexity theoretic analysis of verification problems, and more refined probabilistic reasoning.

*Acknowledgments.* This survey is based on the results of a long-lasting research agenda [47,49,50,60,57,12,79]. We are grateful to our past and present collaborators Nathalie Bertrand, Roderick Bloem, Annu Gmeiner, Jure Kukovec, Ulrich Schmid, Helmut Veith, and Florian Zuleger, who contributed to many of the described ideas that are now implemented in ByMC.
References

1. Bounded Model Checking of STA. https://github.com/istoilkovska/syncTA

2. Abraham, I., Malkhi, D., Nayak, K., Ren, L., Spiegelman, A.: Solidus: An incentive-compatible cryptocurrency based on permissionless Byzantine consensus. CoRR abs/1612.02916 (2016), http://arxiv.org/abs/1612.02916

3. Aguilera, M., Toueg, S.: The correctness proof of Ben-Or's randomized consensus algorithm. Distributed Computing pp. 1–11 (2012)

4. Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. IPL 15, 307–309 (1986)

5. Bakst, A., von Gleissenthall, K., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. PACMPL 1(OOPSLA), 110:1–110:27 (2017)

6. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV. pp. 171–177 (2011)

7. Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In: PODC. pp. 27–30 (1983)

8. Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: CAV. LNCS, vol. 11562, pp. 245–266. Springer (2019)

9. Berman, P., Garay, J.A., Perry, K.J.: Asymptotically Optimal Distributed Consensus. Tech. rep., Bell Labs (1989), plan9.bell-labs.co/who/garay/asopt.ps

10. Berman, P., Garay, J.A., Perry, K.J.: Towards Optimal Distributed Consensus (Extended Abstract). In: FOCS. pp. 410–415 (1989)

11. Bertrand, N., Konnov, I., Lazic, M., Widder, J.: Verification of Randomized Consensus Algorithms Under Round-Rigid Adversaries. In: CONCUR 2019. LIPIcs, vol. 140, pp. 33:1–33:15 (2019)

12. Bertrand, N., Konnov, I., Lazić, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: CONCUR. pp. 33:1–33:15 (2019)

13. Biely, M., Schmid, U., Weiss, B.: Synchronous Consensus Under Hybrid Process and Link Failures. Theor. Comput. Sci. 412(40), 5602–5630 (2011)

14. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: TACAS. LNCS, vol. 1579, pp. 193–207 (1999)

15. 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 (2015)

16. Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: CAV. pp. 372–391 (2018)

17. Bracha, G.: Asynchronous Byzantine agreement protocols. Inf. Comput. 75(2), 130–143 (1987)

18. Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985)

19. Brasileiro, F.V., Greve, F., Mostéfaoui, A., Raynal, M.: Consensus in one communication step. In: PaCT. LNCS, vol. 2127, pp. 42–50 (2001)

20. Buchman, E.: Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. Master's thesis, University of Guelph (2016), http://hdl.handle.net/10214/9769

21. Buchman, E., Kwon, J.: Cosmos whitepaper: a network of distributed ledgers (2018), https://cosmos.network/resources/whitepaper

22. Buchman, E., Kwon, J., Milosevic, Z.: The latest gossip on bft consensus. arXiv preprint arXiv:1807.04938 (2018), https://arxiv.org/abs/1807.04938
23. Buterin, V.: A next-generation smart contract and decentralized application platform (2014)

24. Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: CAV. pp. 334–342 (2014)

25. Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)

26. Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. JACM 43(2), 225–267 (March 1996)

27. Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distributed Computing 22(1), 49–71 (2009)

28. Chaudhuri, S., Herlihy, M., Lynch, N.A., Tuttle, M.R.: Tight Bounds for *k*-set Agreement. J. ACM 47(5), 912–943 (2000)

29. Damian, A., Drăgoi, C., Militaru, A., Widder, J.: Communication-closed asynchronous protocols. In: CAV. pp. 344–363 (2019)

30. Decker, C., Seidel, J., Wattenhofer, R.: Bitcoin meets strong consistency. In: ICDCN. pp. 13:1–13:10 (2016), https://doi.org/10.1145/2833312.2833321

31. Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almost-synchronous reductions. In: OOPSLA. pp. 709–725 (2014)

32. Dobre, D., Suri, N.: One-step consensus with zero-degradation. In: DSN. pp. 137–146 (2006)

33. Dolev, D., Dwork, C., Stockmeyer, L.: On the minimal synchronism needed for distributed consensus. J. ACM 34, 77–97 (1987)

34. Drăgoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A Logic-Based Framework for Verifying Consensus Algorithms. In: VMCAI. LNCS, vol. 8318, pp. 161–181 (2014)

35. Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288–323 (1988)

36. Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)

37. Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL. pp. 85–94 (1995)

38. Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)

39. Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32(2), 374–382 (1985)

40. v. Gleissenthall, K. Gökhan Kici, R., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony. In: POPL (2019), (to appear)

41. Gmeiner, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In: Formal Methods for Executable Software Models. pp. 122–171. LNCS, Springer (2014)

42. Guerraoui, R.: Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distributed Computing 15(1), 17–25 (2002)

43. Hadzilacos, V., Toueg, S.: Fault-tolerant broadcasts and related problems. In: Mulender, S. (ed.) Distributed systems (2nd Ed.). pp. 97–145 (1993)

44. Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83–92 (2017)

45. Holzmann, G.: The SPIN Model Checker. Addison-Wesley (2003)

46. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms (October 2012), http://arxiv.org/abs/1210.3846
47. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD. pp. 201–209 (2013)

48. Konnov, I., Kukovec, J., Tran, T.: TLA+ model checking made symbolic. PACMPL 3(OOPSLA), 123:1–123:30 (2019)

49. Konnov, I., Lazić, M., Veith, H., Widder, J.: Para²: Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Methods in System Design 51(2), 270–307 (2017)

50. Konnov, I., Lazić, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL. pp. 719–734 (2017)

51. Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. In: CONCUR. LNCS, vol. 8704, pp. 125–140 (2014)

52. Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: Parameterized model checking of threshold-based distributed algorithms. In: CAV (Part I). LNCS, vol. 9206, pp. 85–102 (2015)

53. Konnov, I., Veith, H., Widder, J.: What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: PSI 2015, in Memory of Helmut Veith, Revised Selected Papers. LNCS, vol. 9609, pp. 6–21. Springer (2016)

54. Konnov, I., Widder, J.: ByMC: Byzantine model checker. In: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems. pp. 327–342. Springer International Publishing, Cham (2018), https://hal.inria.fr/hal-01909653

55. Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation 252, 95–109 (2017)

56. Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR. pp. 21:1–21:17 (2018)

57. Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: All flavors of threshold automata. In: CONCUR. LIPIcs, vol. 118, pp. 19:1–19:17 (2018)

58. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

59. Lamport, L.: Specifying systems: The TLA+ language and tools for hardware and software engineers. Addison-Wesley (2002)

60. Lazić, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: OPODIS. LIPIcs, vol. 95, pp. 32:1–32:20 (2017), https://doi.org/10.4230/LIPIcs.OPODIS.2017.32

61. Le Lann, G.: Distributed systems – towards a formal approach. In: IFIP Congress. pp. 155–160 (1977), http://www-roc.inria.fr/novaltis/publications/IFIP%20Congress%201977.pdf

62. Lincoln, P., Rushby, J.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: FTCS. pp. 402–411 (1993)

63. Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco, USA (1996)

64. Malekpour, M.R., Siminiceanu, R.: Comments on the “Byzantine self-stabilizing pulse synchronization”. protocol: Counterexamples. Tech. rep., NASA (Feb 2006), http://shemesh.larc.nasa.gov/fm/papers/Malekpour-2006-tm213951.pdf

65. Mostéfaoui, A., Moumen, H., Raynal, M.: Randomized k-set agreement in crash-prone and Byzantine asynchronous systems. Theor. Comput. Sci. 709, 80–97 (2018)

66. Mostéfaoui, A., Mourgaya, E., Parvédy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: DSN. pp. 541–550 (2003)
67. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS. pp. 337–340 (2008)

68. Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008), https://bitcoin.org/bitcoin.pdf

69. Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI. pp. 614–630 (2016)

70. Pease, M.C., Shostak, R.E., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228–234 (1980)

71. Raynal, M.: A case study of agreement problems in distributed systems: Non-blocking atomic commitment. In: HASE. pp. 209–214 (1997)

72. Raynal, M.: Fault-Tolerant Agreement in Synchronous Message-Passing Systems. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2010)

73. Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv. 22(4), 299–319 (1990)

74. Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. PACMPL 2(POPL), 28:1–28:30 (2018)

75. Song, Y.J., van Renesse, R.: Bosco: One-step Byzantine asynchronous consensus. In: DISC. LNCS, vol. 5218, pp. 438–450 (2008)

76. Srikanth, T.K., Toueg, S.: Optimal clock synchronization. Journal of the ACM 34(3), 626–645 (1987)

77. Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Dist. Comp. 2, 80–94 (1987)

78. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: TACAS. LNCS, vol. 11428, pp. 357–374. Springer (2019)

79. Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking. In: TACAS. LNCS, vol. 11428, pp. 357–374 (2019)

80. Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)

81. Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI. pp. 357–368 (2015)

82. Yin, M., Malkhi, D., Reiter, M.K., Golan-Gueta, G., Abraham, I.: Hotstuff: BFT consensus with linearity and responsiveness. In: PODC. pp. 347–356 (2019)