key: cord-0045079-c8pbn8m1 authors: Konnov, Igor; Lazić, Marijana; Stoilkovska, Ilina; Widder, Josef title: Tutorial: Parameterized Verification with Byzantine Model Checker date: 2020-05-13 journal: Formal Techniques for Distributed Objects, Components, and Systems DOI: 10.1007/978-3-030-50086-3_11 sha: b6fd0b1ccf1e891d9ecf1af46df3dfa5e521495d doc_id: 45079 cord_uid: c8pbn8m1 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 [Formula: see text]; (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., [Formula: see text]. 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. The recent advent of blockchain technologies [2, 20, 23, 30, 68, 81] 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, 15, 37, 38, 79] apply in this setting. One way to circumvent 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 [81] 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 Sect. 5 . In addition to practical importance, the reasons for the long-standing interest [39, 58, 61, 70] 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) [33, 39, 70 ]. 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 Sect. 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 Sect. 3 we will discuss how these algorithms can be modeled and how they can be automatically verified. 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 [25, 27, 35] to establish the Order property. For instance, the atomic broadcast algorithm from [25] contains these two sub-algorithms. The simplest canonical system model that allows one to solve consensus is the synchronous one, and we discuss it in Sect. 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 Sect. 2.3. In fact, reliable broadcast can be solved with an asynchronous distributed algorithm. We discuss their characteristics in Sect. 2.2. 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 Fig. 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 Sect. 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 Fig. 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 [28] 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 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. We now discuss the asynchronous semantics of the code in Fig. 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. A prominent example is Ben-Or's fault-tolerant binary consensus [7] algorithm in Fig. 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 essages 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 [29, 36] . 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. In [78] , we introduced the synchronous variant of threshold automata, and studied their applicability and limitations for verification of synchronous faulttolerant 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 Fig. 1 (left). A synchronous threshold automaton (STA) that encodes the pseudocode of this algorithm is given in Fig. 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 i ∈ {v0, v1, se, ac} (a node in the graph), we have a counter κ i that stores the number of processes located in 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 Fig. 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, 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 , for 1 ≤ i ≤ 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 Fig. 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 φ 1 ≡ #{v1, se, ac} ≥ t + 1 − f . This guard evaluates to true if he 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 φ 3 ≡ #{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 φ 2 ≡ #{v1, se, ac} ≥ 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 φ 4 ≡ #{v1, se, ac} < n − t. The rule r 6 is unguarded, i.e., its guard is . 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 σ 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 σ 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 σ t+3 is reached by a long execution on the left, it is reached in just two steps on the right (observe that σ 2 = σ 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 ≤ 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 Sect. 4. 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. 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 γ → act. A process moves along an edge labelled by γ → act and performs an action act, only if the condition γ, called a threshold guard, evaluates to true. We model reliable broadcast [76] using the same threshold automaton from Fig. 1 but with different edge labels in comparison to the STA. We use a shared variable x to capture the number of messages sent by correct processes. We have two threshold guards: γ 1 : x ≥ (t + 1) − f and γ 2 : x ≥ (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 , and executes the rule r 3 : true → 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 γ 1 to become true, and then it broadcasts the message and moves to location se. Thus, r 2 is labelled by γ 1 → x++. Finally, once a process has γ 2 -enough messages, it sets accept to true and moves to ac. Thus, r 5 is labelled by γ 2 , whereas r 7 and r 8 by γ 2 → 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 to locationlabelled by γ → act -is modelled by the configuration update as follows: (i) the counter of is decreased by 1, and the counter of 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. 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, γ 1 and γ 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 {} . . . {γ 1 } . . . {γ 1 , γ 2 } captures all finite executions τ that can be represented as τ = τ 1 · t 1 · τ 2 · t 2 · τ 3 , where τ 1 , τ 2 , τ 3 are subexecutions of τ , and t 1 and t 2 are transitions. No threshold guard is enabled in a configuration visited by τ 1 , and only γ 1 is enabled in all configurations visited by 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 Fig. 1 F (a ∧ F d ∧ F e ∧ G b ∧ G F c) . The crosses show cut points for: (A) formula F (a ∧ F d ∧ F e ∧ G b ∧ G F c) , There are two segments τ 1 and τ 2 corresponding to {} and {γ 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 γ 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 γ 1 . We say that an execution follows the schema S if its transitions appear in the same order as in 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 ρ = (r 1 , 2)(r 3 , 3)(r 2 , 2)(r 4 , 1) follows S, where the transitions of the form (r, 0) are omitted. In this case, we prove that for each execution τ of pattern {} . . . {γ 1 }, there is an execution τ that follows the schema S, and τ and τ 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, τ = (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 τ = ρ from above, and they reach the same configurations. Therefore, instead of checking reachability for all executions of the pattern {} . . . {γ 1 }, it is sufficient to analyse reachability only for the executions that follow the schema 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 3 ? For each SMT query, we add the constraint that the counter of 3 is non-zero in the final configuration. If the query is satisfiable, then there is an execution where at least one process reaches 3 . Otherwise, there is no such execution following the particular schema, where a process reaches 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 FT . 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, τ · ρ ω , where τ and ρ are finite executions. Hence, we have to enumerate the patterns of lassos. 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 Fig. 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 τ i can be transformed into τ i that follows the segment's schema, so that τ i and τ 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 FT formulas are negations of specifications, an SMT model gives us a counterexample. If no schema is satisfiable, the temporal property holds true. 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 Fig. 3 is shown in Fig. 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 Sect. 3.2. In [11] , we prove that one can reorder transitions of any fair execution such that their round numbers are in a nondecreasing order. The obtained ordered execution is stutter equivalent to the original one. Thus, the both execution satisfy the same LTL -X 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 specifications 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 socalled 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. 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 [41, 46, 47] . Instead of using [52] SMT-L [50] SMT+MR [11] FRB [26] S+L S+L S S S+L -STRB [77] S+L S+L S S S+L - 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 . 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 Sect. 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] . 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 [9, 10, 13, 63, 72] , k-set agreement (from [63] , whose pseudocode is given in Fig. 2 and [72] ), and reliable broadcast (from [13, 77] ) 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] . 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: upon PROPOSAL, h p , round p , v, * from proposer(h p , round p ) AND 2f + 1 PREVOTE, h p , round p , id (v) while valid(v) ∧ step p ≥ prevote for the first time 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 p , round p ) that is identified by the current round round p and consensus instance h p , and (2) messages of type PREVOTE from several nodes. Here the term 2f + 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 Tendermint 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. Computer-aided verification of distributed algorithms and systems is a lively research area. Approaches range from mechanized verification [44, 74, 80] over deductive verification [8, 29, 31, 34, 69] to automated techniques [5, 16, 40, 56] . 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 techniques 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. Bounded Model Checking of STA Solidus: an incentivecompatible cryptocurrency based on permissionless Byzantine consensus The correctness proof of Ben-Or's randomized consensus algorithm Limits for automatic verification of finite-state concurrent systems Verifying distributed programs via canonical sequentialization CVC4. In: CAV Another advantage of free choice: Completely asynchronous agreement protocols Verification of thresholdbased distributed algorithms by decomposition to decidable logics Asymptotically optimal distributed consensus Towards optimal distributed consensus (Extended Abstract) Verification of randomized consensus algorithms under round-rigid adversaries Verification of randomized consensus algorithms under round-rigid adversaries Synchronous consensus under hybrid process and link failures Symbolic Model Checking without BDDs. TACAS Decidability of Parameterized Verification. Morgan & Claypool, Synthesis Lectures on Distributed Computing Theory On the completeness of verifying message passing programs under bounded asynchrony Asynchronous Byzantine agreement protocols Asynchronous consensus and broadcast protocols Consensus in one communication step PaCT Tendermint: Byzantine Fault Tolerance in the Age of Blockchains Cosmos whitepaper: a network of distributed ledgers The latest gossip on BFT consensus A next-generation smart contract and decentralized application platform The NUXMV symbolic model checker, In: CAV. pp Unreliable failure detectors for reliable distributed systems Unreliable failure detectors for reliable distributed systems The heard-of model: computing in distributed systems with benign faults Tight Bounds for k-set Agreement Communication-closed asynchronous protocols Bitcoin meets strong consistency Natural proofs for asynchronous programs using almost-synchronous reductions One-step consensus with zero-degradation On the minimal synchronism needed for distributed consensus A logic-based framework for verifying consensus algorithms VMCAI Consensus in the presence of partial synchrony Decomposition of distributed programs into communicationclosed layers Reasoning about rings Decidability of model checking for infinite-state concurrent systems Impossibility of distributed consensus with one faulty process Pretend synchrony Tutorial on parameterized model checking of fault-tolerant distributed algorithms Non-blocking atomic commit in asynchronous distributed systems with failure detectors Fault-tolerant broadcasts and related problems Ironfleet: proving safety and liveness of practical distributed systems The SPIN Model Checker Counter attack on byzantine generals: parameterized model checking of fault-tolerant distributed algorithms Parameterized model checking of fault-tolerant distributed algorithms by abstraction TLA+ model checking made symbolic. PACMPL 3(OOPSLA) Para 2 : Parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. CONCUR SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms What you always wanted to know about model checking of fault-tolerant distributed algorithms ISoLA 2018 On the completeness of bounded model checking for threshold-based distributed algorithms: reachability Synchronizing the asynchronous Reachability in parameterized systems: all flavors of threshold automata Time, clocks, and the ordering of events in a distributed system Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers Synthesis of distributed algorithms with parameterized threshold guards Distributed systems -towards a formal approach A formally verified algorithm for interactive consistency under a hybrid fault model Comments on the "Byzantine self-stabilizing pulse synchronization Randomized k-set agreement in crashprone and Byzantine asynchronous systems Evaluating the conditionbased approach to solve consensus Z3: an efficient SMT solver Bitcoin: a peer-to-peer electronic cash system Ivy: safety verification by interactive generalization Reaching agreement in the presence of faults A case study of agreement problems in distributed systems: Nonblocking atomic commitment Fault-tolerant agreement in synchronous message-passing systems Implementing fault-tolerant services using the state machine approach: a tutorial Programming and proving with distributed protocols one-step Byzantine asynchronous consensus. DISC Optimal clock synchronization Simulating authenticated broadcasts to derive simple faulttolerant algorithms Verifying safety of synchronous fault-tolerant algorithms by bounded model checking Proving properties of a ring of finite-state machines Verdi: a framework for implementing and formally verifying distributed systems Hotstuff: BFT consensus with linearity and responsiveness Acknowledgments. This survey is based on the results of a long-lasting research agenda [12, 47, 49, 50, 57, 60, 78] . 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.