1 Introduction

Satisfiability Modulo Theories (SMT) solvers reason about logical problems expressed in terms of a wide variety of theories (arithmetic, bit-vectors, strings, and so on). They are used as back ends for software verification tools as well as a variety of other safety-critical applications (e.g., [7]). A key concern for these applications is that SMT solvers are large and complex systems. As such, they are at risk of containing bugs that affect their correctness.

A pragmatic but rigorous approach for addressing this concern is for an SMT solver to produce a proof certificate, or just proof for short, for each its answers. This is typically a textual artifact, expressing a formal proof of the answer’s correctness, which can be checked by an external tool, a proof checker [1, 17]. A proof accepted by a proof checker is a strong piece of evidence that the solver’s answer is correct. The reason is that, since proof checking is in general considerably simpler than proof finding, which is ultimately what SMT solvers do, even a proof checker that is not formally verified can strengthen the user’s trust in the SMT solver’s answer. This approach requires the definition of a format for SMT proofs, which is a serious challenge as different SMT solvers, or even different theory solvers within the same SMT solver, may use vastly different proof systems, or calculi, due to differences in the theories they support and in the preprocessing and reasoning methods they implement.

In this paper, we present Ethos, a generic proof checker for SMT. Instead of implementing a fixed calculus, Ethos supports the Eunoia logical framework, which is designed to make specifying proof systems and proofs in them simple and convenient for SMT developers. Eunoia’s syntax extends that of Version 2.7 of the SMT-LIB standard [5] with commands for (i) defining theory signatures, i.e., the collection of types, constants, and proof rules that constitute a proof calculus, and (ii) expressing proofs themselves. Given a Eunoia file that provides both a signature and a proof, Ethos checks that the proof correctly applies the rules in the signature. It can also verify that the assumptions used in a proof in fact correspond to the assertions in a specific SMT-LIB problem, thus ensuring that the proof is not just a correct proof but a proof of the correct theorem.

While Ethos is not formally verified, it significantly reduces the trusted code base. For example, the source code of the cvc5 SMT solver [3] consists of over 300K lines of C++, while Ethos is less than 10K lines of C++. The signature for cvc5 proofs is expressed in 6,397 lines of Eunoia code. Strong runtime performance was a main goal when implementing Ethos, with the aim of reducing the cost, and thus incentivizing the use, of proof checking. To this end, Ethos implements multiple optimization techniques, which we discuss below.

Related Work. The main inspiration for Ethos comes from two related systems. The first is Alethe [15], a proof format and calculus for SMT supported by the Carcara checker [1]. In contrast to Eunoia, Alethe defines a fixed calculus, described in English in a reference document [4]. The SMT solver SMTInterpol [10] uses a custom proof format similar to Alethe. The second inspiration is LFSC, also a logical framework, and its proof checker [17]. In contrast to Eunoia, its syntax does not resemble SMT-LIB and rappresents proofs as terms. Based on our experience, SMT developers find it unintuitive and difficult to use, which may have hindered its wide adoption.

Both LFSC and Eunoia are inspired by other logical frameworks, starting with Edinburgh LF [8]. Among them, Dedukti [2] stands out as explicitly designed for proof exchange. Multiple calculi for SMT solvers and other automated reasoners have been modeled in Dedukti [6]. RARE is a domain specific language for declaring proofs based on rewriting [11]. Eunoia is partially inspired by it and can be seen as a generalization of its functionality to arbitrary proof rules.

Beyond those mentioned so far, there a number of additional approaches for defining proof formats. DRAT [19] is a unified proof format for propositional logic that enables SAT solvers to easily generate proofs for most state-of-the-art solving techniques in a manner that can be efficiently checked. As a result, most contemporary SAT solvers support DRAT. Unfortunately, due to the heterogeneous nature of SMT solving, it seems doubtful that a format with a fixed proof calculus could provide similar standardization benefits for SMT. The eDRAT format [9] uses DRAT together with unjustified theory lemmas, which must be checked separately. It does not support proofs for preprocessing.

