bioRxiv Science⌕ Search
Home/Archive/bioRxiv

bioRxiv · 10.1101/2022.04.08.487709

From Specification to Implementation: Assume-Guarantee Contracts for Synthetic Biology

Pandey, A.·Incer, I.·Sangiovanni-Vincentelli, A.·Murray, R. M.
View original source ↗Export metadata ↓

Abstract

We provide a new perspective on using formal methods to model specifications and synthesize implementations for the design of biological circuits. In synthetic biology, design objectives are rarely described formally. We present an assume-guarantee contract framework to describe biological circuit design objectives as formal specifications. In our approach, these formal specifications are implemented by circuits modeled by ordinary differential equations, yielding a design framework that can be used to design complex synthetic biological circuits at scale. We describe our approach using the design of a biological AND gate as a motivating, running example.

Explore related subjects

synthetic biologyPreprint

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Pandey, A., Incer, I., Sangiovanni-Vincentelli, A., Murray, R. M.. 2022-04-11. From Specification to Implementation: Assume-Guarantee Contracts for Synthetic Biology. https://doi.org/10.1101/2022.04.08.487709

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related preprints

bioRxiv2026

Living electronic transistors with tunable conductivity

Electroactive bacteria, like Shewanella oneidensis, can couple the oxidation of organic electron donors to the reduction of external conductive surfaces, such as minerals and electrodes, by utilizing multiheme cytochromes to carry charge from within the cell to external surfaces. Additionally, multiheme cytochromes facilitate gateable, long-distance (micrometer-scale) redox conduction along the outer membrane and across multiple cells bridging electrodes. While electroactive microbes are being used to develop bioelectrochemical devices, there have been limited efforts to use synthetic biology to exert additional control over microbes serving as device components. Thus, this work implements an optogenetic biofilm patterning gene circuit and a small molecule sensor in S. oneidensis to simultaneously control cell deposition and cytochrome expression. This allows for photolithographic patterning of biofilms possessing tunable electrical properties controlled with small molecules. This system demonstrates tunable electrochemical activity, redox conduction, intrinsic biofilm conductivity, and negative differential transconductance as a function of cytochrome expression. Additionally, temperature-dependent measurements of this tunable biofilm conduction reveal changes in activation energy as a function of cytochrome expression. Through this combination of synthetic biology and electrochemistry, simultaneous control over biofilm geometry and conductivity sheds light on fundamental microbial electron transport processes, and it enables the construction of living electronic devices.

synthetic biology↗
bioRxiv2026

Evolutionary stabilisation of stressful metabolism via integrated biocomputing and essential-gene metabolic locking circuits

Synthetic genetic circuits enable microbial differentiation from growth to production, yet metabolic burden, imbalance and toxicity frequently drive strain degeneration. Yeast strains engineered to produce different terpene products exhibited divergent genetic responses to metabolic stresses, but commonly underwent progressive loss of induction of synthetic GAL regulatory circuits, either across the entire population or within subpopulations. Using di- and tri-input biocomputing circuits, the essential glutamine synthetase gene GLN1 was coupled to GAL induction, thereby enabling stabilisation and evolutionary adaptation of the synthetic genetic circuits and stressful heterologous terpene synthetic pathways. The integrated biocomputing and metabolic coupling circuit systems not only prevent strain degeneration but also enable interrogation of non-degenerative evolutionary shifts, providing a platform for metabolic engineering optimisation.

synthetic biology↗
bioRxiv2026

Unbiased and scalable reduction of diverse bacterial genomes

The genome is a complex, integrated system where the functions and regulatory interactions of its many components remain poorly understood. Genome minimization aims to reduce genomic complexity by removing non-essential elements to reveal the fundamental building blocks of cellular life. However, current minimization strategies are often slow and species-specific due to a reliance on prior information, and limited to producing single, isolated strains, which obscures the diverse ways a genome can adapt to large-scale DNA removal. Here we show the development and application of Stochastic Lineage-based Iterative Minimization (SLIM) a modular, high-throughput platform for unbiased genome reduction across phylogenetically diverse bacteria. We apply SLIM to generate a library of genome-reduced Escherichia coli lineages. We then interrogate the lineages, identifying both universal and lineage-specific transcriptional and translational reprogramming in response to deletions. We demonstrate that these expression dynamics drive environment-dependent fitness, allowing us to pinpoint a single gene deletion in one genome-reduced lineage as the driver of a measurable environmental growth defect. Beyond E. coli, we successfully deploy SLIM in phylogenetically distinct bacterial taxa to rapidly reduce the genomes of Shigella flexneri and Pseudomonas putida, distinct genus and order respectively from E. coli, without species-specific optimization. Our results establish a scalable, generalizable framework for navigating the vast landscape of minimized genomes, providing a powerful new tool for functional discovery and the rational design of synthetic genomic chassis.

synthetic biology↗