Model checking is a powerful verification technique, but it often suffers from the state space explosion problem. Combining model checking with simulation relations is one possible way to mitigate this problem. However, the integrated formal verification technique requires a plenty amount of manual effort, which is both time-consuming and prone to human error. This paper presents a support tool that automates the major steps of this verification process. The tool is implemented in Maude and leverages its meta-programming facilities to systematically verify the simulation relation for each state transition. It automates a complex sequence of verification commands and handles case splitting for states with associative-commutative properties. We demonstrate the tool’s practical effectiveness through a case study where we formally verify that the Alternating Bit Protocol is simulated by a more abstract protocol. The tool enhances the efficiency and reliability of the verification process by reducing manual intervention.