Since deterministic semantics is not accurate for low molecular populations, we additionally explored stochastic semantics. Visual GEC exports models to the probabilistic model checker PRISM, which then enables verification of the induced continuous-time Markov chain against temporal logic properties. This allows one to check that the circuits ensure the correct temporal ordering of the events, for example, for the Muller pipeline seen in Fig. 6, that the species in the first stage of the pipeline is present before the species in the second, i.e. with probability 1, and that the signal is eventually propagated to the end of the pipeline. PRISM implements numerical solution of the CME, which is exponential in the initial number of molecules and hence not scalable, and analysis based on stochastic simulation, which is time consuming. We thus additionally used an experimental implementation of the LNA within Visual GEC, based on Cardelli et al. (2015). As well as being capable of checking temporal logic properties (Cardelli et al. 2015; Bortolussi et al. 2016), the LNA can plot the species concentration over time together with standard deviation, and is fast and reasonably accurate even for low molecule counts. Moreover, compared to the deterministic semantics, LNA provides important information about stochasticity that may affect the robustness of the circuits, and which can be explored further with CME, stochastic simulation, or verifying that the circuit converges with probability 1 to a single value.