One of the main factors of the increasing power of deductive verifi- cation 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. In this paper, we describe how we integrated a translation of proof obligations to Z3 (There …) with the replay of proof transcripts reported by Z3 inside KeY (… and Back Again). We describe the conceptual and the engineering challenges we encountered for this round trip and present solutions for them. The replay technique has been implemented in KeY, and in the evaluation, we demonstrate the feasibility of the approach for first- order proof instances and investigate the effects of proof replay on the proof run time and size.