The TPTP world [18] provides a proof format for automated theorem provers (ATPs). However, it does not prescribe a way to define proof rules, and theorem provers choose their own. A notable consequence of this design choice is that, since TPTP proofs rules can be quite high level, a trusted ATP, as opposed to a simpler checker, is needed to prove individual rule applications correct.

2 Eunoia

In this section, we provide an overview of Eunoia through an example containing a signature and a proof in that signature. The Ethos user manual [13] contains a a complete introduction to Eunoia.

Types and Constants. A Eunoia signature starts with a declaration of relevant types and constants (in the HOL sense), as shown in the following. The constants , , , and are not declared because they are built-in.

Seven lines of code declare constants and functions related to natural numbers and bitwise operations. The first line declares a constant named 'nat' as a natural number type. The second line declares a constant 'and' as a function taking two Boolean values and returning a Boolean, with right-associative notation. The third line declares a parameterized constant 'and' as a function taking two Boolean values and returning a Boolean. The fourth line declares a parameterized constant 'and' as a function taking two Boolean values with implicit type arguments. The fifth line declares a parameterized constant 'bitvec' as a function from a natural number to a type. The sixth line declares a parameterized constant 'const' as a function from a natural number to a type. The seventh line defines a function 'c' taking a bit vector and returning a bit vector, using bitwise 'and' and 'xor' operations. The code uses small letters for variables and types, with some implicit type arguments. This code snippet is important for defining basic logical and bitwise operations in a formal system.

Eunoia contains several built-in syntactic categories. It is up to the user though to give them a type. In the example above, the command (line 1) tells Ethos that every (signed) numeral ( , , , ...) has type . This makes it possible to change the type of numerals depending on the SMT-LIB logic of interest. For example, in the QF_LIA logic, numerals have type , while in QF_LRA they have type . The defined symbols do not carry any semantic information, beyond their type. They are simply constructors of the term language on which the proof rules operate.

The annotation (line 3) for the constant is an extension of SMT-LIB’s annotation. It indicates that can be used as a variadic operator with as a neutral (or nil) element.Footnote 1 Like , it allows applications of the operator to more than two arguments as syntactic sugar for a nested application. However, it also allows applications of the form , treated as a shorthand for . This implies that is parsed as and not , as would be the case with the annotation. One motivation for is that, in contrast with the annotation, it distinguishes between terms like and , as the latter is parsed as . As we will see, Eunoia has additional features to facilitate working with such operators.

In Eunoia, it is also possible to define dependent types and parametric constants. In the example above, we first declare the usual polymorphic equality constant with an implicit type argument . Afterwards, we declare a size-indexed type for bit-vectors and the bit-vector concatenation constant. The return type of (line 6) is defined by a computation performed by the built-in operator for adding two numbers. Eunoia has a large library of such operators. Some, like , are primitive operators that implement fundamental functionality; others are defined as Eunoia programs built from primitive operators.

Proof Rules. After declaring the theory signature we can declare a proof signature. That consists of proof rules and associated helper programs which can be used to implement side conditions. A file inclusion command allows us to isolate the theory signature in its own file. Proof rules follow the theory signature.

Code snippet defining a program named "polic" that takes a Boolean function and a list of integers as input and returns a Boolean function. It includes a conditional statement checking if the list is empty, then returns the function applied to zero. Otherwise, it recursively calls itself with the tail of the list and combines results using logical operations. The code uses color to distinguish keywords, types, and comments for clarity.

Every command takes a rule name (e.g., , in lines 2, 6) and lists parameters used in the declaration. The attribute lists patterns for the rule’s premises. To check a proof step using rule , the proof checker applies pattern matching to two previously derived formulas to find a matching substitution for the parameter . This substitution is then applied to the conclusion, which in general is also a pattern, although not in this case. Rule illustrates the use of computations in proofs. The rule implements the elimination of variadic applications of using a recursive program, (lines 2– 5), that returns the n-th argument of a conjunctive formula.

