<div class="csl-bib-body">
<div class="csl-entry">Onderka, J., Biere, A., & Fleury, M. (2026). Lean Certified Bitvector Solving without Bitblasting. In B. Dutertre & B. Könighofer (Eds.), <i>Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026</i> (pp. 147–154). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_20</div>
</div>
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
en
dc.language.iso
en
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.title
Lean Certified Bitvector Solving without Bitblasting
