PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex produces a stepper. It also provides support for building a test suites from the specification of a semantics.

PLT Redex is embedded in PLT Scheme, meaning all of the convenince of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.

Getting started: PLT Redex is available via PLaneT. To install and use it, evaluate this in DrScheme:

Scholarly paper: A paper on an early version of PLT Redex appeared at the International Conference on Rewriting Techniques and Applications (RTA) in 2004. Beware: the notations are different now (and the feature set was much smaller back then).