Two Loops, One V-Model: Composing Process Governance and Formal Product Verification for Assurance of AI-Generated Software

Two independent research lines have converged on the same conclusion from opposite directions: code generated by large language models cannot be trusted on the generator's own account, and the remedy is structural — place the generator inside a loop whose other side it does not control. The formal-methods line, most recently Wei et al. (2026), closes a product loop: generated code is transformed into formal models and discharged through mechanical verifiers (Dafny, FDR4, Isabelle/HOL), with verification failures fed back as correction prompts until proof obligations close. The process-governance line, developed by this author, closes a process loop: every change is authored as a controlled instruction document, independently assessed by an agent with no codebase access, implemented by a third agent, and validated against the controlled record, with a human gatekeeper at every transition and a cumulative governance ledger converting failures into tenets. Neither loop subsumes the other. The product loop proves properties of the artefact but leaves the requirements unvalidated, the toolchain unqualified, and the change history ungoverned — Wei et al.'s own list of what certification additionally demands (process evidence, requirements validation, independence, configuration management) is precisely what the process loop provides. The process loop governs specification soundness and implementation fidelity but never mathematically proves the deployed artefact's behaviour — precisely what the product loop provides. The two literatures do not currently cite each other's traditions: the formal-methods paper carries no process-quality references (no GAMP, no ISA, no change control), and the governance papers carried no formal-methods references. This paper closes that gap deliberately, in both directions. The synthesis is grounded in seven months of production evidence from a regime the formal-methods line does not yet have: 781 controlled instruction documents in 811 archived files (254,000 lines of specification against a current codebase of roughly 309,000 lines), a 297-entry governance ledger with a cumulative tenet register reaching T-40, and a review-arc record whose machine-countable core shows a shape stable under every defensible variant of the counting rule: median 2 review rounds in all variants, first-pass clearance a minority (16.7–20.9%), and a long tail to 7 rounds concentrated on the system's highest-consequence changes. In both regimes, first-pass adequacy is the exception rather than the rule, and both exhibit the same structural behaviours, independently engineered: monotonic defect-class collapse, generator-constraint discipline, and vacuity guarding. The paper maps both loops onto the GAMP 5 V-model, specifies the composed architecture in which a formal-verification stage slots into the governed pipeline as machine-generated qualification evidence, and states the composability conditions. Deposited artefacts. The derived per-instruction aggregate table for the clearance distribution (v7, the current table), the superseded v6 recording a corrected decision, the v1 table now load-bearing as the extraction script's self-test fixture, the hand-curated read-verified supplement, the extraction script, the packet builder, and both figures in vector form. The extraction script's docstring states the counting rule and its lineage; the rule-variant analysis, residue instrumentation and verification record are Appendix A of the paper. Verification. This paper was produced under the regime it describes and publishes its own closure record. The manuscript cleared a nine-round bilateral review arc at an air-gapped station (Leg A, 25 July 2026) and the archival statistics were independently re-derived at a third station with tree access (Leg B, 25 July 2026, CLOSED): output table byte-identical to the deposited copy, 21 of 21 published-figure pins verified, residue tiers reproduced, and sampled clearance rows read against the ledger text. Artefact checksums, the as-at census boundary and both legs' verdicts are printed in Appendix A.4 — a paper arguing that process evidence must accompany product evidence supplies its own.