Verifying Chemical Reaction Networks with the Isabelle Theorem Prover

Molecular programming involves algorithmically controlling nanoscale devices to compute functions, create structures, and manipulate molecules to perform various tasks. Many programmed nanoscale devices have been successfully demonstrated in the laboratory with physical experiments. Some of the applications for these devices are safety critical, and thus require extensive verification for their correctness. Unfortunately, experiments and deployment of these applications require molecular device counts on the order of ten to the eighteenth power, making verification via model checking and simulation infeasible. Verification of these systems must therefore be accomplished through proof techniques independent of the number of devices in the system.Developing these proofs can be tedious and time-consuming. In this paper, we develop general proof constructs for a subclass of molecular programs that compute semilinear functions modeled by a stochastic chemical reaction network. These proof techniques are developed in Isabelle, an automated theorem prover, with resulting theory files packaged so that they can be reused.