1.1 Distributed Systems Safety Verification

Distributed systems are sets of computing nodes that work together to act as one system. These systems are increasingly pervasive, complex, and critical. For example, some estimates suggest that over 75% of organizations across industries use some form of cloud computing and that cloud revenues could reach $2 trillion by 2030.^{2 3} These industries include everything from entertainment and banking to health and science, and are geographically distributed across the world. To meet this demand, software engineers are building globally distributed systems (which power cloud services) that coordinate with each other to provide users with strong performance, availability, and fault tolerance. For example, AWS uses 114 Availability Zones and over 700 edge locations to power their cloud services.

Unfortunately, these complex cloud systems are not immune to bugs. For example, in 2024, the three major cloud providers—Amazon, Google, and Microsoft—all experienced significant failures, including outages and customer data loss.^{4 5 6} These failures happen despite extensive engineering efforts. For example, Liu et al. (2019) find that fault and timing-related bugs account for 44% of production Microsoft Azure incidents despite these kinds of bugs being carefully tested for. More concerning still, these issues exist in designs, not just implementations. For example, Michael et al. (2017) find that three previously published distributed system designs suffer from “serious correctness violations.”

Much of the challenge of designing and implementing distributed systems stems from bugs that can arise from complex combinations of machine failures and message orderings. This complexity is difficult for humans to reason about manually (Gabrielson 2019). As distributed systems become increasingly critical infrastructure, engineers will need more computational support to build and deploy them correctly.

Automated reasoning engines promise to be the computational support that engineers need. These engines can solve tedious, mission-critical logic problems billions of times a day (e.g., Rungta (2022)). In the domain of distributed systems specifically, these tools have helped find bugs and prove the correctness of industrial systems (e.g., Newcombe et al. (2015)). Unfortunately, despite their power and flexibility, adoption of automated reasoning engines remains low for one fundamental reason. Today, successful users must be experts in their application domain and in automated reasoning—a rare combination. Specifically, users must be able to precisely describe their problem in a formal language, such as first-order logic, and know enough about automated reasoning to make sure their encoded problem is practically solvable.^{7 8 9}

This dissertation describes a stack of automated reasoning tools that help software engineers reason about their distributed systems. The stack reduces the need for automated reasoning expertise by allowing engineers to verify their systems in a modeling language they are already using (Chapter 5), providing one of the fastest solvers in the world for a relevant fragment of logic (Chapter 3), and partially automating the interaction with automated reasoning tools (Chapter 4, Chapter 6, and Chapter 7).

Our work follows a long tradition in formal methods that took an important pivot in Lynch and Tuttle (1987). Lynch and Tuttle introduced a new modeling formalism for distributed algorithms, I/O Automata, that accentuated the distinction between internal and external actions of system components. This distinction helps decompose systems and the reasoning about them, and did not exist in many earlier modeling languages, such as Communicating Sequential Processes (Hoare 1978) and the Calculus of Communicating Systems (Milner 1980). We provide a brief overview of I/O Automata in Chapter 2.5.

Work on I/O automata and similar modeling formalisms has continued for decades with an increasing emphasis on automation and executable code generation. For example, Garland and Lynch (2000) defined a formal language for describing and reasoning about I/O automata that interfaces to both a theorem prover and a model checker, and can generate code in a standard programming language. Around the same time, TLA+ and its extensions, which are still used today, provided similar functionality and interfaces (Lamport 2002). More recent works, such as Ivy (Kenneth L. McMillan and Padon 2020), have continued this tradition as well, incorporating more automation by encoding complex questions about models in a decidable fragment of logic.

Much of the work since the 80s has focused on two kinds of specifications: safety and liveness. Informally, safety properties state that nothing bad happens in a system; liveness properties state that something good will eventually happen. For example, for a leader election protocol, one might want to ensure the safety property that at most one leader is elected at any given time. It would be bad if two candidates were elected for one position. One might also want to ensure the liveness property that we will have a leader: it would be good for the election to conclude successfully. Leader election protocols are a class of consensus protocols where a set of nodes, each performing its local computation and communicating by sending and receiving messages, must agree on a specific value or result. Consensus protocols, in turn, are a class of distributed systems.

In distributed systems, like the consensus protocols described above, we often draw a distinction between synchronous and asynchronous. Informally, when messages are always sent and received within a known, fixed amount of time and nodes execute within a known, fixed relative speed, we call the system synchronous (Dwork, Lynch, and Stockmeyer 1988). When messages can take an arbitrarily long amount of time to deliver, or nodes execute at arbitrary relative speeds, we call the system asynchronous. Real-life systems are generally asynchronous. When we send a packet over the Internet, we do not have formal guarantees about the delivery time or whether the packet will be delivered at all. Unfortunately, this makes liveness properties difficult and often impossible to prove in the asynchronous setting. For example, Fischer, Lynch, and Paterson (1983) proved that distributed consensus is impossible even in the presence of just one faulty process.

The automated reasoning stack that we build, therefore, focuses on safety properties of fully asynchronous systems. As we will see throughout the dissertation, certain decisions will be tailored exclusively to this context while others will be more general. We pair the more general contributions with work that helps tailor them to our specific domain. This mix of general yet adaptable with highly domain-specific contributions enables us to resolve the central tension explored by the body of work contained in this dissertation. While it can be costly to create an entirely new approach for each new domain, we can develop general tools and techniques that can express problems across multiple domains and be tailored to specific domains. We must be general but adaptable so as to achieve usability and scalability.

1.2 Running Example and Thesis Overview

To better understand our domain and contributions, consider the following distributed system inspired by Le Lann (1977) and Chang and Roberts (1979), called the ring leader election protocol. The system consists of a set of nodes that work together to elect a leader. Each node has a unique, integer label value and the goal of the protocol is for the nodes to collectively discover the node with the greatest label. Nodes are arranged in a ring: each node can only receive messages from the node on its “left” and can only send messages to the node on its “right.” Nodes execute asynchronously and begin their execution by sending their label “right.” If a node receives a label greater than its own, it forwards the received label. If the received label is smaller, then the node sends its own label “right.” Finally, if the received label is equal, then the node declares itself the winner. Figure 1(A) depicts an instance of this system with three nodes and one of its executions: node 3 is to the right of node 2; 2 to the right of 1; 1 to the right of 3; and node 3 declares itself the winner after receiving its own label from node 2. Figure 1(B) depicts one possible safety specification for this system: at most one node should declare itself the winner of the election.

Given a distributed system model and a specification, such as the ring leader election protocol and the simple safety property described above, the goal of our work is to automatically decide if the model is guaranteed to satisfy the specification. The execution depicted in Figure 1(A) does satisfy the specification depicted in Figure 1(B) but, will all possible executions of the system do the same? Figure 1(G) depicts the response from the automated reasoning stack that we describe in this dissertation. The checkmark represents that the system does indeed satisfy the specification for all executions; the X mark represents that the attempted proof failed. Together, Figure 1(A), (B), and (C) depict the external interface to the automated reasoning stack. Interactions between users and the automated reasoning stack can be longer—Figure 11 depicts a more complicated example.

The next three subsections (Chapter 1.2.1, Chapter 1.2.2, and Chapter 1.2.3) give an overview of the automated reasoning stack itself—the right side of Figure 1. These three subsections cover Chapter 3, Chapter 4, Chapter 5, Chapter 6, and Chapter 7. In Chapter 2, we provide the necessary background on first-order logic to understand our work; we present a simple logical language, mar, that we use to ground our work, and we describe performance optimizations for checking mar programs related to proof caching and decomposition. We conclude this dissertation in Chapter 8 with plans for future work. Specifically, in Chapter 8.1, we present the problem of crossword construction as an example where automated reasoning can be useful but cannot exist on its own. We then briefly describe exciting future directions that combine automated reasoning engines with neural network-based tools.

1.3 Contributions

Overall, this dissertation presents novel integrations of artificial intelligence and formal methods at every level of the automated reasoning stack for scalable and usable domain-specific automated reasoning. We apply our work to distributed systems modeling and verification but aim to be an exemplar for how to build a full automated reasoning stack that targets any domain. In particular, we make the following contributions.

1. We create the P Verifier, a formal verification engine for the P programming language. Engineers already use P for modeling and testing their distributed systems. Existing verification engines for distributed systems do not provide users with language primitives or abstractions to support explicit message passing. To work at the message passing level—where a significant source of implementation errors lie—therefore usually has a cost: significant manual modelling and user effort. We introduce the idea of message chain invariants, seamlessly integrate them into the P Verifier, and show that, with message chain invariants, explicitly reasoning about message passing does not make verification more challenging. Specifically, message chain invariants give users the vocabulary to reason about the low-level details of explicit message passing while remaining at an intuitive level of abstraction. We demonstrate this empirically by replicating verification efforts from related work, simplifying these proofs using message chains, and then verifying a system with complex message passing—the onion routing network–and two industrial case studies.

2. We present a new specification mining toolkit that uses the structure provided by message chains to discover meaningful invariants for distributed system models. Our tools take execution data and infer specifications that likely hold for all executions. This reduces the burden on verification users by suggesting invariants that would otherwise require manual effort to discover and formalize. We extend a classic learning algorithm for non-erasing patterns, give a domain-specific definition of optimality, and prove that our algorithm correctly discovers the optimal specification using an NP oracle. We empirically evaluate our tools and find that six out of 24 invariants that were used in P Verifier proofs can be mined automatically in under a second each. Without the structure of message chains, the underlying learning algorithms cannot discover meaningful properties.

3. We present a new auto-formalization method that generates quality code in very low resource programming languages—like languages for verification—where existing work fails to even generate syntactically correct code. Auto-formalization methods take natural language text and return code in a formal language. Existing work focuses on prompting, constrained decoding, and fine-tuning strategies, which are unreliable, insufficiently expressive, or data hungry. We propose a complementary design-based solution. Specifically, we design an intermediate language that LMs are good at writing and can be compiled down to the target, low resource language. When LMs write code that is not exactly in the intermediate language, we use automated reasoning to identify the minimal error source and automatically repair the code at that source. We empirically evaluate our approach on a very low resource language in the verification domain, and show that we can substantially improve the syntactic correctness of generated code, producing code that passes all compiler checks 84.8% of the time compared to 9.1% by the best baselines.

4. We present one of the fastest SMT solvers in the world for queries over the theory of quantifier-free algebraic data types. Most existing solvers take a lazy approach. We define a new eager approach, prove that it is sound and complete, and demonstrate its empirical performance over three large benchmark sets. These results were independently validated at the 2024 SMT competition (Bromberger, Bobot, and Jonáš 2024), where our solver won the quantifier-free algebraic data type track.

5. SMT users typically solve more than one query at a time and that they do not need to solve the same query more than once. We present the first online learning-based solution for the problem of improving solver performance in this typical SMT setting. Existing work—like solver selection tools—can help by using expensive solver runtime data to optimize solver performance generally. We frame the problem as an online learning problem and combine multi-armed bandits with timeout prediction schemes to match, and sometimes exceed, the performance of existing work without any expensive pre-training.

2.1 Satisfiability Modulo Theories (SMT)

Boolean satisfiability (SAT) solvers have been shown to efficiently solve a number of NP-hard problems in areas such as AI planning (Kautz and Selman 1992), verification (Clarke et al. 2001), and software testing (Cadar et al. 2006). Satisfiability modulo theories (SMT) solvers are a natural extension of SAT solvers that reason about many-sorted first-order logic instead of just propositional logic. Specifically, SMT solvers can reason about first-order structures defined by background theories (Barrett et al. 2021), allowing them to tackle more general problems or to accept more succinct inputs. For example, SMT solvers can reason about bit-vectors (Brummayer and Biere 2009), floating-point numbers (Rümmer and Wahl 2010), strings (Bjørner et al. 2012), and algebraic data types (Barrett, Fontaine, and Tinelli 2017).

In this section, we provide a minimal reminder of concepts from many-sorted first-order and model theory that are required to understand what SMT solvers are. Many-sorted first-order logic is like first-order logic but with the universe partitioned into different sorts (Barrett et al. 2021). For a complete introduction, on first-order logic, we refer the reader to Lubarsky (2008). We focus on quantifier-free many-sorted first-order logic.

Symbols in many-sorted first-order logic are either logical or non-logical. Logical symbols include logical connectives, like disjunction (\(\lor\)), conjunction (\(\land\)), and negation (\(\neg\)). Non-logical symbols include predicate symbols and function symbols. Predicates and functions have an associated arity. In first-order logic, the arity is the number of arguments that the predicate or function takes. In our context, many-sorted first-order logic, the arity is more like a type signature: it defines the input sorts and the return sort. We treat predicates as functions whose return sort is Boolean: the set of predicates is a subset of the set of functions. When a function takes no arguments, we call it a constant. The set of non-logical symbols and their associated arity is given by a signature.

Expressions are formed from the symbols in a given signature. There are two kinds of expressions: terms and formulas. The set of terms is the smallest set such that every constant is a term and, if \(t_1, ..., t_n\) are terms and \(f\) is a function with appropriate arity, then \(f(t_1, ..., t_n)\) is a term. The set of formulas is the smallest set such that

1. every constant predicate is a formula;
2. if \(t_1, ..., t_n\) are terms and \(p\) is a predicate with appropriate arity, then \(p(t_1, ..., t_n)\) is a formula;
3. if \(\phi\) is a formula, then \(\neg \phi\) is a formula; and
4. if \(\phi_1\) and \(\phi_2\) are formulae, then \(\phi_1 \lor \phi_2\), \(\phi_1 \land \phi_2\), and so on are formulas.

A theory literal is a predicate application or its negation. These are the base units of SMT solving and are the equivalent of literals in SAT solving. A clause is a disjunction of theory literals. A cube is a conjunction of theory literals. A formula is in conjunctive normal form (CNF) iff it is a conjunction of clauses. A formula is in disjunctive normal form (DNF) iff it is a disjunction of cubes. A formula is in negation normal form (NNF) if only theory literals are negated. A formula is flat if all theory literals are of the form \(\neg (t_1 = t_2)\), \(t_1 = t_2\), or \(t_1 = g(t_2, ..., t_n)\) where \(t_i\) are constants.

A first-order theory is a set of formulas (axioms). For example the theory of Equality and Uninterpreted Functions (UF) consists of axioms that restrict the possible interpretations of \(=\) (reflexivity, symmetry, transitivity) and all function symbols (congruence) (Burch and Dill 1994). A structure is a many-sorted universe along with a function that describes how all non-logical symbols must be interpreted over the many-sorted universe. We extend the notion of interpretation to terms and formulas inductively, as expected. When a formula \(\phi\) is interpreted as true in a structure \(\mathcal{M}\), we say that \(\mathcal{M}\) satisfies \(\phi\), denoted \(\mathcal{M} \models \phi\), and we call \(\mathcal{M}\) a model of \(\phi\). As a slight abuse of notation, for a set of formulas \(\Phi = \{\phi_i\}\), we use \(\mathcal{M} \models \Phi\) to mean \(\mathcal{M} \models \bigwedge_1^n \phi_i\). Similarly, we use \(\phi \models \psi\) to mean every model of \(\phi\) is a model of \(\psi\). For a model \(\mathcal{M}\), we use \(\mathcal{M}[f]\) to represent the interpretation of \(f\) in \(\mathcal{M}\).

