Tool support A number of software tools exist for examining the behaviour of CRNs. We employ Microsoft’s Visual GEC, which provides a programming language, LBS, for designing and simulating a given CRN under the deterministic or stochastic semantics, including also the LNA approximation of the stochastic semantics. The tool is capable of producing plots of expected or average species concentrations over time. This functionality is used extensively within this paper to validate our circuit designs. In addition, Visual GEC exports models to the probabilistic model checker PRISM (Kwiatkowska et al. 2011), which then enables verification of the induced continuous-time Markov chain against temporal logic properties. We use PRISM to verify the correctness of the temporal ordering of events occurring as the CRN circuit executes.