Appendix A · The Factory: A Formal Paper Built From Its Contract, With No Module Written By Hand

A deterministic architecture engine declares software architecture as verifiable constraints and confronts them against real code. Since August 2026 it also builds: given a contract carrying structures, signatures and flow, its factory`plane produces the complete system, with an external verifier rejecting whatever violates the contract that requested it. This appendix documents the run that shows the plane works. A published paper defining a rewriting operator over structural states — with a well-founded measure and four theorems — was declared as a contract of 40 modules across 8 planes and fabricated: one round of 35 model calls, 40 of 40 modules verified, none stuck, no module written or corrected by hand. Five contract corrections were applied across three refabrication rounds, nine calls; two of the five consumed no call at all. The resulting system reproduces both of the paper's appendix trajectories exactly — the primitive selected at each step, the energy that motivates the selection, and the measure after each application. Three conditions carried the result, and all three are transferable: the retry must see its own rejected code; the verifier must catch what compiles and does not work; and the contract must be sufficient rather than merely well-formed. Five classes of sufficiency are identified, each by the defect it would have prevented — declared delegation, object construction, the level at which each criterion of a formalism operates, the enumeration of closed sets, and unambiguous return semantics. What the contract contributes is measured rather than asserted: 391 executable statements written by the model against 30 prose signatures, every line of which is either a structural fact about the code or a transcription of a numbered definition from the paper. The appendix closes with a negative control. Two instances of the same system, built from contracts differing in one clause of one signature, converge to the identical final state in the identical number of steps, offering the identical candidate set with identical energies at the initial state — and traverse different paths. No aggregate metric distinguishes them; the defective one violates nothing, because every state it visits is legitimate and what is wrong is the choice among transformations that are all valid. Endpoints verify the existence theorems; only trajectories verify the dynamics.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-08-13
DOI
https://doi.org/10.5281/zenodo.21921913
Primary Topic
Security and Verification in Computing
Type
article
Field-Weighted Citation Impact
0.00
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Appendix A · The Factory: A Formal Paper Built From Its Contract, With No Module Written By Hand

Diego Gabriel Impieri
Zenodo (CERN European Organization for Nuclear Research)
Security and Verification in Computing
article

Appendix A · The Factory: A Formal Paper Built From Its Contract, With No Module Written By Hand

Diego Gabriel Impieri
article en

Abstract

A deterministic architecture engine declares software architecture as verifiable constraints and confronts them against real code. Since August 2026 it also builds: given a contract carrying structures, signatures and flow, its factory`plane produces the complete system, with an external verifier rejecting whatever violates the contract that requested it. This appendix documents the run that shows the plane works. A published paper defining a rewriting operator over structural states — with a well-founded measure and four theorems — was declared as a contract of 40 modules across 8 planes and fabricated: one round of 35 model calls, 40 of 40 modules verified, none stuck, no module written or corrected by hand. Five contract corrections were applied across three refabrication rounds, nine calls; two of the five consumed no call at all. The resulting system reproduces both of the paper's appendix trajectories exactly — the primitive selected at each step, the energy that motivates the selection, and the measure after each application. Three conditions carried the result, and all three are transferable: the retry must see its own rejected code; the verifier must catch what compiles and does not work; and the contract must be sufficient rather than merely well-formed. Five classes of sufficiency are identified, each by the defect it would have prevented — declared delegation, object construction, the level at which each criterion of a formalism operates, the enumeration of closed sets, and unambiguous return semantics. What the contract contributes is measured rather than asserted: 391 executable statements written by the model against 30 prose signatures, every line of which is either a structural fact about the code or a transcription of a numbered definition from the paper. The appendix closes with a negative control. Two instances of the same system, built from contracts differing in one clause of one signature, converge to the identical final state in the identical number of steps, offering the identical candidate set with identical energies at the initial state — and traverse different paths. No aggregate metric distinguishes them; the defective one violates nothing, because every state it visits is legitimate and what is wrong is the choice among transformations that are all valid. Endpoints verify the existence theorems; only trajectories verify the dynamics.

Zenodo (CERN European Organization for Nuclear Research)
Openalex Percentile: Top 7%
Security and Verification in Computing
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.