An SMT solver \(S\) is sound for a theory \(T\) if, for every formula \(\phi\), \(S(\phi, T) = \text{SAT}\) implies that the query (\(\phi, T\)) is SAT. An SMT solver is complete for a theory \(T\) if, for every formula \(\phi\), the query (\(\phi, T\)) is SAT implies that \(S(\phi, T) = \text{SAT}\). The distinctive aspect of SMT solvers is that they perform an encoding to SAT, either implicitly or explicitly. Eager SMT solvers perform a satisfiability-preserving reduction to SAT in a single phase (e.g., see Seshia (2005)) whereas lazy solvers perform an iterative encoding, on demand.

In Chapter 3, we use the following definition to build a sound and complete solver for the quantifier-free theory of algebraic data types using a sound and complete solver for the theory of uninterpreted functions and equality.

In Chapter 7, we use an optimization variant of SMT solvers, called weighted maximum satisfiability modulo theories solvers (MAX-SMT solvers).

2.2 Algebraic Data Types

Algebraic data types (ADTs) are a representation of finite trees that are common in functional programming languages. The power behind ADTs lies in how they can succinctly express complex structures at a high-level of abstraction while avoiding common programming pitfalls, like null pointer dereferencing (Hoare 1975). For most of their history, ADTs lived exclusively inside functional programming languages, like NPL (Burstall 1977), Standard ML (Milner 1997), and Haskell (Hudak et al. 2007). Recently, however, the interest in ADTs has exploded with a number of mainstream languages being released with support for ADTs, e.g., Rust (Jung et al. 2021), or have added support, e.g., Python¹⁰ and Java.¹¹

An algebraic data type consists of a set of constructors (node names), selectors (directed edge names), and testers (predicates). Each constructor has a fixed set of selectors associated with it (possible edges out). Each selector has an associated type (each edge can only point to a fixed set of node names). Every constructor is associated with exactly one unique tester: that tester returns true on a given tree iff the root of the tree is labeled with the corresponding constructor. Every instance of an algebraic data types (a particular finite tree built from those node and edge names) must be acyclic.

We denote the theory of algebraic data types as DT. It contains the full theory of UF along with the following additional axioms.

An algebraic data type term is any expression of an algebraic data type sort. The set of normal algebraic data type terms is the smallest set containing 1. constants (0-ary constructors), 2. constructors applied to only normal algebraic data type terms. It is useful to think of normal terms as trees: constants are leaves and we can build larger trees by applying constructors to normal terms.

In Chapter 3.2 we define an algebraic data type called tower. The definition of tower uses two constructors: Empty and Stack. These are the two possible ways to build a tower. Empty is a function that takes no inputs and outputs a tower. Stack is a function that takes a block (another simple algebraic data type) and a tower and outputs a tower. Each corresponding constructor has a set of selectors. Empty has no selectors and so it is a normal term, but Stack has two selectors, top and rest. We often apply selectors using dot notation, e.g., x.top. Selectors can be thought of as de-constructors—we use them to get back the terms constructed a tower. The tower definition implicitly defines two testers: is Empty and is Stack These predicates take a tower and return true iff the argument was built using the matching constructor. In mar syntax, which we describe in Chapter 2.3, tower is defined as follows.

data block = A() | B()
data tower =
  | Empty ()
  | Stack (top: block, rest: tower)

We deviate from the SMT-LIB standard slightly in the vocabulary we use related to algebraic data types. The following clarifies the connection. If a sort \(t\) has a non-empty set of constructors, then we call \(t\) an algebraic data type. If \(t\) has a single constructor \(c\) and every selector \(s\) of \(c\) is such that it is not the case that \(t\) appears in the sort of \(s\), then we call \(t\) a record. When \(t\) is a record with constructor \(c\), we call every selector \(s\) of \(c\) a field of \(t\). If \(t\) is an algebraic data type and every constructor of \(t\) has no associated selectors, then we call \(t\) an enum. When \(t\) is an enum, we call every constructor of \(t\) a variant of \(t\) and often treat the enum as a set.

2.3 Modeling and Automated Reasoning Language

The modeling and automated reasoning language (mar) is a simple functional programming language that supports satisfiability testing, algebraic data types, and simple function contracts.¹² We use mar as an intermediate language: it is easy to translate to SMT-LIB 2.6—the standard input language for most modern SMT solvers—and it introduces just enough of an abstraction to express the contents of this dissertation. mar as the smallest version of UCLID5 needed to understand the contributions of this dissertation.

d ::= data r n1 ... nn = | C1 (s11: t11, ..., s1l: t1k) 
                         | ... 
                         | Cm (sm1: tm1, ..., sml: tml)

d ::= type n = t

t ::= bool
t ::= a

b ::= let f (x1: t1, ..., xn: tn) -> (y: t) = e
b ::= let f (x1: t1, ..., xn: tn) -> (y: t)

a ::= f requires e1
a ::= f ensures e2

e ::= true
e ::= false
e ::= x
e ::= e1 is C
e ::= e1.s
e ::= e1 == e2
e ::= e1 != e2
e ::= not e
e ::= e1 and e2
e ::= e1 or e2
e ::= e1 ==> e2
e ::= if e1 then e2 else e3
e ::= f(e1, ..., en)
e ::= C(e1, ..., en)
e ::= match e1 with | C1(x1 ... xn) -> e2 
                    | ... 
                    | Cm(x1 ... xn) -> em

c ::= assert e
c ::= print e

p ::= d p
p ::= b p
p ::= a p
p ::= c p
p ::= c

data natural = Z() | S(p: natural)
data option-natural = None() | Some(value: natural)

let get-natural (x: option-natural) -> (y: natural) = 
    match x with
    | Some(n) -> S(n)
    | None() -> Z()

print get-natural(Some(S(S(Z())).p))

get-natural requires x-is-some: x is Some
get-natural ensures y-is-s: not y is Z

2.4 Advanced Solver Interface

The semantics of mar programs as described above is sufficient for understanding the contributions of this dissertation. In this section, we shift our focus to more practical considerations related to writing and reasoning about mar programs. These contributions are yet to be published but an essential part of making automated reasoning usable and scalable. Specifically, in this section, we introduce proof commands and give more detailed semantics, including a new label, “unknown.”

In general, writing mar programs is not a one-shot process. Users refine their models and specifications repeatedly, and they make frequent calls to solvers under the hood as they go. In Chapter 4 we described how to automatically learn to pick the best solver over sequences of queries, like those that we would expect to see from a typical mar user. This is a form of adaptability. In this chapter, we describe a mar backend strategy that gives users two more desired features: non-repetition and progress.

Non-repetition refers to a backend that avoids calling a solver to perform the same reasoning multiple times. Progress refers to a backend that avoids redefining previously settled reasoning questions. To better understand the features and the distinction between them, consider the following mar program.

data natural = Z() | S(p: natural)

let subtract-two (x: natural) -> natural = x.p.p
let add-three (x: natural) -> natural = S(S(S(x)))

The program declares a data type that represents natural numbers, natural, and two functions that act on natural numbers, subtract-two and add-three. These functions use selectors and constructors. Since selectors can lead to undefined behavior—selecting p from Z() can result in any value—we likely want to require that subtract-two is never called with an input value of less than two. The following code snippet enforces this precondition.

subtract-two requires x-is-gte-2: x is S and x.p is S

Every time we use subtract-two in the code, the backend must check that the precondition holds. For example, if we declare an uninterpreted function a of type natural and then print subtract-two(add-three(a)), then the backend must check that add-three(a) is greater than or equal to two. Without any postconditions on add-three, the solver will not be able to prove that the precondition on subtract-two holds for that call. The simplest possible postcondition that we can add says that the result of an application add-three is greater than or equal to two. The following snippet captures this constraint.

add-three ensures y-is-gte-2: add-three(x) is S and 
                              add-three(x).p is S

Running mar will result in a successful proof that the precondition x-is-gte-2 is satisfied for the function application in the print statement. If we run the backend again on this same input, we should not need to check this fact again. This is the simplest form of non-repetition. This version of non-repetition can be achieved by caching queries.

Now suppose that we add the assertion subtract-two(add-three(a)) is Z. One might expect this assertion to block all models and therefore that printing subtract-two(add-three(a)) should fail. But, in the composed semantics, the backend must only consider the function contracts, and therefore the print statement should actually display Z(). To get the response that we might expect when considering the body of the add-three function, we need a different postcondition. Specifically, we can add the following postcondition.

add-three ensures y-is-gte-3: add-three(x) is S and 
                              add-three(x).p is S and 
                              add-three(x).p.p is S

For the composed semantics, this new postcondition will allow the backend to conclude UNSAT, and the print statement will fail, as expected. Unfortunately, this will also result in a new query for the contract semantics. We already proved that the precondition x-is-gte-2 will hold for the call subtract-two(add-three(a)) using the postcondition y-is-gte-2. But now, the naive backend would have to re-prove this fact with a larger query: the new query would contain both y-is-gte-2 and y-is-gte-3. In many realistic cases—programs that are more complex than this toy example—adding constraints on previously solved queries can make the solver timeout. If adding y-is-gte-3 caused the solver to timeout, then our edits to the mar program would have actually set back our proof efforts. Guaranteeing that this cannot happen (for a class of updates) is a form of progress.

Non-repetition and progress are similar. Providing progress opens up opportunities for non-repetition: if we can avoid changing backend checks, then we will get more cache hits. The opposite can also be true. More fine-grained caching, like through saving UNSAT cores, can automatically guarantee some progress—adding irrelevant facts will not lead to a new solver call. Another form of progress comes from building on previously proved facts. For example, if we have previously proven y-is-gte-3, then we can easily prove y-is-gte-2 without even looking at the body of add-three. For more complicated functions and properties, building on previously proven facts can lead to speedups over the entire verification effort.

// ----- Program -----
data natural = Z() | S(p: natural)

let subtract-two (x: natural) -> natural = x.p.p
let add-three (x: natural) -> natural = S(S(S(x)))

let a: natural

print subtract-two(add-three(a))
assert subtract-two(add-three(a)) is Z

// ----- Contracts -----
subtract-two requires x-is-gte-2: x is S and x.p is S
subtract-two ensures y-is-0-if-2: subtract-two(x) is Z 
                                    ==> x == S(S(Z()))

add-three ensures y-is-gte-2: add-three(x) is S and 
                              add-three(x).p is S
add-three ensures y-is-gte-3: add-three(x) is S and 
                              add-three(x).p is S and 
                              add-three(x).p.p is S

// ----- Proofs -----
prove y-is-0-if-2 using x-is-gte-2
prove x-is-gte-2  using y-is-gte-2
prove y-is-gte-2
prove y-is-gte-3

data natural = Z() | S(p: natural)

let subtract-two (x: natural) -> natural = x.p.p
let add-three (x: natural) -> natural = S(S(S(x)))

let a: natural

print subtract-two(add-three(a))
assert subtract-two(add-three(a)) is Z

subtract-two requires x-is-gte-2: x is S and x.p is S
subtract-two ensures y-is-0-if-2: subtract-two(x) is Z 
                                    ==> x == S(S(Z()))
add-three ensures y-is-gte-2: add-three(x) is S and 
                              add-three(x).p is S

prove y-is-0-if-2 using x-is-gte-2
prove x-is-gte-2  using y-is-gte-2

Z()

☒ y-is-0-if-2
☐ y-is-gte-2
☑ x-is-gte-2 

2.5 I/O Automata

