Better SMT proofs for certifying compliance

Haniel Barbosa (U Federal de Minas Gerais)

Abstract: SMT solvers can be hard to trust, since it generally means assuming their large and complex codebases do not contain bugs that lead to wrong results. Machine-checkable certificates, via proofs of the logical reasoning the solver has performed, address this issue by decoupling confidence in the results from the solver’s implementation. Despite previous work, in several SMT solvers, to produce and check proofs, users still have to choose among solvers that may not produce fine-grained proofs, may not produce proofs for some of their crucial-for-efficiency components, or have proofs that are checkable only as part of a specific proof assistant. To facilitate the use of SMT proof certificates, the cvc5 developers team has completely redesigned its proof-production infrastructure, aiming for a sufficiently general and extensible infrastructure to allow: the generation of coarse- and fine-grained proofs for all parts of the solver, particularly for previously unsupported components such as the rewriter and the strings subsolver; and the printing of proofs in different formats to enable the use of different proof checkers. Specifically, we are working on producing cvc5 proofs for LFSC, Isabelle/HOL, Lean4, and Coq, while also creating proof calculi for previously unsupported SMT-LIB theories in these settings. While the project is still ongoing, we will report on significant progress on all of these fronts.