Hans-Jörg Schurr (Univ. of Iowa, USA)

Satisfiability Modulo Theories (SMT) solvers combine decision procedures for various theories into a homogeneous automated reasoning framework. They are an indispensable tools to solve formal verification and decision problems. To validate the SMT solver’s responses we can use proof certificates. However, a major challenge is that different theories and decision procedures use different proof calculi.

We will discuss the novel Eunoia language which allows SMT developers to define proof rules precisely. The syntax of Eunoia resembles the standard SMT-LIB format. Proofs using Eunoia-defined rules can be checked using the dedicated Ethos proof checker. We specified all proof calculus of the industrial strength SMT solver cvc5 in Eunoia. We will also discuss ongoing efforts to provide a formal and mechanized type system for Eunoia, and future directions for proof certificates for SMT solvers.