Reusing Proofs when Program Verification Systems are Modified Bernhard Beckert, Thorsten Bormer, and Vladimir Klebanov In this position paper, we describe ongoing work on reusing deductive proofs for program correctness when the verification system itself is modified (including its logic, its calculus, and its proof construction mechanism). We build upon a method for reusing proofs when the program to be verified is changed, which has been implemented within the KeY program verification system and is successfully applied to reuse correctness proofs for Java programs.