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.

翻译：暂无翻译