In this ACG meeting, we present our approach to medeling and verification of Reo circuits using process specification language mCRL2 and the corresponding model checking toolset. We start from the encoding of Reo in mCRL2 according to its constraint automata semantics, and then discuss several lines of ongoing work on more expressive encodings, icluding the encoding of intentional automata and colouring semantics to support context dependency. Finally, we present our ideas about semantics for Reo that distinguishes handshaking mechanism from data flow and allows us to specify behavior of Reo circuits in presence of data transmission delays.