We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.