A proof-carrying architecture for synthetic genetic logic circuits under stochastic temporal contracts
Abstract
Genetic design automation maps Boolean specifications to regulatory networks and DNA sequences, but a successful mapping does not establish the probability that every output remains correct over time. This paper presents Proof-Carrying Synthetic Biology (PCS-Bio), a formal architecture for acyclic genetic logic circuits operated under fixed inputs. An ideal checker connects Boolean equivalence, sequence and model provenance, local stochastic contracts, and any surrogate-to-target discrepancy bounds. Under explicit semantic and checker assumptions, these obligations imply a joint temporal refinement guarantee without assuming independence among molecular events. Assignment-specific sufficient cubes select the branches needed to prove each output value. This can reduce risk and delay accounting provided that the retained local contracts remain uniform over the physically present but logically masked inputs. The reported evaluation exercises three separate interfaces: an archived Cello execution with sequence reconstruction, a restricted exact rational checker for a synthetic finite-state instance, and diagnostic IEEE~754 binary64 replay. Across 60 deterministic Boolean formula graphs, slicing reduced the worst-assignment risk-charge sum in 55 cases and the maximum accounting delay in 54. These results concern proof accounting and selected implementation components. They do not establish an integrated sequence-bound temporal certificate or physical validation.
Related
- Synthetic genetic circuits that count developmental cues in plant roots
- Tertiary lymphoid structures in luminal gastrointestinal cancers: biological circuits, spatial architecture, and biomarkers in the perioperative immunotherapy era
- Information contracts determine what inverse perturbation benchmarks measure
- Statistical patterns in the Ethereum blockchain: Analysis of EOAs and smart contracts in ERC20 token network
- Distinct cadmium detoxicity response between rice cultivars carrying functional or loss-of-function OsHMA3 allele
BibTeX
@misc{ferdowsi2026proofcarrying,
title = {{A proof-carrying architecture for synthetic genetic logic circuits under stochastic temporal contracts}},
author = {Arman Ferdowsi and Laura Kovacs},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.38218},
eprint = {2609.38218},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.38218},
note = {CC BY-NC-ND 4.0},
}
RIS
TY - UNPB
TI - A proof-carrying architecture for synthetic genetic logic circuits under stochastic temporal contracts
AU - Arman Ferdowsi
AU - Laura Kovacs
PY - 2026
DA - 2026/09/27
PB - arXiv
DO - 10.48550/arxiv.2609.38218
UR - https://arxiv.org/abs/2609.38218
AB - Genetic design automation maps Boolean specifications to regulatory networks and DNA sequences, but a successful mapping does not establish the probability that every output remains correct over time. This paper presents Proof-Carrying Synthetic Biology (PCS-Bio), a formal architecture for acyclic genetic logic circuits operated under fixed inputs. An ideal checker connects Boolean equivalence, sequence and model provenance, local stochastic contracts, and any surrogate-to-target discrepancy bounds. Under explicit semantic and checker assumptions, these obligations imply a joint temporal refinement guarantee without assuming independence among molecular events. Assignment-specific sufficient cubes select the branches needed to prove each output value. This can reduce risk and delay accounting provided that the retained local contracts remain uniform over the physically present but logically masked inputs. The reported evaluation exercises three separate interfaces: an archived Cello execution with sequence reconstruction, a restricted exact rational checker for a synthetic finite-state instance, and diagnostic IEEE~754 binary64 replay. Across 60 deterministic Boolean formula graphs, slicing reduced the worst-assignment risk-charge sum in 55 cases and the maximum accounting delay in 54. These results concern proof accounting and selected implementation components. They do not establish an integrated sequence-bound temporal certificate or physical validation.
ER -