Reconstructing z3 proofs in KeY: there and back again
Wolfram Pfeifer, Jonas Schiffl, Mattias Ulbrich · 2021
One of the main factors of the increasing power of deductive verification tools are modern SMT solvers. Unfortunately, SMT solvers usually do not produce proof artifacts that could be inspected or checked. KeY is a formal platform for the deductive verification of Java programs which produces explicit, browsable proofs. SMT solvers can be driven from within KeY, but this unfortunately breaks these proof transparency intentions.