When the Defect Is in the Specification: Trajectory-Level Validation of Generated Code Against a Published Formalism
Diego Gabriel Impieri · Zenodo (CERN European Organization for Nuclear Research) · 2026
Trajectory-level validation of generated code against a published formalism. An experience report on a case where a published, externally reviewed formalism served as a correctness oracle for code generated under contract. The reference implementation of a formal rewriting operator — 40 modules, 44 model calls — was produced entirely by a contract-governed generator, with no module written by hand, and the acceptance criterion was the reference trajectories published in the formalism's own appendices. Three results are reported. First, the generated system reproduces both reference trajectories step by step, including the selection decisions the formalism specifies and that cannot be inferred from the states reached. Second, a material negative control: two implementations of the same contract, indistinguishable in initial state, final state, number of steps, and candidate set with their energies, differing only in the identity of the first step's transformation — one correct, one not, and no aggregate metric separates them. Third, the claimed finding: of the four defects that survived automated verification, none was in the 391 statements generated by the model; all four were in the 30 contract signatures written by a person, and all four consist of mis-transcribing a definition of the formalism that was available. The generation regime employed is the state of the art in specification-driven development and is not claimed as a contribution; trace comparison against formal specifications is an established technique and is likewise not claimed; the general observation that residual defects lie in the human specification is empirically established and is cited as prior work. What the report claims is the narrowed case: under an oracle fixed before the experiment and applied at the trajectory level, the surviving defects were erroneous transcriptions of numbered definitions rather than ambiguity. Limitations are stated in full: two instances, one formalism, one writing model, one human operator who is also the author of the formalism. The work is a self-evaluation with a declared conflict of interest, and its conclusions are illustrative rather than generalizable.