Like rules, programs have a name and a list of local parameters that serve as pattern variables. They also have a type signature that declares the argument types ( and for ) and the return type ( ). As in many functional programming languages, a program is defined by a list of cases that are considered in order. Abstractly, each case is a pair (p, b), where p lists a term pattern for each program input and b is the case’s body. Each local parameter in b must appear at least once in p (non-linear patterns are supported). A program application is evaluated by a Eunoia checker by matching the application’s arguments against each pattern list. When this succeeds, it applies the matching substitution to the body, evaluates it, and returns the resulting term. If no case matches, the checker raises an error and rejects the entire proof.

The example also demonstrates another feature of Eunoia’s handling of variadic operators: the annotation. If an operator is annotated with , its last argument is not handled as syntactic sugar. Without it, the pattern would be parsed as to which, however, would match only with binary conjunctions—of the form .

Proofs. We can construct a proof with the rules seen so far. With the command a proof can be linked to an SMT-LIB problem (e.g., problem.smt2) to check that all declared constants and assumptions appear in the problem.

A short code snippet defines a logical proof process. It starts by referencing a problem file and including a rules file. Then, it declares a constant capital F of type formula. It assumes a condition where a small a is true if capital F is true and not true. The steps apply rules and premises to derive conclusions, ending with a step that concludes false from the premises. This shows a logical contradiction derived from the assumptions, illustrating a proof by contradiction.

The proof above has three derivation steps. The command introduces the assumption and names it . The next two commands apply rule to , deriving formulas and , respectively. The final command concludes from the formulas derived by the previous two steps. The second argument of is its expected conclusion and is optional. If provided, as in this case, it is matched during proof checking against the actual (computed) conclusion, generating an error in case of a mismatch. This is useful for debugging.

3 Proof Checking With Ethos

In this section, we sketch a few details on the implementation of Ethos. We first focus on a description of the general process used by Ethos to check proofs, and then discuss some low-level aspects.

Proof Checking Model. Ethos is designed to be, first and foremost, a fast proof checker. This means that it omits some checks that might be convenient for the signature programmer but are not essential, i.e., their absence cannot lead to Ethos accepting invalid proofs. For example, Ethos does not fully check the types of programs when they are defined. Instead, it checks the monomorphic types of the ground terms that are generated when checking a proof.

For Ethos, checking a proof amounts to evaluating a proof term. Every rule is in fact a program with only one case. For example, the rule from above is internally translated to the following program.

Defines a type named Proof, a constant named pf that takes no arguments and returns a Boolean proof, and a program named contra that takes a Boolean proof as input and returns a Proof. The program contra uses a pattern matching expression: if pf applied to true returns a proof, then it returns that proof; otherwise, if pf applied to false returns a proof, it returns that proof. This code snippet illustrates a logical proof structure using Boolean values and pattern matching.

The earlier proof corresponds roughly to the term , where is the assumption . This term is considered a correct proof if Ethos can evaluate it to without error. Note that we use the symbols and here for illustration purposes; they are not built-in in Eunoia.

Ethos implements a function \(\mathtt {eval(}t, \sigma \mathtt {)}\), where t is a Eunoia term and \(\sigma \) is a grounding substitution over the parameters of t. It evaluates t bottom up, replacing each parameter x in it with \(\sigma (x)\). When \(\texttt{eval}\) encounters a term \((c\ u_1\ \cdots \ u_n)\), where c is a program with cases \([(p_1, b_1), \cdots , (p_m, b_m)]\), it invokes a helper \(\mathtt {match(} p_i, u_1\ \cdots \ u_n \mathtt {)}\) on each pattern \(p_i\) of c in order. If this function succeeds, it returns a substitution \(\sigma '\), and Ethos evaluates \(\mathtt {eval(}b_i, \sigma '\mathtt {)}\).

To ensure the conclusion of proof steps are not mistyped, Ethos can compute the type of parameter-free terms. This task is easier than general type checking because for the theories considered by Eunoia, all literals and constants have monomorphic types. Hence, computing types of applications amounts to pattern matching between the domain types and the monomorphic argument types. This approach has the benefit of being easy to implement, and optimize, at the expense of somewhat reduced statically checked guarantees.

Implementation. Ethos is written in C++, and currently has fewer than 10,000 lines of code. Terms are stored using a data structure with hash-consing (each unique AST is allocated exactly once) and reference counting on expressions. Number-like SMT-LIB literals (numerals, rationals, bit-vector constants) are stored in the AST using GMP arbitrary precision datatypes. Most built-in Eunoia operators on these literals translate directly to GMP functions. Ethos also implements the SMT-LIB policy for Unicode strings.

