In this talk, we first present an operational semantics for Reo in the style of Plotkin's SOS (Structured Operational Semantics). Next, we present a faithful translation of this semantics into Maude (a conditional term rewriting language). This, in turn, allows us to benefit from the tooling around Maude in order to animate and model check Reo circuits.