Another challenge is to provide formal verification of the correctness of the designs. We remark that, although we have validated the behaviour of the components for all possible input configurations and verified that correct outputs are produced and in the correct order using simulation and simulation-based probabilistic model checking with PRISM, this does not amount to full verification. Asynchronous diagrams are represented using a variety of notations, see Fig. 5, and correspond to certain classes of (safe) Petri nets (Myers 2004) known as Signal Transition Graphs (STGs), representing the rise and fall of signals. Our designs are systems containing many molecules which exhibit stochastic behaviour. Firstly, one would need to show that our CRN designs meet the specification given as a Petri net, which would involve relating the two formally via a refinement relation, where one needs to relate structures with many molecules of a given a species to structures with at most one. This presents us with two major challenges: scalability and stochasticity. Scalability can be addressed using compositional verification, which has been developed for (non-probabilistic) process algebraic specifications of asynchronous circuits (Wang and Kwiatkowska 2007) (equivalent to STGs) and it would be interesting to see if they can be applied in this setting. However, no probabilistic extension of this approach is known. Another possibility is to capture stochasticity by employing stochastic Petri nets to model the designs as done for molecular walkers in Barbot and Kwiatkowska (2015), and then perform temporal logic verification using the tool Cosmos. Cosmos relies on an implementation of statistical model checking that exploits parallelism of the Petri net specifications and achieves greater scalability than PRISM.