To accelerate proof checking, Ethos caches evaluation results. As mentioned, the evaluator takes as arguments a term to evaluate and a substitution, or context, mapping its free parameters to ground terms. The evaluator is implemented as a directed-acyclic graph traversal over terms. Since the evaluation primitives in Eunoia are stateless, Ethos can cache intermediate results in this process. This means that the result of invoking a side condition on a particular set of arguments is only computed once. However, this caching is not global, meaning that invoking the same computation on two independent proof steps will result in computing the result again. Ethos also evaluates parameter-free terms in rule and program bodies during parsing.

Since term construction is often the bottleneck, the core evaluation primitives on lists are optimized at a low level to minimize the number of terms that must be reallocated. For example, , which removes all occurrences of a particular element from a list, will reuse the tail of the list after the last occurrence of the element. To ensure the correctness of the optimized implementation, we cross-check these optimizations against a simpler reference implementation of the list operators as ordinary Eunoia programs. The Ethos regression set contains tests that ensure that the built-in evaluation matches the results of these reference implementations.

Finally, Ethos can be extended with plugins. These are modules that register callbacks with the main loop of Ethos. The callbacks notify the plugin when an event occurs, e.g., when a proof step is parsed. The plugin system can be used to implement custom external proof checkers, or converters to other proof formats.

Table 1. Evaluation on benchmark sets (1) and (2).Proofs are either fully checked (Verified), or have holes (Holey). For each case, the table shows the sum of the time in seconds to Generate a proof and to Check it. The last three columns count failures: no proof was generated, checking timed out, some other checking error occurred.
Full size table

4 Evaluation

The cvc5 solver supports three proof checking pipelines. It can produce proofs in the Alethe format which can be checked by Carcara. It can produce proofs in a calculus modeled in LFSC and checkable by the LFSC checker. Finally, it can produce proofs in its native calculus, called CPC, which is modeled in Eunoia and can be checked by Ethos. However, the support for cvc5 features differs significantly in these three pipelines. The Alethe proof format only supports uninterpreted functions, linear arithmetic, and quantifiers, and the LFSC calculus omits rules for many steps performed by cvc5. In those cases, the LFSC proof contains a step marked as . The Eunoia-based pipeline is the most complete. If cvc5 is run in safe mode, intended for users that require high assurance, the generated CPC proofs contains no holes (unjustified steps). An important factor in making this possible was the ease of writing proof rules in Eunoia.

To provide a perspective on the performance of Ethos, we compare the different proof production and checking pipelines of cvc5, and show that the Ethos pipeline is competitive with the other two, while also supporting more features (Table 1). We used all non-incremental SMT-LIB benchmarks [12] without floating-points that do not have status sat or have an inferredStatus of sat in the SMT-LIB catalog [14, 16]. To get a collection of benchmarks cvc5 could solve, we ran it for 60 s in safe mode with proof generation off.Footnote 2 This gave us a set of 161,188 benchmarks. We split this benchmarks set in two: (1) benchmarks in logics supported by Alethe, and (2) the rest. Set (1) contains 20,940 benchmarks. We then ran cvc5 for 600 s on these sets with proofs turned on, and afterwards each checker on the generated proofs for another 600 s. For Eunoia and Alethe, we used fine-grained proof rules for term rewriting steps, which are not supported by LFSC. This is the main reason for the large number of proof holes in LFSC proofs. Support for such rewrite rules is also experimental in Alethe. On commonly solved problems, Ethos is 6.25 times slower than Carcara.

As we gain experience using Ethos in practice, we expect to find more opportunities to improve its performance and usability. We also plan to focus on the support infrastructure around Ethos to make Eunoia easier to use. This includes the development of a standardized unit testing framework for Eunoia signatures, a documentation generator for proof rules, and a language server. One of our goals is to make Eunoia and Ethos robust and flexible enough to be a useful proof checking infrastructure for other SMT solvers and automated theorem provers.