In this section, we give the necessary background on I/O automata and provide a basic encoding of I/O automata into the mar language. We present a version of I/O automata (Lynch 1996) tailored to our context along with examples focused on our encoding described in Chapter 5. Let \(\textit{states}\) and \(\textit{actions}\) be disjoint sets. An I/O automaton \(A\) is a six-tuple \[(\textit{inp}(A), \textit{int}(A), \textit{out}(A), \textit{states}(A), \textit{start}(A), \textit{trans}(A)),\] where \(\textit{inp}(A)\) (input actions), \(\textit{int}(A)\) (internal actions), and \(\textit{out}(A)\) (output actions) are disjoint subsets of \(\textit{actions}\), \(\textit{states}(A)\) is a subset of \(\textit{states}\), \(\textit{start}(A)\) is a subset of \(\textit{states}(A)\), and \(\textit{trans}(A)\) is a transition relation over state-action-state triples. Specifically, \(\textit{trans}(A)\) is a relation on \[\textit{states}(A) \times \textit{inp}(A) \cup \textit{int}(A) \cup \textit{out}(A) \times \textit{states}(A).\] We call individual triples \((s,a,s')\) in \(\textit{trans}(A)\) steps of \(A\). Like Lynch, we require I/O automata to be input-enabled. That is, we require that for every state \(s\) and action \(\alpha \in \textit{inp}(A)\) there exists a state \(s'\) such that \((s, \alpha, s') \in \textit{trans}(A)\).

We often define transition relations piecemeal through precondition-effect pairs.

For example, the simple universal buffer (\(\textit{SUB}\)) has a precondition-effect pair with precondition \(p(s, \textit{get(v)}_{i, j}) \triangleq v \in s\) and effect \(e(s, \textit{get(v)}_{i, j}) \triangleq s \smallsetminus v\). This precondition asserts that \(v\) must be in the set (we cannot get an element which is not present), and this effect removes \(v\) from the set \(s\).

For example, the sequence \(\emptyset,\textit{put(7)}_{i, j},\{7\},\textit{get(7)}_{i, j},\emptyset\) is an execution of \(\textit{SUB}\) from Example 1. On the other hand, the sequence \(\emptyset,\textit{get(7)}_{i, j},\emptyset\) is not an execution of \(\textit{SUB}\).

For example, consider \(\textit{SM}_1 \cdot \textit{SUB}\) from Example 2 and the invariant assertion which states that every element in the set maintained by the \(\textit{SUB}\) component is greater than zero. That is, the invariant is \(p([ s_{\textit{SM}_1}, s_{\textit{SUB}} ]) \triangleq \forall_{i \in s_{\textit{SUB}}} \, i > 0\). A counterexample to induction for this I/O automaton and invariant is the step \(([ -1, \{\} ], \textit{put}_0, [ -1, \{0\} ])\). Note that the pre-state \([ -1, \{\} ]\) is not reachable and that the invariant does indeed always hold. Nevertheless, the proof by induction fails.

data natural = Zero () | Successor (n: natural)
data action = Put (p: natural) | Get (g: natural)
data state = Empty () | Full (current: natural) | Error ()

let start (s: state) -> bool =
  match s with
    | Empty() -> true
    | Full(_) -> false
    | Error() -> false

let trans (s: state, a: action, s': state) -> bool =
    match a with
        | Put(p) ->
          (match s with
            | Empty() -> s' == Full(p)
            | Full(_) -> s' == Full(p)
            | Error() -> s' == Error())
        | Get(g) ->
          (match s with
            | Empty() -> s' == Error()
            | Full(current) ->
                (if current == g then
                    s' == Empty()
                else
                    s' == Error())
            | Error() -> s' == Error())

let s1: state
let s2: state
let s3: state
assert start(s1)
assert trans(s1, Put(Zero()), s2)
assert trans(s2, Get(Successor(Zero())), s3)

print(s1) // will print "Empty()"
print(s2) // will print "Full(Zero())"
print(s3) // will print "Error()"

start ensures start-means-empty: start(s) ==> s is Empty
trans requires not-error: trans(s, a, s') ==> not s is Error
trans ensures correct-action: trans(s, a, s') and 
                              (a is Put) ==> s' == Full(a.p)
trans ensures correct-get: trans(s, a, s') and 
                           (a is Get) and 
                           (s is Full) and 
                           (a.g != s.current) ==> s' is Error

3.1 Introduction

Automated reasoning about algebraic data types is important beyond distributed systems because this construct appears in many different software applications. As the popularity of algebraic data types grows, the demand for efficient SMT solvers will continue to increase. Unfortunately, the state-of-the-art tools in this space are already struggling to keep up. We demonstrate this empirically by generating a new benchmark set and showing that existing solvers, working together, are only able to solve 56.2% of the new queries in under 20 minutes per query (Chapter 3.5.2).

This imbalance between programming languages and SMT solvers is manifest as a gap in the SMT-solving literature. Oppen (1978) was the first to provide a decision procedure for the quantifier-free theory, but algebraic data types do not seem to have permeated the community much further. In 2003, a concerted effort to unify the SMT community began with the first official input standard and competition, called SMT-LIB and SMT-COMP (Barrett et al. 2011), respectively. Algebraic data types were not officially integrated into the standard until 2017 as part of version 2.6 (Barrett, Fontaine, and Tinelli 2017). In the 2023 iteration of SMT-COMP (the iteration before the work we describe in this chapter), only two solvers participated in the algebraic data type track, the least of any track. Both solvers use a variation of the same solving approach: a lazy SMT architecture combined with theory-specific reasoning based on the work by Oppen from 1978 (see Chapter 3.3).

In this chapter, we propose a new solving technique that departs from the standard approach. Instead of a lazy approach, we take an eager approach (Barrett et al. 2021) that translates the original SMT formula into an equi-satisfiable formula without algebraic data types. Our work fills the gap in the literature on SMT solving for algebraic data type queries and, by doing so, solves more queries than existing solvers (see Chapter 3.5.1). More importantly, we make the largest empirical contribution to the solving community on SMT-COMP benchmarks, solving different queries than existing tools (see Chapter 3.5.2).

The rest of this chapter is organized as follows. In Chapter 3.2, we describe algebraic data types, satisfiability, and our approach through an example planning problem called blocks world. In Chapter 3.3, we survey related work. In Chapter 3.4, we describe our eager reduction from algebraic data type queries to queries containing only uninterpreted functions (UF). Chapter 3.4 includes a proof of soundness and completeness, along with a complexity analysis. In Chapter 3.5, we describe a prototype implementation of our approach, called Algaroba, and we evaluate it over two research questions. We find that Algaroba outperforms the state of the art overall and in terms of contribution to the solving community. Chapter 3.5 also describes a new benchmark set consisting of blocks world queries. This set addresses an important gap in the existing literature: the queries in this set contain all important kinds of algebraic data types but are not easy to solve. Overall, we make the following contributions.

1. We define a notion of query depth and a finite, quantifier-free reduction from algebraic data type queries to UF queries that uses depths. This is a new eager solving approach.

2. We prove the soundness and completeness of our approach and show that it generates at most a finite number of assertions.

3. We generate a new benchmark set that contains all kinds of algebraic data types and is not trivial to solve. Existing benchmarks do not enjoy both these properties.

4. We implement our reduction approach in a prototype tool called Algaroba and we compare its performance to the state of the art. Algaroba outperforms existing tools and that it makes the largest empirical contribution to the community of solvers.

3.2 Running Example: Blocks World

To better understand algebraic data types, satisfiability queries, our approach, and the benchmark set that we generate in Chapter 3.5, consider the classic blocks world problem first proposed by Winograd (1971). We use a version of the problem that Sussman (1973) used to illustrate the Sussman anomaly (Russell 2010) and that Gupta and Nau (1992) used to show that the associated decision problem is NP-Hard.

In the simplified version of the blocks world problem, there is a table with (possibly empty) stacks of blocks on it (an initial configuration), a desired way that the stacks should be arranged (a target configuration), and three rules:

1. blocks can only be taken from the top of a stack;
2. blocks can only be placed on the top of a stack; and
3. only one block can be moved at a time.

The general problem is to find a sequence of legal moves that leads from the initial configuration to the target configuration. The associated decision problem is to determine if there is such a sequence of length less than some input \(k\).

Figure 3 shows an example blocks world solution. The initial configuration is given in Figure 3 (a), the target configuration in Figure 3 (e), and Figs. Figure 3 (b), Figure 3 (c), and Figure 3 (d) show a sequence of three legal moves that solve the problem, where faded blocks denote the previous position of the block moved at that step.

The blocks world problem is a useful illustrative example for an algebraic data types solver because the encoding uses sum, product, and inductive algebraic data types. The following mar code gives the required type definitions for the example in Figure 3.

data block = A() | B()
data tower =
  | Empty ()
  | Stack (top: block, rest: tower)
data config =
  | table (left: tower, center: tower, right: tower)

Specifically, this code defines an enumerated type for blocks (block at line 1), a record type for table configurations (config at lines 5-6), and an inductive type for stacks (tower at lines 2-4). Terms of an enumerated type can take on any of the values listed in the type definition. For example, terms of type block can take on the values A or B. Terms of a record type can take on any combination of values of the type arguments listed in the type definition. For example, terms of type config can take on a triple of any three tower values. Enumerated types are the simplest form of a sum type, while records are the simplest form of a product type. Algebraic data types allow for definitions that are both sum and product types. For example, terms of type tower can either be Empty or they can be a Stack but not both (sum). When these terms take on a Stack value, they are a pair of block and tower values (product). Notice that the definition of tower depends on itself, this makes it an inductive type.

The blocks world problem is a useful illustrative example for satisfiability queries for two reasons. First, satisfiability-based solutions for similar planning problems have been around for decades (Kautz and Selman 1992). Second, encoding the problem as a satisfiability problem is simple when using bounded model checking (Biere et al. 1999) for bounded-horizon planning (e.g., see Rintanen (2003)). Specifically, the bounded model checking-based encoding is given by a transition system and a specification. The transition system starts at the initial configuration, and, at each step, makes a non-deterministic choice of which legal move to make. The specification is that the transition system never reaches the target configuration. Given this transition system, specification, and a bound \(k\), bounded model checking will generate a satisfiability query whose solutions are assignments to the non-deterministic choices—concrete choices that get us to the target configuration from the initial configuration in less than \(k\) steps. SMT solvers, like our new solver, generate these solutions or prove that none exist. We use this encoding in Chapter 3.5 to generate a new benchmark set.

The blocks world problem also gives a useful intuition for our approach. While terms of inductive data types, like tower, can take on arbitrarily large values (e.g., a stack of a million A blocks), there is a bound on the size of relevant values. For the blocks world problem in Figure 3 it would never make sense to have a tower value of size greater than two. Such a bound exists for all quantifier-free algebraic data type queries; the problem is that automatically inferring the bound and using it to speed up solving was non-trivial. In this chapter, we give an automated procedure for computing an over-approximation of this bound, and then we use this over-approximation to replace algebraic data type functions with uninterpreted functions along with a finite number of quantifier-free axioms.

You can think of the blocks world problem in terms of distributed systems—it shares all the characteristics of the systems we will work with in Chapter 5. Specifically, each table position is a node in the system. Each node keeps track of its own tower and can move its top most block to another node by sending that other node a message. Assuming that the choice of target node is non-deterministic, solving the blocks world problem is exactly the task of verifying that the distributed system never reaches the target configuration. The subsequent code block is an encoding of the blocks world problem from Figure 3 as a mar program following the encoding of I/O Automata in Chapter 2.5.1. We use bounded model checking for three steps and omit the definition of trans and its contracts for brevity.

data block = A () | B ()

data tower =
  | Empty ()
  | Stack (top: block, rest: tower)

data config =
  | table (left: tower, center: tower, right: tower)

data action = 
  | Left-to-Center () 
  | Left-to-Right () 
  | Center-to-Left () 
  | Center-to-Right () 
  | Right-to-Center () 
  | Right-to-Left ()

let trans (before: config, a: action, after: config) -> bool 

// ... OMITTED ...

let start: config = table(Stack(B(),Stack(A(), Empty())), 
                          Empty(), 
                          Empty())

let goal: config = table(Empty(), 
                         Empty(), 
                         Stack(B(),Stack(A(), Empty())))

let c0: config
let c1: config
let c2: config
let c3: config

let a0: action
let a1: action
let a2: action

assert(c0 == start)
assert(trans(c0, a0, c1))
assert(trans(c1, a1, c2))
assert(trans(c2, a2, c3))
assert(c3 == goal)

print(c0) // table(Stack(B, Stack(A, Empty)), Empty, Empty)
print(a0) // Left-to-Center
print(c1) // table(Stack(A, Empty), Stack(B, Empty), Empty)
print(a1) // Left-to-Right
print(c2) // table(Empty, Stack(B, Empty), Stack(A, Empty))
print(a2) // Center-to-Right
print(c3) // table(Empty, Empty, Stack(B, Stack(A, Empty)))

3.3 Related Work

Most solvers for quantifier-free algebraic data type queries use a lazy SMT architecture, i.e., they use a theory specific solver to handle the data types and a core solver to handle the logical formula (Sebastiani 2007). A common theory solver will use a combination of congruence closure, syntactic unification, and acyclicality checks (Barrett, Shikanian, and Tinelli 2006; Oppen 1978; Reynolds and Blanchette 2017; Reynolds et al. 2018). This is the case for popular SMT solvers like cvc5 (Barbosa et al. 2022), SMTInterpol (Christ, Hoenicke, and Nutz 2012), and Z3 (de Moura and Bjørner 2008). cvc5 and SMTInterpol were the only two participants in the 2023 edition of SMT-COMP for quantifier-free algebraic data type queries. We differ in that we take an eager approach.

Princess (Hojjat and Rümmer 2017) also takes an eager approach. However, Princess reduces queries to UF and Linear Integer Arithmetic (LIA). LIA makes keeping track of the depth of algebraic data type terms easy, but their reduction results in queries that are more difficult to solve (see Chapter 3.5). Bonacina and Echenim (2007) provide a similar reduction but not an efficient implementation.

The scope of our work is quantifier-free algebraic data type queries. However, there is existing related work that deals with quantifiers. De Angelis et al. (2020) and Kostyukov, Mordvinov, and Fedyukovich (2021) provide approaches to solving algebraic data type Constrained Horn Clauses (CHCs). Other approaches (Suter, Dotta, and Kuncak 2010; Pham and Whalen 2013) support restricted forms of recursive functions (called catamorphisms) via partially evaluating these functions. Kovács, Robillard, and Voronkov (2017) provide two decision procedures for quantified algebraic data types.

3.4 Approach: Eager Reduction

We propose a new SMT solver for the DT theory defined in Chapter 2.2. For a quantifier-free input formula p, our solver generates a quantifier-free formula q in UF and then calls an existing UF solver to get a final result. We cannot compute a quantifier-free reduction directly, since DT axioms have universal quantifiers. Instead, we only instantiate the DT axioms over terms that are relevant to the input query.

p1          = NNF(p)
p2          = Flatten(p1)
k           = Number of algebraic data type constants in p2
p3          = Apply rewrite rules A and B to p2
q1, ..., qm = Apply axioms 1, 2, and 3 using k to p3
q           = p3 and q1 and ... and qm
return UF_SMT_Solver(q)

When the universe of the input query is finite (e.g., it only contains enums), we instantiate the entire universe (see Chapter 3.4.1). Otherwise, we follow the procedure in Listing 1. This procedure transforms the input query to NNF, flattens the result, and then applies the rewrite rules in Listing 2 and adds the axioms Listing 3. The depth of a query is the number of constants in the flattened NNF version of the query. In Listing 1, the depth is k. The depth is linear in the size of the input query because the NNF and flattening transformations introduce at most a linear number of constants.

Rules A and B from Listing 2 correspond to rewriting constructor and selector applications respectively so that they work well with other constructor, selectors and testers. Rule B contains existential quantifiers, but these are handled through skolemization (replacing existentially bound variables by fresh constants). Axioms 1 and 2 from Listing 3 ensure that only one tester returns true for each term, and that this tester corresponds to a constant iff the term is a constant. Axiom 3 encodes the acyclicality constraint.

To better understand Axiom 3 and acyclicality, consider the following example query.

data block = A() | B()
data tower =
  | Empty ()
  | Stack (top: block, rest: tower)

let x: tower
let y: tower

assert (x is Stack) and 
       (y is Stack) and 
       (y == x.rest) and 
       (x == y.rest)

This query is UNSAT because any satisfying assignment would need to violate acyclicality. Therefore, to avoid spurious models, we must encode the acyclicality property in our reduction. The challenge is that we need to capture this seemingly infinite property using only finite number of quantifier-free formulas.

Our key result is that we only need to enforce acyclicality for all \(l<k^\text{th}\) descendants, where k is the number of algebraic data type constants in the flattened query. To see the intuition behind this, consider the following generalization of the previous example, where x1, …, xk-1, xk are of type tower.

assert (x1 is Stack) and ... and (xk is Stack) and 
       (x2 = x1.rest) and (x3 = x2.rest) and ... and
       (xk = xk−1.rest) and (x1 = xk.rest)

This query asserts that there is a cycle of size k. Since, our reduction asserts acyclicality for all \(l<k^\text{th}\) descendants, we correctly return unsat on this query. Furthermore, it is impossible to have a query with a cycle of size more than k using k or fewer constants (in the flat query), so our encoding is sufficient (see Chapter 3.4.3 for a full proof).

(A) f(a1, ..., am) == t
    → (t is f and 
          f(a1, ..., am) == t and t.s1 == a1 and ... and t.sm == am)

(B) t.sj == tj
    → (t.sj == tj 
        and (t is f ==> (exists (a1, ..., am) 
          f(a1, ..., am) == t and t.si == a1 and ... and t.sm == am)))

(1) (t is f1 or ... or t is fn) and at-most-one(t is f1, ..., t is fn)

(2) For every zero-ary f, (t is f) == (f == t)

(3) If s is the lth descendant of t and l < k, s != t

data enum = A() | B() 
data rec1 = j (x: enum, y: enum)
data rec2 = k (z: rec1, w: rec1)

data tree =
  | Leaf ()
  | Node (left: tree, right: tree)

3.5 Empirical Evaluation

In this section we empirically compare the performance of our approach to state-of-the-art solvers. Specifically, we aim to answer the following research questions.

1. How does the overall performance of our approach compare to the state of the art?
2. How complementary is the performance of our approach to that of existing solvers?

We implement a prototype of our approach, called Algaroba, in approximately 2900 lines of OCaml code.¹³ We use the Z3 API as the default UF back-end solver but we allow for any UF solver to be used instead. Algaroba takes inputs in the SMT-LIB language and includes a number of simple optimizations, like hash-consing (Ershov 1958), incremental solving, and theory-specific query simplifications. All experiments are conducted on an Ubuntu workstation with nine Intel(R) Core(TM) i9-9900X CPUs running at 3.50 GHz and with 62 GB of RAM. All solvers were given a 1200 second timeout on each query to be consistent with SMT-COMP. The state-of-the-art solvers in this space are cvc5 (we use version 1.0.6-dev.214.97a64fc16) and Z3 (we use version 4.12.2). We also include Princess (latest release as of 2023-06-19) in our evaluation since it is the most related approach. We describe all three solvers in Chapter 3.3.

Our evaluation covers two existing benchmark sets from SMT-COMP, one originally from Bouvier (2021) and one originally from Barrett, Shikanian, and Tinelli (2006) (BST for short). These two benchmark sets are useful but limited: every solver succeeds on every BST query so it is difficult to draw performance conclusions; Bouvier queries are more challenging but only contain sum types.

To address these limitations, we introduce a new benchmark set consisting of randomly generated blocks world queries. Blocks world queries, which we describe in Chapter 3.2, are more challenging to solve than those in BST and, unlike those from Bouvier, contain sum, product, and inductive types. To generate blocks world queries we use the same table configuration as in Chapter 3.2 (three places for towers), but we randomly select a set of blocks (ranging between two to 26) and we randomly generate an initial and target configuration (two sets of three random block towers). We call these three random samples a blocks world setup. For each blocks world setup, we randomly sample a set of step numbers (ranging from one to two times the number of blocks) and generate a blocks world query for each step number. This process resulted in 500 individual queries that each ask “can we get from this initial configuration to this target configuration in exactly this number of steps?”

3.5.2 RQ2: Contribution Rank

Measuring overall performance is useful but it does not give an accurate perspective on how the community uses these tools. When faced with an SMT query, practitioners are likely to use multiple different solvers. This could be in parallel, like Rungta (2022), or through algorithm selection, like Pimpalkhare et al. (2021). Contribution ranks capture this practical perspective by evaluating solvers in terms of how complementary they are to other solvers. A higher rank means a higher contribution to the community of solvers.

To evaluate how complementary our approach is to existing solvers, we use SMT-COMP’s contribution ranking. This ranking uses the notion of a virtual best solver, which is defined as \(vb(q, S) \triangleq s(q)\), where \(S\) is a set of solvers and \(s\) is the solver in \(S\) that terminates most quickly on \(q\). Informally, the ranking answers, “which solver can I remove from the virtual best solver to hurt performance the most?”

In terms of number of queries solved (the primary SMT-COMP metric), there is a four-way tie on the BST benchmark set—all solvers solve all queries. For both other benchmark sets, Algaroba is ranked highest. For blocks world, the virtual best solver without Algaroba succeeds on 56.2% of the queries, less than Algaroba on its own (61.4%). With Algaroba, the virtual best solver succeeds on 62.2%. For Bouvier, without Algaroba, the virtual best solver succeeds on 64.25% of the queries. With Algaroba, this number rises to 83.75%. These positive results are in part because Algaroba solves the most queries, but are mainly due to the uniqueness of our approach. cvc5 and Z3 use a similar underlying algorithm, so removing one does not affect the performance of the virtual best solver. On the other hand, while Princess is the most similar approach to our own, their reduction is different enough to not interfere with our ranking.

Figure 5 shows this same data as a stacked histogram: each colored bar represents the number of queries that are uniquely solved (y-axis) by each solver (x-axis) over the given benchmark set (color and hash-style). In short, we solve many queries that no other solver can (108/900). Given the winning contribution rank of Algaroba on both interesting benchmark sets, and the dominant number of uniquely solved queries, we answer RQ2 by concluding that our performance is complementary to existing solvers—we solve many benchmarks that no other solver can.

3.6 Conclusion

In this chapter, we described the arrow from Figure 1(E) to Figure 1(F): an SMT solver for the quantifier-free theory of algebraic data types called Algaroba. Algaroba takes in queries containing user-defined algebraic data types, transforms them to queries without algebraic data types, calls an existing core solver on the generated queries, and returns the result. We call this transformation a reduction and we say that the approach is eager because it introduces all of the neccessary axioms for reasoning upfront as part of the reduction. Most existing solvers for this theory take a lazy approach: they introduce axioms iteratively.

The main theoretical challenge is to construct a terminating reduction and to prove its correctness. The main practical challenge is to outperform existing tools with years of engineering. We do both. Specifically, we present a new measure based on the depth of the input query; we define our reduction by bounding the introduction of axioms using this measure; prove that this bound is sufficient; and empirically demonstrate that the bound is not too loose by outperforming state-of-the-art SMT solvers on a collection of benchmarks from related work. Perhaps the most interesting result is that the unique algorithmic approach that we take—eager instead of lazy—leads to unique and excellent empirical performance. Our solver handles many queries that no other solver can, leading to the best contribution score in our evaluation.

4.1 Introduction

MedleySolver frames the problem of choosing an SMT solver as a modified Multi-Armed Bandit (MAB) problem, a classic reinforcement learning formulation in which an agent must repeatedly pick from several different choices with unknown reward distributions, minimizing overall regret. This agent must trade-off between exploitation (choosing a solver that is already believed to be fast) and exploration (testing out other solvers). For a given SMT query, MedleySolver selects a sequence of solvers to run, running the solver it believes is most likely to solve the query first and the solver that is least likely last. MedleySolver also predicts the time it should spend running each solver before it should give up and move onto the next solver in the sequence.

We apply classic algorithm selection techniques from the domain of Multi-Armed Bandit problems to the order selection problem. In this work, we highlight Thompson Sampling and \(k\)-Nearest-Neighbor (\(k\)-NN) classification. We select these two as high-performing instances of a non-contextual and a contextual algorithm respectively but perform a more extensive comparison with a variety of other Multi-Armed Bandit algorithms for completeness. These algorithms traditionally predict one optimal action, but we use them to rank SMT solvers on a given query based on the behavior observed on previous queries and, in the case of the contextual bandit algorithms, a feature vector. This ranking allows the algorithm to explore and exploit in a single round.

Non-contextual multi-armed bandit algorithms have been directly applied to selecting search heuristics and variable orderings for constraint satisfaction problems (Xia and Yap 2018; Wattez et al. 2020), and to implementing co-operative sharing of clauses in parallel SAT solving (Lazaar et al. 2012). Our use of a contextual multi-armed bandit framework to select a sequence of SMT solvers for a given SMT query is novel.

We pair these order selection algorithms with two runtime prediction algorithms. The first runtime prediction algorithm estimates the time each solver should be run by modeling its performance as exponential distributions with a parameter that is updated dynamically. The second fits a linear model using stochastic gradient descent (SGD). Runtime estimation helps reduce the cost of exploratory solver choices that do not produce rewards by stopping solvers when we are confident they will not finish before the overall timeout.

Our work is inspired by recent work showing machine learning techniques can be used to solve SMT queries faster. For example, FastSMT (Balunovic, Bielik, and Vechev 2018) is a tool that uses machine learning to find an optimal sequence of tactics, or query transformations, for SMT solvers to use on queries from a given domain. One issue with such approaches is that the complexity of the learning methods leads to training times grossly larger than the time spent solving. In this work, we achieve comparable performance boosts with no pre-training or additional burden on the SMT end-user. To meet this goal, we approached the problem of algorithm selection for SMT solvers in a dynamic, or “online,” manner. This ensures the cost of our training remains small, proportional, and justified by how SMT practitioners use SMT solvers. For example, techniques such as counterexample-guided inductive synthesis (CEGIS) (Solar-Lezama et al. 2006) produce long sequences of similar SMT queries that are not easy to obtain prior to solving for offline training. Overall, we make the following contributions.

1. An adaptation of standard regression techniques to predicting when a given solver will timeout on a query, and a novel approach for the same time allocation problem that models runtime as exponential distributions and estimates timeouts dynamically and with context.

2. A framing of the SMT solver selection problem as a Multi-Armed Bandit (MAB) problem combined with a timeout prediction scheme. Specifically, we extend the MAB problem to selecting sequences of solvers per query instead of a single solver and use the timeout prediction scheme to allocate time to each solver in the sequence. This interaction lets us use lightweight techniques for both problems that do not require pre-training while retaining comparable performance to pre-trained techniques.

3. An empirical evaluation on a set of \(2000\) benchmarks representing a typical user’s workload. Our approach solves \(1813\) queries on this set; \(128\) more than the next best solver in \(3/5th\) of the time, with no pre-training.

4.2 Related Work

MedleySolver is most related to algorithm selection techniques for SAT and SMT. Our motivation, however, is similar to portfolio-based approaches.

Early approaches to learning-based algorithm selection in solvers included picking between different encodings of SMT to SAT in the UCLID solver (Seshia 2005; Bryant, Lahiri, and Seshia 2002) and selecting input parameters for SAT solvers (Hutter et al. 2007). SatZilla (Xu et al. 2008) used empirical-hardness models to map queries to SAT solvers. Models are learned offline, then combined with a fixed order of “pre-solvers”—solvers that are called before featurization with a short timeout—when online. MedleySolver differs from SATZilla in that it targets SMT, learns solver orders, distributes time among solvers, and does not require training. ArgoSmArT \(k\)-NN (Nikolić, Marić, and Janičić 2013) applies a pre-trained \(k\)-Nearest-Neighbor algorithm to portfolio SAT solving. Given a query, they deploy the most successful solver on the \(k\) nearest neighbors. Although one algorithm we apply is \(k\)-NN, we use it to select sequences of solvers and apply it in combination with the time-prediction algorithm. MachSMT (Scott et al. 2021) is a pre-trained tool like SatZilla but for SMT. Like SatZilla, MachSMT pre-trains to learn an empirical hardness model, then used to predict solving time for a given query. This is related to our timeout estimation, however, our version requires no pre-training. We achieve similar performance to MachSMT without pre-training by decoupling solver choice from time allocation and allowing for mistakes by selecting a sequence of solvers to run, instead of a single solver. Where4 (Healy, Monahan, and Power 2016) is a portfolio-based SMT solver that uses regression models to select which solver to run. It extracts features from WhyML programs rather than SMT queries and does not allocate time between solvers. CPHydra (O’Mahony et al. 2008) does allocate time between solvers but does so by solving an NP-Hard problem (knapsack). CPHydra also ignores solver order, requires offline training, and is aimed at CSP, which is related to, but different from, SMT. FastSMT (Balunovic, Bielik, and Vechev 2018) is a pre-trained learning tool for speeding up the Z3 SMT solver that works by selecting algorithmic “tactics” or strategies inside the solver itself. FastSMT is interesting because it produces an interpretable strategy that can often be significantly faster than Z3 out-of-the-box. MedleySolver differs from FastSMT in that it learns to combine solvers, rather than to combine the tactics of a single solver. FastSMT also requires significant training time.

Parallel portfolio solvers execute sets of solving processes in parallel for each query. Our approach is complementary in that we focus on speeding up sequential computation: different configurations of MedleySolver could be run in parallel with a portfolio approach. Nevertheless, portfolio approaches share a similar goal, so we highlight related works in this space. PAR4 (Weber 2019) is a basic portfolio parallel SMT solver that won several tracks in the SMT competition (SMT-COMP) in 2019. Wintersteiger, Hamadi, and de Moura (2009) implement Parallel Z3, a portfolio solver for SMT with the additional feature that learned clauses are shared between processes. Menouer and Baarir (2017) combine search space-splitting with portfolio solving by using EXP3 to dynamically allocate cores to each search space splitting solver from a set. Our approach differs in that we focus on SMT, not SAT; we allocate time, not cores; and we use bandit algorithms (like EXP3) to pick the order of solvers, not the number of cores.

4.3 Approach: Online Learning

SMT users rarely aim to solve a single query in isolation and usually care about resource consumption. For example, verification engines generate many verification queries for one verification problem and aim to solve these queries in the least amount of time. As such, we define the practical SMT problem as that of taking a set of SMT queries \(Q = \{q_1, ..., q_m\},\) a set of SMT algorithms (usually solvers) \(S\), and producing a set of answers \(A = \{a_1, ..., a_m\},\) where each \(a_i\) corresponds to the matching \(q_i,\) while using the least computational resources.

Our approach to the practical SMT problem, MedleySolver, is a program that takes \(Q\), \(S\), and a timeout \(T\) per query, and aims to maximize the number of instances solved while minimizing the cumulative time spent. We decompose our approach into two parts. For each query \(q \in Q\), we predict

1. which solvers are most likely to solve a given query and return a list of solvers ordered by chance of success; and
2. the time each solver is likely to take to solve a given query and distribute the timeout \(T\) to the solvers in the sequence accordingly.

Given a query \(q_i\), MedleySolver generates a sequence of solvers \(\sigma\), and a sequence of time-allocations \(t_1, ..., t_n\), so that the solver in \(\sigma_1\) is run for \(t_1\) seconds and so on. If a solver in the sequence successfully solves the query, we do not run the rest of the solver sequence on that query and instead move onto the next query. For the remainder of this chapter, we use \(\sigma\) to denote a sequence of solvers and \(\sigma_i\) to denote the \(i^{th}\) solver in the sequence \(\sigma\). We process each query \(q_1, ..., q_m\) in order and our solver selection algorithms learn as we go, so the solver selection for \(q_m\) uses information from queries \(q_1, ..., q_{m-1}\). In practice, this historical information can be reset whenever and in our experimental results, we reset it when confronting a new set of queries (for instance, a new category of the SMT competition). An overview of our approach is shown in Figure 6. We describe the three main components of Figure 6: the solver selector, the timeout predictor, and the featurization of queries, in detail in the next two sections.

4.3.1 Solver Order Selection

In the Multi-armed Bandit (MAB) problem (Cesa-Bianchi and Lugosi 2006) an agent sequentially selects between choices with unknown associated reward distributions, aiming to maximize the reward achieved over time. The agent must trade off exploration (trying new actions and learning about them) and exploitation (deploying actions we know have the potential for high reward).

We frame the solver selection problem as a MAB problem. The agent is selecting the solver to use and the payout is based on successfully solving queries. We assume that running a solver for a randomly selected SMT query is equivalent to sampling from some unknown distribution that we seek to approximate. Contextual MABs extend the problem by giving agents access to a feature vector before each round. This allows us to add information about the characteristics of the SMT query we are trying to solve in each round, as described in Chapter 4.3.1.2.

We modify the MAB problem in one key way: we select a sequence of solvers to run (with corresponding time allocations that we consider later), instead of selecting a single solver. This contribution allows solver selection to perform exploration on each query until it observes a reward, has tried all solvers, or reaches the time-out per query. We also use a time-prediction algorithm, described in Chapter 4.3.2 which predicts the time it is worth running a solver on a given query, allowing us to perform “partial exploration” instead of committing to running a single solver until time-out or termination. Both of these extensions to the MAB algorithms allow the solver selection to correct incorrect solver choices, reducing the cost of exploration vs exploitation. In the following subsections, we adapt one non-contextual algorithm and one contextual algorithm (i.e., algorithms that use the feature vector) from the literature to our domain. We choose the algorithms based on their popularity in the classic literature for MAB, and the compatibility of the assumptions the algorithm makes with our domain (for instance, we omit algorithms such as LinUCB (L. Li et al. 2010), which assumes that the reward is linearly correlated with the feature vector). In Chapter 4.4 we evaluate our choices against other MAB algorithms for completeness.

We use a binary reward structure where a solver receives a reward of 1 if it is observed solving a query and 0 if it is observed failing to solve a query, which decouples solving time from rewards. We also explored an exponential reward structure where a solver receives a reward of \((1 - t/T)^4\) if it solves a query in time \(t\), but found the binary reward more effective which we believe is due to its ability to differentiate more clearly between benchmarks that are slow to solve and benchmarks that are not solved.

4.3.1.1 Thompson Sampling

Thompson Sampling (S. Agrawal and Goyal 2012, 2013) uses Bayes’ rule to choose an action that maximizes the expected reward. Each round of the MAB in this context is picking a random query from the set of queries and trying to solve it with a specific solver \(\sigma_i\). To adapt non-contextual Thompson Sampling to our SMT solver selection problem, we model the outcome of an experiment with a Bernoulli distribution where the solver solves the query with a probability \(\theta_i\) and fails to solve it within the time-out with a probability \(1-\theta_i\). In Thompson Sampling, the agent does not know the value of each \(\theta_i\) but begins with some prior belief over each one. These priors are beta-distributed: the prior for \(\theta_i\) is \[p(\theta_i) = \frac{\Gamma(\alpha_i + \beta_i)}{\Gamma(\alpha_i)\Gamma(\beta_i)}\theta_i^{\alpha_i - 1}(1 - \theta_i)^{\beta_i - 1}.\] We initially take this distribution to be uniform: \(\alpha_i = \beta_i = 1\). That is, we assume a prior that, for a random query, each solver has a \(50\)% chance of solving the query within the timeout and a \(50\)% chance of failing to do so.

To select a solver to deploy, Thompson Sampling takes a sample from each distribution \(p(\theta_i)\) corresponding to a solver. Note that, because Thompson Sampling takes a sample from the distributions \(p(\theta_1)...p(\theta_n)\), it is more likely to pick solvers that we are uncertain about instead of simply returning the solvers in order of the \(p(\theta)\) with the highest mean, allowing exploration. Conventional Thompson Sampling returns the solver with the highest valued sample. Our algorithm returns a sequence of solvers in descending order of these sampled values i.e., the solver with the \(\theta\) closest to 1 is first.

After deploying the solvers and observing the results, the distributions over \(\theta_1, .., \theta_n\) are updated according to Bayes’s rule. Each time a solver \(\sigma_i\) is run, a reward \(r_i\) is observed. The posterior distribution for the beta distribution (Castillo, Hadi, and Solares 1997) is obtained by adding the reward \(r_i\) to \(\alpha_i\) and \(1 - r_i\) to \(\beta_i\), as illustrated in Figure 7.

Thompson Sampling assumes events are independent, i.e., the probability of a solver being able to solve a query is independent of all queries the solver has seen before. This could be true if our time-out prediction algorithm is perfect so that if a solver can solve a query within the timeout \(T\), the solver will also always be able to solve that query within the time \(t\) allocated to the solver.

4.3.1.2 Features for Contextual Approaches

Contextual approaches depend on the assumption that queries with similar characteristics will cause SMT solvers to perform similarly. We capture the characteristics of each SMT query \(q_i\) in a feature vector \(\boldsymbol{v}_i \in V\). We use these feature vectors both in contextual bandit algorithms (described next) and in our contextual time-prediction (described in Chapter 4.3.2).

We identify a list of 24 features that are quick to extract and that we believe correlate with solving time for specific solvers. These features include context-free qualities like counts for specific operators (e.g. array store operators), the maximum value of literals, the sum of literal values, and so on. The features also include context-sensitive qualities like quantifier nesting and alternations, as well as the size of a given queries’ abstract syntax tree as a minimal graph (we refer to this representation as a term graph). All feature extraction procedures run in \(\mathcal{O}(n)\) where \(n\) is the size of the term graph. The term graph construction is efficient and the term graph itself is often exponentially smaller than the input query. Therefore, the cost of extracting features is relatively small.

As a heuristic, we try to build features that can differentiate solver performance on their own. For example, Figure 8 (a) shows the performance of three different SMT solvers over one of these features. For this example, intuitively, we would want to favor the use of Bitwuzla as the feature value increases, instead of CVC4, which appears to be more sensitive to changes in that feature. While we did not do any empirical feature selection, we did use our prior knowledge of SMT solvers to decide which feature extractors to build, and we evaluate the impact of our decisions in Chapter 4.4.4.4.

4.3.1.3 \(k\)-Nearest-Neighbor

The \(k\)-Nearest-Neighbor algorithm(\(k\)-NN) is a simple contextual approach. Viewed from the perspective of a MAB problem, given solvers \(s_1, ..., s_n\), \(k\)-NN classifies SMT queries into \(n\) classes: queries where solver \(s_1\) is the best choice, queries where solver \(s_2\) is the best choice, and so on. We extend the standard \(k\)-NN algorithm to return a sequence of solvers.

Given a query, \(q\), the basic \(k\)-NN algorithm looks at the \(k\) nearest queries to \(q\), tallies the number solved by each solver, and orders the solvers by their tallies. We calculate the distance between two queries—how “near” two queries are—by computing the Euclidean distance between their feature vectors. The idea behind this algorithm is that if a solver succeeded on many queries similar to \(q\), then it is likely to succeed on \(q\). If any solvers in the solver set are not included in the neighbors, we randomly shuffle these solvers and append them to the end of the sequence—we make an exception for the \(k=1\) case: when \(k=1\) we return the solver that solved the nearest neighbor, followed by the solver that solved the next nearest neighbor and so on, without replacement.

Once an order is selected, we run the solvers in sequence. If a solver \(s\) succeeds, we add the feature vector of that query to our data set of previously solved queries along with the label \(s\). See Figure 9 for three steps of a 1-nearest neighbor example.

4.4 Empirical Evaluation

We implemented a prototype of MedleySolver in Python.¹⁴ The input is a directory of queries, and the output is the result, solver used, and time elapsed per query. In this section, we evaluate this prototype and aim to answer the following research questions:

1. How does MedleySolver compare to individual solvers on the practical SMT problem?

2. How does MedleySolver compare to the best available alternatives on the practical SMT problem?

3. How do the individual components of MedleySolver affect the overall performance?

4.5 Conclusion

In this chapter, we described the arrow that leaves Figure 1(F): a new way to coordinate solvers, like those described in Chapter 3, called MedleySolver. MedleySolver addresses a practical need borne from theoretical limitations. Solver performance can differ greatly across domains due to the use of carefully tuned heuristics that maximize performance in settings where no dominant algorithmic strategy exists. At the same time, solver users usually need to solve multiple related queries in sequence. If the user does not know which solver is best for their domain, then performance over the entire sequence can be prohibitively poor. MedleySolver learns to use a set of solvers over a stream of input logical queries to optimize performance over the sequence without human intervention.

We empirically demonstrated the power of MedleySolver over a set of benchmarks from related work in comparison with existing alternatives. We found that MedleySolver outperforms every individual solver and is comparable to existing pre-trained approaches, even though MedleySolver uses no pre-training. When accounting for pre-training time, MedleySolver significantly outperforms all related work. In short, MedleySolver eliminates the need for users to know which solver is best for their domain.

5.1 Introduction

Programming error-free, reliable, distributed systems is hard. Engineers need to reason about numerous control branches stemming from a myriad interleaving of messages. The systems are incredibly tricky to debug due to the nested mesh of messages and failures, and it is surprisingly easy to introduce subtle errors while improvising to fill in gaps between high-level system descriptions and their concrete implementations. Yet, we are dependent on distributed systems to deliver high-performance computing, fault-tolerant networked services, and global-scale cloud infrastructures. What can we do to ease the job of the engineer tasked with programming a distributed system? In this chapter we turn to a combination of formal modeling and automated reasoning.

Modeling languages and automated reasoning already play an important role in raising the level of assurance in distributed systems and cloud services. Classic domain-specific examples of the combination include TLA+ (Lamport 2002); newer examples include Ivy (Kenneth L. McMillan and Padon 2020). These languages and associated automated reasoning tools can be used to guarantee correctness for all executions of a given system model, or at least systematically explore the space in search of errors. Once developers have a correct model, they can build their production systems with confidence. Unfortunately, these modeling languages do not provide users with language primitives or abstractions to support explicit message passing. To work at the message passing level—where a significant source of implementation errors lie—therefore requires manual modelling and significant user effort, making the translation to and from production systems more challenging.

More specifically, modern programming languages provide software engineers with a choice of different distributed systems programming paradigms. Two popular paradigms include the actor model, supported natively by e.g., Erlang; and the model of communicating sequential processes, supported natively by e.g., Go. No mainstream verification language supports either of these popular paradigms. For example, a software engineer working with the actor model will likely turn to Ivy (Kenneth L. McMillan and Padon 2020), TLA\(^+\) (Lamport 1999), or Dafny (Leino 2010) for formal verification. Ivy works in the paradigm of synchronous reactive programs; TLA\(^+\) is explicitly designed not to resemble any programming language (Lamport 2021); and Dafny targets imperative programs similar Java.

To remedy this, we propose message chains, an automated method for keeping track of message chains, and a verification framework that uses message chains to give users the vocabulary to reason about the low-level details of explicit message passing while remaining at an intuitive level of abstraction. Informally, message chains are sequences of logically related messages. This idea is related to message sequence charts (ITU-T 2011) from the software engineering community, and choreographic programming languages (Montesi 2014) from the programming languages community. Message sequence charts are partial specifications that describe the flow of messages through distributed systems. Engineers use these charts for testing, design, simulation, and documentation. Choreographic programming languages, on the other hand, are high-level languages that define distributed systems from a global perspective, focusing on communication flows. Both message sequence charts and choreographic programming offer developers a way to reason about explicit message passing but with the context of how messages flow through the system in question. In this work, we use message chains to bring these same ideas to formal verification.

The rest of this chapter is organized as follows. We begin by revisiting and generalizing the running example from Chapter 1.2 in Chapter 5.2. We then survey related work in Chapter 5.3 and present the necessary background to understand our approach in Chapter 2.5. We formally define the verification problem and our encoding in Chapter 5.4. The problem definition captures systems with any number of machines executing for any number of steps; the encoding captures the notion of message chains and the instrumentation needed to use them. Chapter 5.4 also formally defines message chain invariants and gives a detailed verification of the running example using them. In Chapter 5.4.6 we implement an instance of our verification approach for the P programming language specifically and we call the resulting tool the P Verifier. We then empirically evaluate our implementation in Chapter 5.5. Overall, we make the following contributions.

1. We define message-passing distributed systems based on I/O automata. We define the verification problem and build a framework that compiles the problem to mar programs.

2. We define the notion of message chains and integrate it into our message-passing distributed systems. This notion is suited to programming languages like Erlang,¹⁵ Akka,¹⁶ and P (Desai et al. 2018, 2013).

3. We instantiate our framework for a version of the P language and call the result the P Verifier. We then replicate verification efforts from related work, and simplify these proofs using message chains. We then verify a correctness property for a system with complex message passing—the onion routing network—and two industrial case studies.

5.2 Running Example

Consider again the ring leader election protocol from Chapter 1.2. We display an implementation of this protocol in P-like syntax in Listing 4. This language is like mar but with the extensions described in Chapter 2.5.1, inline let-bindings, P-like syntax for machines and events (described below), and a new induction command that is syntactic sugar for requires and ensures conditions. This code represents an input model to the P Verifier—it is an example of Figure 1(C).

P programs consist primarily of event and machine declarations. Event declarations define the kind of messages machines exchange and the payloads these messages hold. Machine declarations define the kinds of machines in the system and how they interact with each other. In this figure, we define one kind of event, eNominate, which holds an identifier (line 9). We also define one kind of machine, Node, which has no fields, and two states: Search and Won (lines 10-21). When nodes enter the Search state, they send their value to the node on their right (lines 12-13). After sending their value, while nodes are still in the Search state, nodes react to receiving nominations in one of three ways (lines 14-20). First, when nodes receive a value less than their value, they send their value to the node on their right (lines 19-20). Second, when nodes receive a value greater than their value, they forward this new value to the node on their right (lines 17-18). Third, when nodes receive their own value, they move to the Won state (line 16). The code blocks that begin with the keyword on are handlers.

Note that Listing 4 makes no mention of the number of nodes in the system. In Chapter 1.2 we considered only instances of the ring leader election protocol with three nodes. In this chapter, we consider all possible instances of the protocol. We describe this in detail in Chapter 5.4. For now, it suffices to know that the node (lower-case “n”) definition (line 1) declares a new uninterpreted sort that represents a pointer to, or label of, Node (upper-case “N”) machines. The size of the universe of node determines the number of Node machines, and the verification engine that we define will be free to search for counterexamples over any possible universe of node.

data node
type mc = message_chain[node]
type sys = system[node]

let btw(w: node, x: node, y: node): boolean
let right(n: node): node      
let le(x: node, y: node): boolean

event eNominate = {id: node}
machine Node {
  state Search {
    on entry do {
      send right(this), eNominate(this)}
    on eNominate e do {
      let curr = e.payload.id in
      if curr == this then goto Won
      else if le(this, curr) then 
        send right(this), eNominate(curr)
      else 
        send right(this), eNominate(this)}}
  state Won {}}

let in_flight(s: sys, e: mc): boolean = 
  s.events[e] and e is send
let leader(s: sys, l: node): boolean = 
  s.machines[l].Node_state is Won
let rec participated(e: mc, r: node): boolean = 
  if e is empty then false
  else e.source == r or participated(e.history, r)

induction (s: sys) 
  invariant unique_leader: forall (l: node, n: node)
    leader(s, l) and leader(s, n) ==> l == n
  invariant leader_max: forall (l: node, n: node)
    leader(s, l) ==> le(n, l)
  invariant participated_means_le_head: 
    forall (e: mc, n: node) let head = e.payload.id in
      in_flight(s, e) and participated(e, n)
        ==> le(n, head)
  invariant not_participated_means_going_to_visit: 
    forall (e: mc, n: node) let head = e.payload.id in
      in_flight(s, e) and not participated(e, n)
        ==> btw(head, e.target, n) or e.target == n

5.2.2 Verification

Our goal, in general, is to prove that systems of asynchronously communicating state machines guarantee specified safety properties. The P Verifier is responsible for this process. It takes a set of properties and returns true if the conjunction of properties passes a proof by induction. For the ring leader election protocol specifically, we prove that there is only ever a single node that declares itself the winner and that the winning node has the label with the greatest value, regardless of the number of nodes included in the system. In general, and specifically for the ring leader election protocol, our proofs will rely on message chains. Note that while a successful proof by induction implies there are no bugs, a failed proof by induction does not imply there are bugs. This fact makes our tool unsuitable for bug finding, like all other proof-by-induction-based tools. But our work can be easily extended to support bug-finding algorithms, like bounded model checking.

Textbook proofs of correctness for such a ring leader election protocol often assume synchronous execution of nodes (e.g., Aspnes (2020)). For the synchronous version of this protocol, for every round \(k < n\), every node sends the greatest value it has seen so far to the node on its right. After \(n\) rounds, the protocol terminates as every node is aware of the greatest value in the ring. Proofs of correctness for the synchronous version of this protocol use induction on the round number. Unfortunately, most realistic implementations are not synchronous so these textbook proofs of correctness do not apply. In the asynchronous setting, proofs of correctness for this protocol tend to ignore message passing altogether. For example, Koenig et al. (2020) provide a proof in mypyvy that abstracts away individual message buffers into a single, shared, append-only relation.¹⁷ Padon et al. (2016) provide a similar proof in Ivy.

In this chapter, we propose a new verification approach based on message chains and use it to prove the correctness of asynchronous distributed systems at the message-passing level of abstraction. For example, for the ring leader election protocol, we can encode and machine-check a proof of correctness that is simple, like the textbook proof, and asynchronous, like the mypyvy proof, all while being at a lower level of abstraction than both, since it captures message passing directly. Specifically, Listing 4 displays the full verification of the ring leader election protocol in our prototype verification framework, the P Verifier. This proof, which we revisit in Chapter 5.4, uses two target invariants and two auxiliary invariants—invariants used to make the target specification inductive. The first invariant captures the desired property that there is only ever a single node that declares itself the winner. The second invariant captures the desired property that the winning node has the label with the greatest value. The third invariant is an auxiliary invariant. It says that the head of every message chain always holds the largest label it has seen so far. The fourth invariant is also an auxiliary invariant. It says that, for every message chain, if there is a node that has not yet participated in the message chain, then the message chain is going towards that node. Together, these four invariants capture the textbook proof of correctness over every message chain: for every message chain, the round number in the textbook proof is equal to the length of the message chain.

We provide the full proof of correctness for the ring leader election protocol in Chapter 5.4.5. However, proofs are generally not correct on the first attempt. Figure 11 is a visualization of what a more realistic interaction with the P Verifier would look like. The user first provides a system model (Figure 11 A) and specification (Figure 11 B), and then calls the P Verifier. Usually specifications, like the two target invariants for the ring leader election protocol, are not inductive on their own. In Figure 11 C, the P Verifier rejects the first proof attempt and provides a counterexample to induction. This does not necessarily mean that the model violates the specification, it only means that the proof by induction failed. To fix this, the user must provide auxiliary invariants. Figure 11 D represents an auxiliary message chain invariant. Specifically, Figure 11 D is a visualization of an invariant that asserts that the head of every message chain always holds the largest label in the message chain so far. With the added auxiliary invariants, the user will call the P Verifier again. Figure 11 E represents a successful proof attempt.

5.3 Related Work

Schwarz and Mattern (1994) define a notion of causal histories that has some features in common with message chains. For a given event \(e\), the causal history of \(e\) is the set of events that happened-before (Lamport 1978) \(e\). Message chains are a focused and ordered version of causal histories. That is, the chain relation in a message chain induces a sub-relation of happened-before, but the inverse is not true. See Figure 10 for a visual comparison (e.g., event 2:1 happens before event 2:2, but the two events are not related in terms of message chains). Some of our key insights are that thread order is not necessarily important in the context of asynchronous message-passing verification, and that a lightweight but useful abstraction which ignores thread order can be extracted from the syntax of message-passing programs (message chains).

P (Desai et al. 2018, 2013) comes with an explicit-state model checker that allows users to systematically test their programs over concrete configurations—such as the ring leader election protocol with three nodes. Usually, the state space of P programs, even in concrete configurations, is so large that explicit-state model checking can only be used to find bugs. Our work, the P Verifier, can be used for the unbounded verification of parametric configurations of P programs—like the ring leader election protocol with n nodes. P’s explicit-state model checker and the P Verifier are complementary: users can test their systems until they are confident that they can write a proof of correctness.

Ivy (Kenneth L. McMillan and Padon 2020) is a synchronous reactive programming language and framework for designing, testing, and verifying distributed algorithms. Ivy supports a multitude of features, including compilation to executable code and verification through model checking and induction, all while ensuring that every query to an SMT solver belongs to a decidable fragment of first-order logic. mypyvy (Feldman et al. 2019) is inspired by Ivy but contributes a methodology for inferring inductive invariants through lightweight user guidance. Specifically, users provide mypyvy with a system model and an automaton that describes the high-level “phases” of the system in question; mypyvy then uses the automaton to decompose the invariant inference problem and return a safety guarantee based on a set of inferred phase invariants. QuickSilver (Jaber et al. 2020) presents a framework for modeling and verifying distributed systems based on sound abstractions of complex components and then verifying the system assuming the complex components are verified separately. IronFleet (Hawblitzel et al. 2015) is a methodology for verifying distributed system implementations that was validated through a large-scale case study of a practical, real distributed system. The P Verifier differs in that it is domain-specific and supports verification at the message-passing level of abstraction using message chains.

The most related work is that of Talupur and Tuttle (2008), who observe that message sequence charts can be used as a proof artifact. The authors formalize the notion of message flows, which in our framework are akin to a sequence of actions, and integrate Message Flows into the CMP proof method (K. L. McMillan 2001). In follow-up work (Sethi, Talupur, and Malik 2014), the authors note that the “key limitation of our approach is that the invariants have to be derived manually by inspecting counterexamples.” Our work addresses this limitation. Other than the use of specification mining, message chains differ from message flows in three big ways: expressive power, verification flexibility, and programming language integration. In terms of expressive power, message flows can only express fixed-length sequences, so they cannot capture properties like those we use for the ring leader election protocol or the onion routing protocol, among others. In terms of verification flexibility, due to how they compile flows to the CMP verification method, their users can only specify a disjunction of possible flows. In contrast, our users can also express conjunctions and negations. Finally, we show how to use these ideas in real programming languages.

5.4 Approach: Message Chain Invariants

In this section, we formulate the problem of verifying asynchronously communicating state machines, we describe our verification workflow, and we define message chain invariants. All of this is built on top of FOLDS Automata (first-order logic distributed systems automata), a short-hand for parametric compositions of I/O automata with restrictions that

1. make modelling distributed systems easy (see Chapter 5.4.6),

2. make encoding these systems into SMT straightforward (see Chapter 5.4.3), and

3. enable our verification workflow by integrating message chains.

data [E, R] MC = | empty 
  | send (source: R, target: R, payload: E, history: MC[E, R])

5.5 Empirical Evaluation

We aim to answer the following research questions.

1. Is the P Verifier expressive enough to replicate existing proofs from other systems? How does the performance of the P Verifier compare to the state-of-the-art?

2. Do message chains help simplify proofs?

3. Can we use the P Verifier to verify industrial distributed systems?

5.6 Conclusion

In this chapter, we described the arrow to Figure 1(E): a verification engine that takes formal models and specifications, and generates logical queries that can be solved by tools like our work in Chapter 3—the arrow from Figure 1(E) to Figure 1(F). The main challenge with verifying distributed systems is in managing the level of abstraction of models. More abstract models can be easier to verify, but harder to link to implementations. Low-level models are hard to verify, but easier to link to implementations. We introduce a new abstraction, called message chains, that can be automatically extracted from and linked to low-level models. Message chains allow users to reason about sequences of related messages instead of only individual messages. This leads to proofs at a more abstract level while retaining the low-level details of low-level models.

Our empirical evaluation demonstrates that message chains are a powerful new tool that distributed system engineers can use to verify their systems. Specifically, we show that the P Verifier is expressive enough to replicate proofs from other systems; that the P Verifier performs comparably to mypyvy in terms of runtime; that message chains can simplify proofs when the system involves communication; and that the P Verifier can be used to verify industrial benchmarks.

A new version of the P Verifier, which is part of the P language toolchain and includes the advanced solver interface described in Chapter 2.4, is in use at Amazon Web Services today. The new P Verifier was used to verify an industrial version of the 2PC protocol. This protocol works for multiple rounds of transactions and is used to maintain agreement on a partitioned key-value store. See P Team (2025) for more details.

6.1 Introduction

The intuition behind our approach is that message chains reveal enough structure that they can even be used to automatically learn meaningful specifications from only distributed system execution data. That is, given only example message chains (no access to the system definition or specifications), existing learning techniques can discover properties that hold for all executions of a system. In Chapter 6.4.1 we describe how an existing program synthesis technique can be used to discover the third invariant of Listing 4 using only example message chains. Without message chains, given only example execution logs, the same off-the-shelf, state-of-the-art tool is unable to learn any meaningful specifications.

This learning from examples problem is usually called specification mining (Ammons, Bodı́k, and Larus 2002) or likely invariant synthesis (Ernst et al. 2001) and has applications beyond verification. For example, specification mining can be used for automated program repair (Demsky et al. 2006), testing (Schuler, Dallmeier, and Zeller 2009), system understanding (Beschastnikh et al. 2015), and more. In this chapter, we focus on validating the use of message chains for specification mining by showing that learning techniques can discover invariants that appear in our manual verification efforts.

Figure 12 shows a workflow diagram that illustrates how specification mining and verification fit together. The user first inputs a model (Figure 12.a) of their system written in the version of P (Desai et al. 2018, 2013) described in Chapter 5.4.6. This model is fuzzed (Figure 12.b) to generate positive example message chains (Figure 12.c). We formally defined message chains in Chapter 5.4 and we formally define positive (and negative) examples in Chapter 6.3. The message chains in Figure 10 correspond to the “Positive Examples” in Figure 12.c: these can be obtained automatically by fuzzing the input model (Figure 12.a). The user can optionally add negative examples (Figure 12.d) and then run the specification mining framework (Figure 12.e) described in Chapter 6.4, producing likely invariants (Figure 12.f). The user can use these likely invariants as their specification, provide their own invariants (Figure 12.g), or both. Either way, the model (Figure 12.a) and invariants (Figure 12.f and Figure 12.g) are given to the verification engine (Figure 12.h) described in Chapter 5.4 which returns either true, if the proof by induction passes, or false otherwise. This process is usually iterative with the user changing their model, invariants, or adding examples manually or through fuzzing.

The rest of this chapter describes the specification mining components of Figure 12 in detail. We begin with a survey of related work in Chapter 6.2. We then present the necessary background to understand our approach in Chapter 6.3. We formally define the specification mining problem and describe two approaches for mining message chain invariants in Chapter 6.4. Finally, we evaluate both approaches empirically in Chapter 6.5. Overall, we make the following contributions.

1. We define the notion of positive and negative message chain examples and describe new ways to use existing learning and program synthesis techniques to automatically mine specifications from examples only.

2. We evaluate this technique by automatically mining useful specifications for the distributed systems we verified in Chapter 5.

6.2 Related Work

I4 (Ma et al. 2019) is a property-directed reachability (PDR) based approach to verifying distributed systems. I4 learns an inductive invariant over a bounded number of steps of the protocol and then uses this to infer a general inductive invariant for the infinite distributed protocol. Koenig et al. (2020) extend the PDR algorithm using first-order quantified separators. SWISS (Hance et al. 2021) and DistAI (Yao et al. 2021) tackle the same problem but with approaches that are not based on PDR. Inductive invariant synthesis (what they do) and specification mining (what we do) are two different problems. Inductive invariant synthesis is when you have a target property (something you would like to guarantee) and you want to find auxiliary invariants to make your proof by induction pass. Specification mining is when you have a system that you can observe and you want to come up with properties that likely hold. Furthermore, none of these tools are tailored to the message passing level of abstraction.

Jeppu et al. (2020) propose a program synthesis-based technique for automatically learning models from distributed system execution traces. This work follows a long line of related techniques starting in the 1970s (Biermann and Feldman 1972). Many modern techniques in this space are based on Evidence-Driven State Merge (EDSM) (Lang, Pearlmutter, and Price 1998). Our work is complementary in that we aim to mine specifications instead of models. In that sense, our work is more similar to likely invariant synthesis techniques, like Daikon (Ernst et al. 2001). However, we also provide a verification framework and our invariants are tailored to the distributed systems domain.

6.3 Background

In this section, we define specification mining and give the necessary background on two learning techniques that we use to solve the specification mining problem.

6.4 Approach: Function and Pattern Learning

Up until now, we have assumed that users provide system models and specifications. This is the same requirement imposed by related work. However, in practice, specifications are not always obvious and formally expressing them is not always easy. In this section, we describe an approach to mining specifications—message chain invariants—using existing learning techniques. Positive examples can be generated easily by fuzzing the target system. Negative examples, on the other hand, are harder to generate automatically. In our setting, we take negative examples to be hints from the user: they are examples that the user believes can never occur during an execution.

6.5 Empirical Evaluation

We combine the recursive function synthesis approach and the extended non-erasing pattern learning approach into the same framework as the P Verifier. This code includes fuzzing infrastructure to generate positive example message chains. We implement the extended \(\ell\textit{-minl}\) algorithm as a Python program of approximately 250 lines that uses Z3 for the NP oracle that checks sequence membership. The Python code is available with the OCaml code described in Chapter 5.4.6. We use Burst out of the box for synthesis of recursive functions.

For each target distributed system of interest, we give the framework many different queries. The queries all follow the same structure described above, but we categorize and clean the input data before calling the individual tools.

For categorization, we tag example message chains with the last instruction relevant to them, and we group message chains by this tag. For example, for the ring leader election protocol in Listing 4, there are four groups: message chains that have just started at line 13; message chains that have reached the leader at line 16; and message chains that have just been extended at lines 18 and 20. For cleaning, we take each group of message chains and we generate new sets of message chains that each focus on a different aspect. Specifically, we generate a set that removes all payload information from message chains, leaving only the sequence of nodes visited by each message chain (the source of each message along with the final target); and we generate a set that removes all source and target information, leaving only the sequence of payload values exchanged.

For the ring leader election protocol, this categorization and cleaning process generates 12 queries (4 groups, 3 versions of queries each). We give all twelve queries to both specification mining methods (using algebraic data type and sequence encoding as appropriate) and we return 24 suggested invariants to the user. The input queries to Burst contain three negative examples generated by hand and 8 positive examples generated automatically by fuzzing. The three negative examples represent three obviously impossible message chain: one where a node sends a value that is not its own and it did not receive; one where a node sends a value to a node that is not on its “right;” and one where a node receives its own value and instead of declaring itself the winner and stopping, it extends the message chain by sending a new message.

We evaluate our specification mining framework on the four unique systems from the benchmarks that display message chain of length longer than three messages because these are the hardest cases. The other benchmarks from related work are either simplified versions of the four (e.g., ‘client-server-ae’ is like ‘client-server–db-ae’ but without a database) or they do not display very complicated message passing (e.g., ‘ticket’ which we briefly describe in Chapter 5.5.1). We generate examples and create specification mining queries as described in Chapter 6.4. All specification mining runs terminated in less than a second.

For “ring,” we are able to automatically discover the first auxiliary invariant of Theorem 2, and the correct, but less immediately useful fact that the suffix of message chains leading to a victory is a list of nodes from left to right, ending in the leader. For “client-server-db-ae,” we are able to automatically discover the first (target) and fourth (auxiliary) invariants described in the verification in Chapter 5.5.2.1; and that every message chain in the client-server-db system begins with a Client—a fact that is very close to the third invariant of the same verification. For “firewall” we are able to discover the specification that every message arriving at an internal node must have originated from an internal node; that the firewall blocks messages originating from external nodes; that blocked message chains are of length at most one; and that complete message chains are of length at least one. For “tor,” we are able to automatically mine the target invariant described in Chapter 5.5.2.4.

In total, this means six out of 24 invariants used in the proofs were mined. Removing the mined specifications from their respective proofs makes each of the proofs fail: these six specifications are essential. The mined specifications that do not appear in the hand written proofs may still be useful for other proofs or other applications, like testing, debugging, and documentation, but a thorough evaluation of the effectiveness for other applications is needed to draw any conclusions about them. In conclusion, we find that we can learn meaningful specifications using only message chain examples.

6.6 Conclusion

In this chapter, we presented the arrow from Figure 1(C) to Figure 1(D): a specification mining toolkit that uses the structure provided by message chains to discover meaningful invariants for distributed system models. In short, our tools take execution examples and infer specifications that likely hold for all executions. This reduces the burden on verification users by suggesting invariants that would otherwise require manual effort to discover and formalize.

We empirically evaluated our tools and found that six out of 24 invariants that were used in the proofs in Chapter 5 can be mined automatically in under a second each. Without the structure of message chains, the underlying learning algorithms cannot discover meaningful properties. Therefore, we conclude that message chains expose enough structure in distributed executions to make automated specification mining feasible and effective.

7.1 Introduction

Language models (LMs) have demonstrated an exceptional ability to generate code from natural language prompts for popular programming languages, like Python and Java (M. Chen et al. 2021). Unfortunately, these same language models struggle to generate code for low-resource programming languages (LPLs), like many domain-specific languages (e.g., CUDA (Tarassow 2023)). These challenges are even more pronounced for very low-resource programming languages (VLPLs) (e.g., formal verification languages like UCLID5 (Seshia and Subramanyan 2018; Polgreen et al. 2022) and mar). Existing work has attempted to remedy this issue through prompting, constrained decoding, and fine-tuning strategies. Unfortunately, these approaches fail to capture the intricacies of real VLPLs and so success remains limited. To see why, consider the following three exemplars.

First, B. Wang et al. (2023) include context-free grammars in text-to-code prompts to guide LMs toward syntactically correct answers. This approach works well for simple languages but cannot capture many programming languages that are context-sensitive. Second, L. Agrawal et al. (2023) use static analysis techniques to reject tokens that lead to syntactically incorrect output programs. This technique can go beyond context-free languages but assumes a linear programming process. Unfortunately, it is well known that the root cause of a programming error need not surface as it is written (Pavlinovic, King, and Wies 2014), necessitating backtracking and a nonlinear programming process. Third, Cassano et al. (2024) translate training data from high resource languages to low resource languages and then use this new data to fine-tune models. This approach is restricted to languages where the LM is able to translate to the language reliably but unable to generate code from natural language. Further, this approach makes the overly restrictive assumption that the target low-resource language is general purpose: e.g., we cannot translate arbitrary Java programs to CUDA.

In this chapter, we propose a text-to-code approach that is fundamentally different (and complementary) to prompting, decoding, and fine-tuning strategies. The first key idea behind our approach comes from natural programming elicitation, a kind of study that helps programming language designers understand how programmers “naturally” approach problems from a given programming domain (Myers, Pane, and Ko 2004; Chasins, Glassman, and Sunshine 2021). Programming language designers use the results of these studies to create languages that are aligned with the expectations of users, leading to less programming friction and more effective developers. We borrow this idea for the setting where LMs are the “users” of programming languages. Akin to uncovering what human users find “natural” for a given domain, we uncover what LMs find “natural.” Specifically, our first insight is to embrace LM’s tendencies and design an intermediate language that aligns with them.

The second key idea in our approach is that program analyses and repair that are overly aggressive for human users may be suitable for LM “users.” For example, in UCLID5, all variables have to be declared and statically typed: an assignment like x = 0; would require a corresponding declaration like var x: integer;. But, if an LM generates code that had an assignment without a declaration, instead of crashing, one could automatically “repair” the program and output the result.

We use these two ideas to define a new text-to-code approach called synthetic programming elicitation and compilation (SPEAC, pronounced “speak”). Specifically, for a target VLPL \(T\), we use synthetic programming elicitation to select an intermediate language \(P\) (the “parent” language) and define a subset of the language \(C\) (the “child” language). The language \(P\) should be one that LMs are good at generating (e.g. Python); the language \(C\) should be easy to compile to the target VLPL \(T\). Our approach takes \(P\), \(C\), and a compiler from \(C\) to \(T\), and produces a text-to-code pipeline for the VLPL \(T\). This pipeline uses deductive techniques to automatically repair programs generated by LMs that are in \(P\) but not in \(C\). When these deductive techniques are unable to fully repair a program, we insert a “hole” and ask an LM to finish the repair, repeating as necessary.

We demonstrate the effectiveness of this idea by implementing a prototype, called Eudoxus, that targets UCLID5 (Seshia and Subramanyan 2018; Polgreen et al. 2022), a language used for formal modeling and verification of state transition systems. UCLID5 has code examples numbering in the hundreds rather than thousands or millions. Furthermore, UCLID5 programs rely heavily on the notion of a transition system, which is not frequently found in other programming languages. As such, state-of-the-art LMs are unable to generate any useful UCLID5 code out-of-the-box (see Chapter 7.4.1). In our case study, we use Python as the parent language \(P\) and a subset of Python as the child language \(C\), and improve the performance of LM code generation for UCLID5. Overall, we make the following contributions.

1. We present SPEAC, a novel method for generating syntactically correct code from LMs in very low resource programming languages;

2. we implement this method for the UCLID5 verification language; and

3. we demonstrate substantial improvement with SPEAC in syntactic correctness, producing parsable code in UCLID5 84.8% of the time compared to 9.1% by gpt-3.5-turbo fine-tuning and 12.1% by gpt-4-turbo in-context learning.

7.2 Running Example: Traffic Light

Given a natural language description of a programming task and a target programming language \(T\), the text-to-code problem is to generate a program \(t \in T\) that satisfies the task specification. Listing 5 and Listing 6 show a real input-output pair generated by an instance of our approach targeting the UCLID5 programming language. Specifically, Listing 5 shows a task extracted from Lee and Seshia (2016), and Listing 6 shows the output corresponding to that task using a prototype implementation of our approach. Listing 6 passes all compiler checks but has a subtle semantic mistake on line 4.

Model a state machine describing a traffic light at a pedestrian 
crosswalk. This is a time triggered machine that assumes it will 
react once per second. It starts in the red state and counts 60 
seconds with the help of the variable count. It then transitions 
to green, where it will remain until the pure input pedestrian 
is present. That input is generated by some other subsystem that 
detects when a pedestrian is present, and should be modelled as
nondeterministic. When pedestrian is present, the machine 
transitions to yellow if it has been green for at least 60 seconds. 
Otherwise, it transitions to pending, where it stays for the 
remainder of the 60 second interval. This ensures that once the 
light goes green, it stays green for at least 60 seconds. At the 
end of 60 seconds, it will transition to yellow ...

module TrafficLight {
  var sigG, sigR, sigY: boolean; 
  var count, state: integer;
  var pedestrian: boolean; 
  init {
    sigG = false; sigY = false; sigR = true;
    state = 0; count = 0; pedestrian = false; }
  procedure step()
    modifies sigG; modifies sigY; modifies sigR;
    modifies count; modifies state; {
    if (state == 0) {
      sigG = false; sigY = false; sigR = true;
      count = 0;
      if (count < 60) { count = (count + 1); } 
      else { state = 1;}} 
    else { if (state == 1) {
      sigR = false; sigY = false; sigG = true;
      if (pedestrian) {
        if (count >= 60) { state = 2; } 
        else { state = 3; }}} 
...

Figure 13 shows the workflow that generates models based on task descriptions as shown in Listing 6. The workflow is parameterized by an LM, \(L\) (e.g., gpt-3.5-turbo-0125); a target language, \(T\) (e.g., UCLID5); a parent language, \(P\) (e.g., Python); a child language, \(C \subset P\) (e.g., a subset of Python); and a compiler, \(f\), from \(C\) to \(T\) (e.g., a syntax-directed translation from the subset of Python to UCLID5). Given an input task, we create a prompt \(q\) that asks the LM \(L\) to generate code, \(p \in C\), which satisfies the task description, \(q\). The second step of the workflow is to repair \(p\). If there is nothing wrong with \(p\), or \(p\) can be fixed using formal techniques described in Chapter 7.4.2, then repairing will generate a new, complete program \(p'\) and return \(f(p')\) (i.e., a program in the target language, like Listing 6). Frequently, however, repairing will generate a partial program containing “holes” (denoted “??”). For example, Listing 11 shows the first \(p\) generated for the task in Listing 5 and Listing 10 shows the corresponding partial program \(p'\) that was automatically generated using our formal techniques. Programs with holes cannot be compiled to the target language, so the third step of the workflow is ask the LM to complete the partial program \(p'\), generating a new \(p\). We use the template in Listing 9 to generate the LM prompt. Listing 12 shows the output generated by gpt-3.5-turbo-0125 when asked to repair the partial program in Listing 10. This program is still incorrect, but, it is now close enough that we can automatically repair it to a complete program without holes. Listing 13 shows the relevant portion of that complete program. This final, complete program is directly translated to the output in Listing 6. Chapter 7.4 elaborates on each of the workflow components.

To understand the subtle mistake in Listing 6 one needs some understanding of UCLID5. UCLID5 is a verification language used to model hardware and software systems as “state machine” like transition systems and to automatically check if the transition system does indeed satisfy a formal logic specification. UCLID5 transition systems primarily consist of a state space given by a set of variable declarations (e.g., lines 2-4 in Listing 6), an initialization block that represents a set of acceptable start states (e.g., lines 5-7 in Listing 6), and a transition relation block that defines how the transition system moves from one state to the next state (e.g., code starting at line 8 in Listing 6). The var keyword is used to declare variables that are internal to the transition system in question while the input keyword is used to declare read-only variables that are outside the control of the transition system in question. Listing 6 passes all compiler checks but has a subtle semantic mistake on line 4: var pedestrian: boolean; should be input pedestrian: boolean; because the presence of a pedestrian should not be controlled by the traffic light transition system. When manually assessing correctness in Chapter 7.5, this subtle mistake would prevent us from marking this example as fully correct.

7.3 Related Work

Modern language models perform exceptionally well on natural language to code generation tasks. For example, proprietary models like GPT-4 (OpenAI 2023), the Gemini (Team et al. 2024) and Claude 3 Families, and open-source models such as Code-Llama (Rozière et al. 2023) and Deepseek-Coder (Guo et al. 2024) have achieved impressive success on benchmarks such as HumanEval (M. Chen et al. 2021), Mostly Basic Python Problems (MBPP) (Austin et al. 2021), and LiveCodeBench (Jain et al. 2024). However, LMs perform better on popular programming languages that are well represented in training sets (e.g., Python) than less popular programming languages (e.g., Bash) (Guo et al. 2024; R. Li et al. 2023; Peng, Chai, and Li 2024). This effect is even more pronounced for very low resource programming languages, like UCLID5, as shown in Chapter 7.5.

In constrained decoding, syntactically incorrect code is avoided by rejecting impossible prefixes, without producing the full code (Geng et al. 2023; L. Agrawal et al. 2023; Scholak, Schucher, and Bahdanau 2021; Melcer et al. 2024). In the context of autoregressive LMs that naturally produce code left to right, it remains an open problem how to best include the inductive bias of a grammar. Bhatia et al. (2024) use LMs to rewrite existing code into domain-specific languages and prove that the translation is correct. Misu et al. (2024) use retrieval-augmented generation to write Dafny code, another low-resource language for verification (Leino 2010). Unlike these works, we focus on very low resourced languages (VLPLs), which have far fewer training examples in the public domain. Our approach is most similar to techniques that allow LMs to hallucinate but iteratively repair errors (Shinn et al. 2023; X. Chen et al. 2024; T. X. Olausson et al. 2024). For example, Elmaaroufi et al. (2024) use a mixture of prompting and compiler feedback to generate and iteratively repair Scenic code—a probabilistic VLPL that looks like Python (Fremont et al. 2023).

Recent work has considered augmenting LMs with support for low-resource programming languages (Cassano et al. 2024; F. Chen et al. 2022; Guo et al. 2024). F. Chen et al. (2022) show that, on smaller 125M parameter encoder-only models, fine-tuning on adjacent languages improves the monolingual performance coding tasks. Synthetic fine-tuning datasets curated and cleaned by LMs have shown promise for programming tasks. For example, Cassano et al. (2024) targets low-resource programming languages (e.g., Julia), using an LM to translate code examples from high-resource languages to the low-resource language. This process is promising for cases where the language model already has a baseline knowledge necessary to translate to the low-resource language and the target language is general purpose, which is not always the case for VLPLs.

7.4 Approach: SPEAC

In this section we describe the SPEAC approach. We begin with how to select \(P\) and \(C\) (Chapter 7.4.1) and the prompting that we use to interface with LMs. We then describe two formal techniques at the heart of our automated repair (Chapter 7.4.2).

# GTCODE 1: imports a class from the hypothetical library 
from FormalVerificationLibrary import Module 
# GTCODE 2: creates an instance of an imported class 
m = Module("myModule") 
# GTCODE 3: uses a dunder method (e.g., __str__) of an imported class
print(m) 

Write [PARENT LANGUAGE] code to complete the following task.
> [TASK GOES HERE]
Reply with your code inside one unique code block
[DESCRIBE CHILD LANGUAGE]
I can definitely do that! Here is the code:       
'''

Fix the following [PARENT LANGUAGE] code by replacing every occurrence 
of `??` with the correct code.
[CODE WITH HOLES GOES HERE]
Make sure that your code completes the following task.
[LINES 2-6 OF First Prompt]

class TrafficLight(Module):
    def types(self):
        self.state_t = BitVector(2)
    def locals(self):
        self.state = BitVector(2)
        self.count = BitVector(6)
        self.pedestrian = Boolean()
        self.sigG = Boolean()
        self.sigY = Boolean()
        self.sigR = Boolean()
    def inputs(self):
        self.pedestrian = Boolean()
    def outputs(self):
        self.sigG = Boolean()
        self.sigY = Boolean()
        self.sigR = Boolean()
    def init(self):
        self.state = BitVector(2)
        self.count = BitVector(6)
        self.pedestrian = Boolean()
        self.sigG = Boolean()
        self.sigY = Boolean()
        self.sigR = Boolean()
    def next(self):
        if self.state == 0:
            self.sigG = False
            self.sigY = False
            self.sigR = True
            self.count = 0
            if self.count < 60:
                self.count += 1
            else:
                self.state = 1 
        ...
        elif self.state == 3:
            self.sigG = False
            self.sigY = False
            self.sigR = False
            if self.count < 60:
                self.count += 1
            else:
                self.state = 0 

class TrafficLight(Module):
    def locals(self):
        self.state = int
        self.count = int
        self.pedestrian = bool
    def outputs(self):
        self.sigG = bool
        self.sigY = bool
        self.sigR = bool
    def init(self):
        self.state = ??
        self.count = ??
        self.pedestrian = ??
        self.sigG = ??
        self.sigY = ??
        self.sigR = ??
    def next(self):
        if self.state == 0:
            self.sigG = False
            self.sigY = False
            self.sigR = True
            self.count = 0
            ...

class TrafficLight(Module):
    def locals(self):
        self.state = 0
        self.count = 0
        self.pedestrian = False
    def outputs(self):
        self.sigG = False
        self.sigY = False
        self.sigR = False
    def init(self):
        self.state = 0
        self.count = 0
        self.pedestrian = False
        self.sigG = False
        self.sigY = False
        self.sigR = True
    ...

class TrafficLight(Module):
    def locals(self):
        self.count = int
        self.pedestrian = bool
        self.sigG = bool
        self.sigR = bool
        self.sigY = bool
        self.state = int

    def init(self):
        self.state = 0
        self.count = 0
        self.pedestrian = False
        self.sigG = False
        self.sigY = False
        self.sigR = True
    ...

7.5 Empirical Evaluation

In this section, we implement a prototype of SPEAC for UCLID5, called Eudoxus, and use it to evaluate the performance of SPEAC across three research questions.

1. Does Eudoxus perform better than LM baselines on syntactic correctness (passing compiler checks)?

2. Does Eudoxus perform better on semantic correctness?

3. Does MAX-SMT cost too much computation time?

Eudoxus uses the \(P\) and \(C\) described in Chapter 7.4 and is implemented in Python. We use tree-sitter to parse and search partial programs, and Z3 (de Moura and Bjørner 2008; Bjørner, Phan, and Fleckenstein 2015) to solve MAX-SMT queries. We allow Eudoxus to repeat the repair loop five times. All MAX-SMT queries are solved locally on a 2.3 GHz Quad-Core Intel Core i7 with 32 GB of RAM. All LM calls are made through the OpenAI Python API.[Code available at https://github.com/uclid-org/eudoxus]

We compare Eudoxus against three LM baselines: few-shot, self-repair, and fine-tuning. All using gpt-3.5-turbo-0125 (GPT3t) and gpt-4-turbo-2024-04-09 (GPT4t). For the few-shot baseline with and without chain-of-thought, we provide examples taken from the UCLID5 GitHub repository to the LM in context. We tried with one in context example, and then again with three in context examples. We also combine few-shot prompting with chain-of-thought (Wei et al. 2022). As with many VLPL, there are very limited number of natural language to UCLID5 examples in the public domain, and certainly not enough for fine-tuning. We do, however, have access to \(317\) regression tests from the open-source code base. For the purposes of fine-tuning, we use self-instruct (Y. Wang et al. 2023) to first ask the model to summarize the UCLID5 regression tests in natural language and then provide this as the natural language description during fine-tuning. We fine-tune GPT3t for 284 steps with learning-rate multiplier 0.16. For self-repair, we gave the LMs compiler feedback in a loop for five iterations starting from a zero-shot prompt.

We use three sets of UCLID5 benchmarks. The first set is a curated set of \(33\) regression tests with handwritten natural language descriptions. These tests are designed to cover a broad range of UCLID5 features and were used for the synthetic programming elicitation study in Chapter 7.4.1. The second set is a set of \(317\) regression tests without descriptions taken directly from the UCLID5 GitHub repository. These tests were used for fine-tuning our baseline model, as described above. This set is representative of the quantity and quality of data that a user may have available for a VLPL. The third and final set is a set of \(33\) exercises and examples taken from three textbooks (Baier and Katoen 2008; Lee and Seshia 2016; Huth and Ryan 2004). These benchmarks cover formal modeling of concurrent systems, linear-time properties, model checking and systems with discrete dynamics. We used this final set for the end-to-end evaluation below.

We run two variations of Eudoxus (one using GPT3t, one using GPT4t) and 11 variations of the baselines on all \(33\) textbook benchmarks. We report the fraction of outputs that pass all compiler checks (“parse,” for short) and semantic correctness over all 11 approaches in Table 4. Semantic correctness is manually assessed by one author using a combination of manual reasoning and hand-written specifications for all programs that compile. Correctness is rated on a scale from \(1 - 5\), where \(1\) is entirely wrong, and \(4\) indicates that the model is correct with only a few minor errors (e.g., the example output described in Chapter 7.2 and Listing 11). Intuitively, any score of \(\geq 4\) indicates that we believe the output would be useful to text-to-code users.

7.5.2 RQ2: Semantic Correctness

Eudoxus outperforms all baselines in terms of semantic correctness (see Figure 14), scoring 5/5 on more benchmarks than any other approach. Every unique problem that the baselines perform well on—four unique problems where some baseline scored four or higher—was also solved by Eudoxus. These are likely the easiest problems in the test set. On the other hand, \(33/52\) programs (24 unique problems) that pass compiler checks produced by Eudoxus scored four or higher. This data suggests that our approach does not negatively impact semantic performance, but it is difficult to draw conclusions since so few of the programs generated by the baselines pass compiler checks.

7.6 Conclusion

In this chapter, we described how to build the arrow into Figure 1(C). That is, we described a new methodology for building tools that generate code in very low-resource programming and formal languages from natural language descriptions. Our approach, SPEAC, bridges the gap between code that LMs are good at writing and code that we need to write for formal verification and related tasks through a mix of programming language design, human-computer interaction, and formal methods. We borrow ideas from the intersection of human-computer interaction and programming languages research to discover what LMs find “natural” in a given domain. We then design a corresponding intermediate language for which LMs are good at writing code and for which we can automatically translate programs into our target language, using ideas from formal methods.

We empirically demonstrated that this combination makes it possible to generate syntactically correct and semantically meaningful code in VLPLs like UCLID5, where traditional prompting, decoding, and fine-tuning strategies fall short. Specifically, SPEAC produces code that passes compiler checks at a much higher rate than prior approaches (syntactic correctness), and shows promising results in semantic correctness.

8.1 Crossword Construction

American style crosswords, like those found on the New York Times, consist of a set of clues, a grid of white and black cells, and a solution. The solution to a crossword is a sequence of characters, usually a word, per clue. For example, the answer for the clue “software platform suitable for Starbucks?” could be “java.”¹⁹ You can think of the clues as semantic constraints and the grid as a set of syntactic constraints. Every clue has an orientation, down or across, and a starting cell in the grid. The answer to each clue must be laid out, character by character, cell by cell, starting from the designated cell, moving in the correct orientation, over only the white cells of the grid. This imposes length constraints on answers and will lead to answers that share characters. The goal of the crossword game is to guess the solutions from the clues and the grid: players must guess a solution that satisfies both the semantic and syntactic constraints. Figure 15 shows one example crossword puzzle.

Many people play crossword games everyday; fewer people construct crosswords. Similarly, existing work, like Wallace et al. (2022), have looked at automatically solving crossword puzzles, but few projects exist for automatically generating crossword puzzles. In this section, we focus on the latter problem, and specifically on the challenges of solving the latter problem with current LMs.

Q: Make a 5 by 5 crossword grid with the fewest possible blanks 
(use * for blanks) as a markdown table using the following 
fills: DIP, IMOUT, SAUCE, CYCLE, HAN, DISC, IMAY, POUCH, UCLA, 
TEEN. 
A: 
| | | | | |
|-|-|-|-|-|
|D|I|P|*|*|
|I|M|O|U|T|
|S|A|U|C|E|
|C|Y|C|L|E|
|*|*|H|A|N|

Q: Make a 5 by 5 crossword grid with the fewest possible blanks 
(use * for blanks) as a markdown table using the following 
fills: {WORDS}
A:
| | | | | |
|-|-|-|-|-|

data letter = d () | o () | t () | BLACK ()
...

...
let p00: letter
let p01: letter
let p10: letter
let p11: letter
let off: letter
...

...
let to_00_down:   boolean
let to_00_across: boolean
let to_01_down:   boolean
let to_01_across: boolean
let to_10_down:   boolean
let to_10_across: boolean
let to_11_down:   boolean
let to_11_across: boolean
let do_00_down:   boolean
...
let do_11_across: boolean
...

...
assert to_00_down ==> 
  (off == BLACK() and p00 == t() and p10 == o() and off == BLACK())
...

...
assert at-most-one(to_00_down, to_00_across, to_01_down, to_01_across, 
              to_10_down, to_10_across, to_11_down, to_11_across)
...

...
assert ((off == BLACK() and p00 != BLACK() and p10 != BLACK()) ==> 
    (to_00_down or to_00_across or to_01_down or to_01_across or 
     to_10_down or to_10_across or to_11_down or to_11_across or 
     do_00_down or do_00_across or do_01_down or do_01_across or 
     do_10_down or do_10_across or do_11_down or do_11_across))
...

...
assert off == BLACK()
...

...
assert p00 != BLACK() ==> 
    ((off != BLACK() or p01 != BLACK()) and 
     (off != BLACK() or p10 != BLACK()))
...

...
assert (p00 == BLACK()) == (p11 == BLACK())
...

...
assert at-most-k(p00 == BLACK(), p01 == BLACK(), 
                 p10 == BLACK(), p11 == BLACK())

|A|D|S|*|*|
|D|O|U|G|H|
|A|D|D|L|E|
|M|O|S|E|S|
|*|*|Y|E|S|

|A|M|I|G|O|
|L|I|V|E|R|
|I|V|A|D|O|
|V|E|D|A|S|
|E|R|O|U|G|

8.2 Future Work

It is not yet clear how to best combine neuro and symbolic approaches. In Chapter 7 we proposed one combination that has exciting implications for the neuro-symbolic reasoning research area. For example, T. Olausson et al. (2023) follow the tool-use paradigm to solve natural language word problems by equipping an LM with an automated theorem prover tool. These same authors find that one of the biggest limitations of this approach is that LMs frequently generate syntactically incorrect calls to the theorem prover—precisely the problem we solved with Eudoxus for UCLID5. We aim to explore these exciting implications, particularly for reasoning about distributed systems described in natural language and diagrams. The dream is that developers will be able to ask questions about their documented designs and get meaningful feedback powered by scalable automated reasoning.

Our work has interesting implications for the neuro-symbolic research area beyond the tool-use paradigm. For example, agentic AI systems, which have recently gained popularity, can be thought of as a distributed systems: independent computing nodes work together to accomplish a shared goal by sending and receiving messages. Today, however, little work exists on verifying properties of agentic systems. For example, there are few tools available to ensure that private information does not leak from one agent in a system to another. We believe that programming, testing, and verification languages like P will play a crucial role in building safer agentic systems.

All of these advances will depend on the availability of fast solvers. The problem is that we do not know what logical theories and fragments we will need to support or what industrial queries will look like tomorrow. This is true for the whole field of automated reasoning: the demand for solvers is growing in often unpredictable directions. We aim to meet this demand through eager solvers. Eager solvers are promising for distributed solving, but handling theory combinations is currently challenging. We are particularly excited about facing these challenges by generating eager solvers from declarative specifications. Similarly, we are excited to explore solvers with custom LM generated components. Existing work, like Romera-Paredes et al. (2024), has successfully generated heuristics for combinatorial solvers. We believe that similar approaches can be used to generate hyper domain-specific heuristics that improve solver performance well beyond what general purpose solvers can attain today.

Finally, language design will continue to play a crucial role in all future developments. Either for getting the most out of LMs, like our work in Chapter 7, or for communicating with engineers, like our work in Chapter 5. Automated reasoning engines do not currently support many programming paradigms and features. For example, OCaml’s new concurrency model (Sivaramakrishnan et al. 2021), based on algebraic effects, is popular in programming language circles but has gained much less attention in the automated reasoning community. Therefore, today, human and non-human programmers have few choices when it comes to proving the correctness of these programs. We are interested in new programming language paradigms and features, like algebraic effects, and building full automated reasoning stacks for their users, broadly construed.