Measurement-based quantum computation (MBQC) is a key paradigm for quantum computing, offering advantages in blind quantum computation, for example. However, guaranteeing the correctness of MBQC protocols is challenging due to the inherent nondeterminism of quantum mechanics. Formal verification is therefore needed to provide systematic assurance. We propose an automated verification framework for MBQC. Our method formalizes MBQC using the Measurement Calculus (MC) and implements it in Maude, an algebraic specification language. We represent quantum states and operations symbolically using Dirac notation, enabling exhaustive exploration of all computational paths by rewrite-based reduction rather than direct matrix calculation. We use fidelity to automatically verify that the final quantum state is the desired state. In case studies, we successfully verified seven MBQC protocols.