Context

SMT solving is a technique for determining the Satisfiability of formulas in first-order logic (FOL) Modulo background Theories, describing mathematical domains such as linear integer arithmetic (LIA), or describing data structures such as arrays (A) or bit-vectors (BV).

For example the formula ((x ^ (x >>s 31)) – (x >>s 31)) ≠ (x – (2*x & (x >>s 31)))) states that two different ways of calculating the absolute value of a bit-vector variable ‘x’ are not the same. This formula being satisfiable means that there is a value for ‘x’ which witnesses this difference. Using an SMT solver that can reason about bit-vectors one can show that this formula is unsatisfiable, which proves the two different ways of calculating the absolute value of a bit-vector are equivalent.

SMT solvers are versatile tools with many applications, in formal methods, software engineering and the automated verification of mathematics among other domains. Due to all these interesting applications, many efforts have been dedicated over the years to improve the performance and the range of application of SMT solvers, with state-of-the-art systems such as cvc5 with dedicate solving procedures for over ten theories.

A negative impact of these efforts is as follows. It has been observed that  research in SMT solving is currently hampered by how complex state-of-the-art tools have become. For example, cvc5, the leading SMT solver world-wide,  requires a dedicated team of five people for maintenance. Moreover, novel results often take a significant time to integrate or are not integrated at all to the solver simply because their components are so tightly interconnected that it requires too much time and effort to carefully consider how to upgrade a component of the system without affecting the performances of the other components.

In recent years, SMT solvers have even been extended to higher-order logic (HOL) , with the aim of improving in particular the automation of proof assistants, the tools that verify mathematical proofs and algorithms (such as Coq,  Isabelle/HOL or TLAPS). So far, the results of higher-order SMT have been mitigated, because although the core components of the solvers have been lifted, many others still operate solely in first-order logic.

The integration of SMT solvers to proof-assistants has raised another concern in the community, that of producing proof certificates when the solver terminates, that can be checked by the proof-assistant and eventually lead to a reconstruction of the proof found by the solver in the proof-assistant. The format in which SMT solvers should output proof certificates has been a hot topic of discussions in the SMT community in recent years. Interesting proposals such as the Alethe proof format have emerged and coexist in different solvers. An additional  benefit of certificates is that, by offering a way to check the results of a solver independently, they also strengthen the confidence that can be put in these solvers.

Objectives

This collaboration aims at improving the state of the art in SMT solving on three fronts.

• Our first objective is to counter the research slowdown created by the tight interconnection of parts in state-of-the-art SMT solvers. We will do this by creating a new SMT solver to act as a vessel for research, with a strong emphasis on modularity. Our goal is that all components can simply be plugged in and out to make it easy to upgrade and serve as a platform for comparison between different techniques. The tentative name of this new solver is ModulariT.
• Our second objective concerns higher-order SMT and the missing components to make it competitive. We are convinced that one of the missing key components is an efficient conflict-based instantiation technique for higher-order logic. We plan to provide this component for  ModulariT (that will be designed to operate on first- and higher-order logic from the start) by lifting the technique called “Congruence Closure with Free Variables” (CCFV) to HOL.
• Our third objective concerns the coexistence of various proof formats for SMT solving. We want more interoperability so that the various formats do not create a divide in the community. Specifically, our aim for this  collaboration will be to provide a tool for translating Alethe proofs originating from TLA specifications (extracted from the proof assistant TLAPS) to  Dedukti, a logical framework based on the λΠ-calculus modulo, in which many logics and theories can be expressed, that has become the  lingua franca of proof translation.