  Formal methods have enabled breakthroughs in many fields, such as in hardware
verification, machine learning and biological systems. The key object of
interest in systems biology, synthetic biology, and molecular programming is
chemical reaction networks (CRNs) which formalizes coupled chemical reactions
in a well-mixed solution. CRNs are pivotal for our understanding of biological
regulatory and metabolic networks, as well as for programming engineered
molecular behavior. Although it is clear that small CRNs are capable of complex
dynamics and computational behavior, it remains difficult to explore the space
of CRNs in search for desired functionality. We use Alloy, a tool for
expressing structural constraints and behavior in software systems, to
enumerate CRNs with declaratively specified properties. We show how this
framework can enumerate CRNs with a variety of structural constraints including
biologically motivated catalytic networks and metabolic networks, and seesaw
networks motivated by DNA nanotechnology. We also use the framework to explore
analog function computation in rate-independent CRNs. By computing the desired
output value with stoichiometry rather than with reaction rates (in the sense
that $X \to Y+Y$ computes multiplication by $2$), such CRNs are completely
robust to the choice of reaction rates or rate law. We find the smallest CRNs
computing the max, minmax, abs and ReLU (rectified linear unit) functions in a
natural subclass of rate-independent CRNs where rate-independence follows from
structural network properties.
