Lean Certified Bitvector Solving without Bitblasting

Abstract

Satisfiability Modulo Theories (SMT) solvers are the main working horse in many applications of automated reasoning. Unfortunately, they are frequently exposed to produce incorrect results. Trust in their results can be regained by producing proof certificates that are proof-checked within a trusted codebase. However, certificate size as well as proof-checking time of existing SMT proof checking approaches can be excessive. We introduce a new scheme of twinning an untrusted solver and a trusted proof checker using the same solving procedure, in which proof certificates produced by the solver act as an oracle for the proof checker. We have implemented our approach in two new tools, Roole (the untrusted solver, written in Rust) and Roolean (the trusted proof checker, written in Lean), using simplified Three-Valued Abstraction Refinement (TVAR) instead of bitblasting. Our approach yields small certificates and produces trusted results in reasonable time for the majority of quantifier-free bitvector benchmarks in SMT-LIB that are claimed to be unsatisfiable. Index Terms—SMT solving, interactive theorem provers, certifying oracles, three-valued bitvector domain