We present a way to enjoy the power of SAT and SMT provers in
without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in
. It is conceived in a modular way, in order to tame the proofs’ complexity and to be extendable. It can currently check witnesses from the SAT solver
and from the SMT solver
. Experiments highlight the efficiency of this checker. On top of it, new reflexive
tactics have been built that can decide a subset of
’s logic by calling external provers and carefully checking their answers.