Contextual improvement is a directed form of contextual equivalence that ensures a reduction in the number of evaluation steps. We present ReCheck, an automated tool that verifies contextual improvement for foundational calculi (such as extensions of the \(\lambda \) -calculus) and higher-order functional programs across operational semantics defined by Felleisen’s evaluation contexts. ReCheck allows users to define syntax, evaluation, and refinement rules as rewriting systems called Term Evaluation and Refinement Systems (TERS). We implement the theory of TERS and the method for deriving contextual improvement proposed by Muroya and Hamana in the tool ReCheck. We demonstrate ReCheck ’s applicability by proving contextual improvement across diverse calculi and programs.