Speed and correctness guarantees for programmable enthalpy-neutral DNA reactions

Abstract

Molecular control circuits embedded within chemical systems to direct molecular events have transformative applications in synthetic biology, medicine, and other fields. However, it is challenging to understand the collective behavior of components due to the combinatorial complexity of possible interactions. Some of the largest engineered molecular systems to date have been constructed from DNA strand displacement reactions, in which signals can be propagated without a net change in base pairs. For linear chains of such enthalpy-neutral displacement reactions, we develop a rigorous framework to reason about interactions between regions that must be complementary. We then analyze desired and undesired properties affecting speed and correctness of such systems, including the spurious release of output (leak) and reversible unproductive binding (toehold occlusion), and experimentally confirm the predictions. Our approach, analogous to the rigorous proofs of algorithm correctness in computer science, can guide engineering of robust and efficient molecular algorithms.