The 12th Workshop on Formal Reasoning in Distributed Algorithms

Where the number of trials of a mechanism is bounded, it is sensible to engineer that mechanism to have such a small probability ϵ of failure that over all time we can discount the probability δ of it ever going wrong. So if there are at most 10⁹ trials and we are prepared to accept a δ=10⁻⁹ probability of failure over all time, this would suggest ϵ=10⁻¹⁸. If a blockchain has a good source of random numbers, this allows us to create many efficient mechanisms, including consensus, that are stochastically certain to work. A number of interesting challenges in formal reasoning arise.

Game-theoretic security analysis of blockchain technologies has proven highly valuable. Such analysis examines protocols from an economic perspective, specifically by exploring the economic incentives that drive user behavior. Thus, it ensures that deviating from the intended, honest behavior of a protocol is not financially beneficial: as long as users follow the protocol, they cannot be financially harmed, regardless of how others behave. Such an economic analysis of blockchain protocols can be encoded as an automated reasoning problem in the first-order theory of real arithmetic, thereby reducing game-theoretic reasoning to satisfiability modulo theories (SMT) solving. We conduct a divide-and-conquer security analysis based on compositional reasoning over games. Our compositional analysis is incremental: we divide games into subgames such that changes to one subgame do not necessitate re-analyzing the entire game, but only the ancestor nodes. Our approach is sound, complete, and effective: combining the security properties of subgames yields security of the entire game. Experimental results show that compositional reasoning scales well to games with millions of nodes, enabling security analysis of large real-life protocols.

In distributed systems with asymmetric trust, each participant is free to make its own trust assumptions about others, captured by an asymmetric quorum system. This contrasts with ordinary, symmetric quorum systems and threshold models, where trust assumptions are uniformly shared among participants. In the symmetric setting, quorum systems must satisfy the consistency and availability properties to solve key problems like reliable broadcast and consensus. But what properties are needed in the asymmetric setting to solve these problems? We examine this question in both the crash-fault and Byzantine models. In the crash-fault setting, any quorum system satisfying consistency and availability can be transformed into a symmetric one, removing any benefit from asymmetric trust. In the Byzantine model, consistency and availability are not enough to solve reliable broadcast and consensus. Existing approaches overcome this by introducing stronger assumptions. We show that some of these assumptions are overly restrictive, so much so that they effectively eliminate the benefits of asymmetric trust. We introduce a new way to characterize asymmetric problems and, based on this, present protocols for reliable broadcast and consensus that work under weaker assumptions than existing solutions.

The Delaying the Future approach provides a framework for reasoning about the order of events in executions: under precise conditions we identified, events can be postponed and reordered in ways that remain indistinguishable to processes. This approach applies across different computational models. Characterizing the conditions under which this is possible requires defining an appropriate relation between events for each model, capturing when order must be preserved. This talk will show how the approach yields clean characterizations of communication requirements in asynchronous message-passing systems (DISC 2024), and how the same reasoning extends to shared-memory systems under the TSO memory model (DISC 2025). This talk highlights the power of the Delaying the Future approach and its practical implications for implementing standard objects such as registers.

Communication networks have become a critical infrastructure of our digital society. The resulting stringent reliability requirements however stand in stark contrast to today’s manual and error-prone approach to operate networks. In this talk, I will present opportunities for using formal methods to build highly dependable communication networks. In particular, we show how the policy-compliance of important network protocols can be verified in polynomial time, and explore synthesis approaches to efficiently generate and update network configurations. We will also discuss opportunities of AI/ML methodologies in this context.

Standard formal methods techniques apply to the verification of distributed algorithms only for a fixed number of finite-state processes. Parameterized verification aims at generalizing this to checking correctness for any number of processes, but typically assumes each process is finite-state. We address a more general setting, asynchronous round-based distributed algorithms, in which every process executes an unbounded sequence of asynchronous rounds and is therefore infinite-state. The resulting systems are unbounded in two dimensions: the number of processes and the number of rounds. Towards efficient verification of parameterized round-based distributed algorithms, we exhibit a series of reduction theorems, that collapses the unbounded round dimension into a single counter and reduces the parameterized verification problem to LTL model checking of a counter system. This enables the use of off-the-shelf state-of-the-art infinite-state model checkers such as NuXmv. We demonstrate the feasibility of our approach by verifying several round-based consensus and leader election algorithms. This is a joint worh with Pranav Ghorpade and Sasha Rubin.

Reasoning about consistency models for replicated objects is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches.

In this work, we introduce a fully automated approach to reasoning about consistency models for replicated objects. We explore the monadic second-order logic (MSO) representation of consistency properties, with the aim of extending the well-known MSO-to-automata translation to traces of executions.

Thus, this talk focuses on reducing MSO over execution traces to MSO over finite words, so as to match the input requirements of the MONA tool, which performs satisfiability in this setting by translating such formulas into automata.

Binding requires a distributed protocol to limit the possible outputs of processes, in a manner that is unknown to the processes themselves. Commitment fixes the output to a value that remains hidden from almost all processes. Both are hyperproperties since they consider possible extensions of a trace.

Specifying these properties is cumbersome, and arguing about them is even more so.

This talk explores how these properties can be captured by enforcing strong refinement of abstract modules that produce ghost outputs, which are not observed by the processes invoking the protocol implementing the module. We will discuss how ghost outputs may facilitate the composition and verification of such modules.

Examples will include binding crusader agreement and gather, random secret draw and verifiable secret sharing.