Paper deep dive
GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation
Corrado Priami
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:AI coding agents are stochastic workflows: prompts are interpreted, artifacts are sampled, validators produce observations, and orchestrators commit or repair. Small prompt or specification changes can therefore alter program-behavior distributions even when the texts appear synonymous. Existing systems evaluate correctness, but lack a compositional criterion for safely replacing a prompt, contract, generator, or program inside a complete agentic workflow. We introduce GenOS, a probabilistic operational semantics for this replacement problem. Each layer is modeled as a Markov kernel, and each interface carries an observer-relative equivalence. We prove that equivalence-compatible kernels descend to quotient classes and that quotienting commutes with distributional extension and sequential composition. Hence, equivalent prompts induce equal probabilities for all downstream equivalence-closed events, including verified commit. We also establish workflow bisimulation, guarded-commit safety under sound validation, total-variation non-expansiveness, and an additive robustness bound that attributes approximation error to individual pipeline layers. An executable insertion-sort audit instantiates the theory with natural-language paraphrases, a formal contract, six programs, two observers, and exhaustive execution on 121 inputs. Equivalent prompts yield identical code-class and commit distributions; a prompt assigning 5% probability to an in-place contract is distinguished by a mutation observer, while downstream distances remain within the predicted bound. Across 20,000 randomized finite-kernel trials, no exact or approximate law is violated. GenOS is model-parametric: compatibility is a measurable property to test, not an assumption about language-model behavior.
Tags
Links
- Source: https://arxiv.org/abs/2608.03588v1
- Canonical: https://arxiv.org/abs/2608.03588v1
Trouble viewing inline? Open PDF directly →
Full Text
43,465 characters extracted from source content.
Expand or collapse full text
GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation Corrado Priami Dipartimento di Informatica, Università di Pisa and Fondazione Start Attractor corrado.priami@unipi.it Abstract AI coding agents are stochastic programs: a prompt is interpreted, candidate artifacts are sampled, validators return observations, and an orchestrator commits or repairs. Small changes to a prompt or specification can therefore change a distribution of program behaviors even when the texts appear synonymous. Existing code-generation systems and benchmarks measure correctness, but do not provide a compositional criterion for when one prompt, contract, generator, or program may safely replace another inside a complete agentic workflow. We introduce GenOS, a probabilistic operational semantics for this replacement problem. Each layer is a Markov kernel and each semantic interface carries an observer-relative equivalence. Our main result proves that an equivalence-compatible kernel descends to quotient classes and that quotienting commutes with distributional extension and sequential composition. Consequently, equivalent prompts induce equal probabilities for every downstream equivalence-closed event, including verified commit. We further prove an operational workflow-bisimulation theorem, guarded-commit safety under sound validation, total-variation non-expansiveness, and an additive robustness bound that isolates approximation defects at individual pipeline layers. An executable insertion-sort audit instantiates the theory with natural-language paraphrases, a formal contract, six concrete programs, two program observers, and exhaustive execution on 121 inputs. Equivalent prompts have identical code-class and commit distributions; a prompt with 5% mass on an in-place contract is separated by a mutation observer while its downstream distances remain below the predicted bound. Twenty thousand randomized finite-kernel trials produce no violation of the exact or approximate laws. The framework is model-parametric: compatibility is a measurable property to test, not an assumption that language models automatically satisfy. Introduction A contemporary AI programming system is not a function from text to code. It is a workflow: interpret an instruction, retrieve context, sample one or more artifacts, execute tests or proof tools, repair failures, and decide whether to commit. Systems such as Jigsaw combine neural generation with program analysis and synthesis Jain et al. (2022); Clover, AutoSpec, and VeCoGen place formal checking inside iterative generation loops Sun et al. (2024); Wen et al. (2024); Sevenhuijsen et al. (2024); and prompt languages such as LMQL make model interaction and constraints programmable Beurer-Kellner et al. (2023). These systems expose a semantic problem that pass rates alone do not answer: When can one component of a stochastic code-generation workflow be replaced by another without changing the behavior observable at the end of the workflow? Textual equality is too strong and informal synonymy is too weak. “Return a sorted copy” and “produce a nondecreasing permutation without modifying the input” may denote the same contract. Two generators may assign different probabilities to syntactically distinct programs but the same mass to behavioral classes. A test suite may identify programs that a mutation-sensitive observer separates. A verifier can preserve safety even when the generator is unreliable, but only if the commit guard is connected formally to target-language truth. We propose GenOS (Generative Operational Semantics), a layered semantics in which prompts, contracts, code artifacts, validator outcomes, and workflow observations are linked by probability kernels. At each interface, an equivalence states what the next layer is allowed to forget. The central proof obligation is compatibility: equivalent inputs must induce equal mass on equivalent outputs. Compatibility yields a quotient kernel, and quotienting commutes with composition. This turns a local condition at each interface into an end-to-end semantic certificate. Contributions. (1) We define an observer-relative kernel semantics for prompt-driven code generation, including a probabilistic labelled transition system (PLTS) for generate–check–repair–commit workflows. (2) We prove the commuting quotient theorem: compatible kernels induce well-defined quotient kernels, and quotienting commutes with Kleisli composition. (3) We derive prompt-replacement and workflow-bisimulation corollaries, plus guarded-commit safety. (4) We introduce a quotient total-variation metric and prove non-expansiveness and an additive bound for approximately compatible layers. (5) We provide an executable finite audit with concrete Python programs, exhaustive observers, exact distributions, and randomized law checking. The aim is not to claim that a particular model is invariant to paraphrase. FormalBench, for example, reports substantial instability under semantics-preserving transformations Le-Cong et al. (2025). GenOS makes such instability a quantified interface defect and shows how it propagates. Related Work AI code generation and validation. HumanEval and MBPP established functional evaluation for code synthesis Chen et al. (2021); Austin et al. (2021); EvalPlus demonstrates that weak test suites induce overly coarse notions of correctness Liu et al. (2023). In GenOS, a test suite, prover, or analyzer is an observer whose discriminating power explicitly determines program equivalence. Jigsaw uses semantic post-processing Jain et al. (2022), while Clover, AutoSpec, VeCoGen, and recent formal-verification pipelines use generated annotations, proof obligations, and repair feedback Sun et al. (2024); Wen et al. (2024); Sevenhuijsen et al. (2024); Councilman et al. (2025). These systems motivate guarded workflows, but they do not state conditions under which equivalence at one pipeline layer is preserved by all subsequent layers. Prompts and formal specifications. LMQL gives prompts control flow and output constraints Beurer-Kellner et al. (2023). nl2spec maps natural language to temporal logic while exposing ambiguity for interactive correction Cosler et al. (2023). FormalBench evaluates specification consistency, completeness, and robustness Le-Cong et al. (2025). GenOS is complementary: it treats prompt interpretation and formalization as kernels, then relates their quotient behavior to generated programs and commit decisions. Operational and probabilistic semantics. Our transition-based view follows structural operational semantics Plotkin (2004); the lifting of equivalence to distributions follows probabilistic bisimulation and probabilistic automata Larsen and Skou (1991); Segala and Lynch (1995); Baier and Katoen (2008). Pi-calculus is structurally appropriate for communicating agents Milner (1999), but classical stochastic pi-calculus places rates on actions Priami (1995). Model calls instead expose uncertainty over which artifact is produced, motivating transitions to distributions over artifacts and successor configurations. Layered Generative Operational Semantics We use finite distributions; countable and measurable versions follow with standard kernel assumptions. For a set X, (X)D(X) is the set of finitely supported probability distributions on X, and δx _x is the point distribution at x. A kernel K:X→(Y)K:X (Y) has affine extension K†(μ)(y)=∑xμ(x)K(x)(y).K (μ)(y)= _xμ(x)K(x)(y). For K:X→(Y)K:X (Y) and L:Y→(Z)L:Y (Z), sequential composition is (K;L)(x)=L†(K(x))(K ;L)(x)=L (K(x)). A minimal pipeline has prompt sources P, contracts S, generated artifacts C, and observations O: P→(S)→(C)→(O).P FrontD(S) GenD(C) ObsD(O). When validation depends on the contract, generation preserves the contract tag: ^(s) Gen(s) is a distribution on S×CS× C with first component s, and :S×C→(O) Obs:S× C (O). Observations may record tests, proof results, diagnostics, repair requests, resource use, mutation, exceptions, or commit. Table 1 summarizes the proof obligation at each interface. The equivalences are not required to be identical across applications: a security audit can refine the code observer with information-flow events, while a cost audit can add time or token use to workflow observations. Layer Typical equivalence Local audit obligation Intent Same contract mass Paraphrases formalize alike Generate Same behavior mass Syntax preserves behavior Validation Same verdict class Tools distinguish selected classes Control Same abstract trace Replacement is safe in context Table 1: Semantic interfaces and their local compatibility obligations. The same kernels generate a PLTS. A configuration contains a control location, semantic value, context, and provenance trace. A model call steps to a distribution; deterministic parsing, communication, and commit rules step to point distributions. For example, ⟨(s),Γ,κ⟩→∑c(s)(c)δ⟨(s,c),Γ,κc⟩. generate(s), ,κ sample\\ _c Gen(s)(c)\, _ check(s,c), ,κ c . Thus the kernel and operational views describe the same transition structure at different granularities. Observer-relative equivalence. Let RXR_X be an equivalence on X and qX:X→X/RXq_X:X→ X/R_X its quotient map. The lifting to distributions compares probability mass on equivalence classes. Definition 1 (Lifted equivalence). For μ,ν∈(X)μ,ν (X), write μRX¯νμ\, R_X\,ν iff, for every class E∈X/RXE∈ X/R_X, μ(E)=ν(E)μ(E)=ν(E). Equivalently, (qX)#μ=(qX)#ν(q_X)_\#μ=(q_X)_\#ν. Program equivalence is deliberately parameterized by an observer. A return-value observer may equate a pure sort with an in-place sort; an observer that also records the post-state separates them. Contract equivalence can be defined extensionally by satisfaction over program classes, and prompt equivalence by the contract-class mass induced by Front. Definition 2 (Compatible kernel). A kernel K:X→(Y)K:X (Y) is (RX,RY)(R_X,R_Y)-compatible when xRXx′xR_Xx implies K(x)RY¯K(x′)K(x)\, R_Y\,K(x ). Compatibility is the semantic substitutability test for a layer. It is inspectable empirically by repeated sampling and classifying outcomes, or proved for deterministic front ends and symbolic transformations. Contracts and extensional validators. Let ⊧⊆S×C \; S× C be target-language satisfaction. A useful contract relation is sRSs′⟺∀c,c′.cRCc′⇒(s⊧c⇔s′⊧c′).sR_Ss ∀ c,c .\ cR_Cc (s c s c ). This definition says that equivalent contracts select the same accepted code classes, not necessarily the same syntax or proof obligations. A deterministic validator is extensional when its verdict and diagnostic class depend only on [s][s] and [c][c]. Proposition 1 (Validator compatibility). If contract satisfaction is closed under (RS,RC)(R_S,R_C) and a validator is extensional, then the tagged validation kernel on S×CS× C is compatible with the product equivalence. If its accept verdict is also sound, the resulting commit observation is both equivalence-preserving and safe. The proposition distinguishes two properties that are often conflated. Extensionality states that equivalent inputs receive equivalent observations; soundness states that acceptance implies semantic truth. Either can hold without the other. Compositional Certificates Theorem 1 (Quotient kernel and commuting square). If K:X→(Y)K:X (Y) is (RX,RY)(R_X,R_Y)-compatible, then K¯([x])=(qY)#(K(x)) K([x])=(q_Y)_\#(K(x)) defines a unique kernel K¯:X/RX→(Y/RY) K:X/R_X (Y/R_Y). Moreover, for every μ∈(X)μ (X), (qY)#(K†(μ))=K¯†((qX)#μ).(q_Y)_\# (K (μ) )= K ((q_X)_\#μ ). Proof. Compatibility makes the definition independent of the representative x. For a class B∈Y/RYB∈ Y/R_Y, both sides equal ∑xμ(x)K(x)(qY−1(B)) _xμ(x)K(x)(q_Y^-1(B)) after grouping the outer sum by RXR_X-classes. Uniqueness follows because point distributions on quotient classes determine a kernel. ∎ Theorem 2 (Quotients commute with composition). Let K:X→(Y)K:X (Y) and L:Y→(Z)L:Y (Z) be compatible with (RX,RY)(R_X,R_Y) and (RY,RZ)(R_Y,R_Z), respectively. Then K;LK ;L is (RX,RZ)(R_X,R_Z)-compatible and K;L¯=K¯;L¯. K ;L= K ; L. Proof. Apply Theorem 1 first to L†(K(x))L (K(x)), then to K(x)K(x). The resulting pushforward is L¯†(K¯([x])) L ( K([x])). ∎ Corollary 1 (End-to-end prompt replacement). If all layers of a GenOS pipeline are compatible and prompts p,p′p,p induce equivalent contract distributions, then the final observation distributions agree on every ROR_O-class. Hence every equivalence-closed event A⊆OA O, including a commit event, has equal probability under p and p′p . This result separates syntax-level variation from observable semantic variation. Artifact probabilities may differ substantially; only class mass must be preserved. Operational consequence. Relate two workflow configurations when they are at the same control location, their current values are equivalent, and their traces agree after quotienting recorded artifacts and observations. Each deterministic rule is matched by a point transition, and each stochastic rule is matched by compatibility. Theorem 3 (Workflow bisimulation). If every stochastic action kernel in two structurally identical GenOS workflows is compatible and deterministic rules respect the selected equivalences, the induced configuration relation is a probabilistic bisimulation. Consequently, the workflows assign equal probability to every equivalence-closed finite trace cylinder. The proof is by cases on the operational rules. The theorem supports local replacement inside loops and agent networks, not only a fixed acyclic pipeline. Guarded commitment. Let s⊧cs c mean that target artifact c satisfies contract s. A checker is sound when (s,c)= Check(s,c)= accept implies s⊧cs c. The commit rule is guarded when only accepted pairs can reach (c) commit(c). Theorem 4 (Safe commit). In a guarded workflow with a sound checker, every reachable committed artifact satisfies its associated contract, independent of the generator distribution and repair policy. Proof. The final transition into a committed state requires a preceding accept observation. Soundness converts this observation into s⊧cs c; earlier stochastic choices are irrelevant. ∎ The theorem does not claim completeness: correct programs may be rejected. It also exposes a key boundary. Tests or learned judges usually justify only a weaker, probabilistic soundness claim, whereas proof-producing or sound static tools can justify the premise directly. Repair, Iteration, and Provenance A core workflow grammar is sufficient to expose iterative behavior: W::= W::= (s)∣(s,c)∣(s,c,d) generate(s) check(s,c) repair(s,c,d) ∣(s,c)∣W;W∣(W). commit(s,c) W;W repeat(W). The configuration trace records events such as generated artifacts, checker results, diagnostics, and commits. Rules only append events. Proposition 2 (Trace monotonicity). If ⟨W,Γ,κ⟩→μ W, ,κ →μ, every configuration in supp(μ)supp(μ) has a trace with prefix κ. Therefore provenance is monotone along every finite execution. Trace monotonicity makes a compatibility claim auditable: the class labels and decisions used to justify replacement can be reconstructed from the run. Traces may be quotiented for privacy, provided the retained abstraction still contains the observations named by the certificate. Repair is a new model call conditioned on the rejected artifact and diagnostic. Let AnA_n be the event that attempt n is accepted, conditional on all earlier failures. A useful progress theorem requires a lower bound on conditional success, but not independence. Theorem 5 (Conditional repair progress). Suppose a sound guarded workflow retries after rejection and, for every history with no earlier acceptance, Pr(An∣¬A1,…,¬An−1)≥p>0 (A_n A_1,…, A_n-1)≥ p>0. Then Pr(no acceptance in the first n attempts)≤(1−p)n. (no acceptance in the first n attempts)≤(1-p)^n. Thus acceptance occurs almost surely if retries continue indefinitely; every artifact eventually committed is correct by Theorem 4. Proof. By the chain rule, the probability of n consecutive failures is the product of their conditional probabilities. Each is at most 1−p1-p, giving the bound. No independence premise is used. ∎ This theorem identifies what an empirical repair study should estimate: a history-uniform or history-stratified lower bound, rather than an unconditional average success rate that can hide repeated failure modes. Approximate Robustness Exact class-mass equality is often too strict for sampled models. Define the quotient total-variation distance dRX(μ,ν) d_R_X(μ,ν) =TV((qX)#μ,(qX)#ν), =TV((q_X)_\#μ,(q_X)_\#ν), TV(α,β) (α,β) =12∑u|α(u)−β(u)|. = 12 _u|α(u)-β(u)|. Theorem 6 (Non-expansiveness). If K is (RX,RY)(R_X,R_Y)-compatible, then dRY(K†μ,K†ν)≤dRX(μ,ν).d_R_Y(K μ,K ν)≤ d_R_X(μ,ν). Proof. By Theorem 1, both outputs are obtained by applying the same quotient kernel K¯ K to the quotient inputs. Total variation contracts under every Markov kernel. ∎ To diagnose imperfect layers, define their compatibility defect def(K)=supxRXx′dRY(K(x),K(x′)).def(K)= _xR_Xx d_R_Y(K(x),K(x )). A defect of zero recovers exact compatibility. The next theorem turns interface defects into an end-to-end error budget. Theorem 7 (Additive robustness budget). For any kernel K:X→(Y)K:X (Y), dRY(K†μ,K†ν)≤dRX(μ,ν)+def(K).d_R_Y(K μ,K ν)≤ d_R_X(μ,ν)+def(K). For a chain K1;⋯;KnK_1 ;·s ;K_n, the final distance is at most the initial quotient distance plus ∑idef(Ki) _idef(K_i). Proof sketch. Match the common mass that (qX)#μ(q_X)_\#μ and (qX)#ν(q_X)_\#ν assign to each input class, coupling matched samples within that class. Their output quotient distributions differ by at most def(K)def(K). Unmatched quotient mass is at most dRX(μ,ν)d_R_X(μ,ν) and can contribute at most that amount. Iteration gives the chain bound. ∎ The budget is actionable: prompt interpretation, retrieval, generation, validation, and repair can be audited separately. A large downstream drift must be explained by an upstream prompt distance or by one or more measured compatibility defects. Estimating Compatibility from Samples For a black-box model, K(x)K(x) is estimated by repeated calls under a frozen model version, context, decoding policy, and tool environment. Let the output quotient have m classes and let K^N(x) K_N(x) be the empirical class distribution from N independent samples. Theorem 8 (Finite-sample certificate). For a fixed input x and 0<δ<10<δ<1, with probability at least 1−δ1-δ, maxE|K^N(x)(E)−K(x)(E)|≤log(2m/δ)2N. _E| K_N(x)(E)-K(x)(E)|≤ (2m/δ)2N. For M tested input pairs, let d^j d_j and djd_j be their empirical and population quotient total variations. If N≥m22τ2log4mMδ,N≥ m^22τ^2 4mMδ, then |d^j−dj|≤τ| d_j-d_j|≤τ simultaneously for every pair, with probability at least 1−δ1-δ. Proof. Apply Hoeffding to each class frequency and union-bound over m classes, two endpoints, and M pairs. With coordinate error at most τ/mτ/m, each endpoint has ℓ1 _1 error at most τ; the reverse triangle inequality for ℓ1 _1 gives total-variation error at most τ. ∎ The independence condition concerns repeated sampling, not repair attempts in Theorem 5. If an API changes model versions or uses stateful caching, the audit must stratify runs or use a dependence-aware confidence method. For an observed empirical defect η η, Theorem 8 supplies an upper confidence value η+η^+; substituting η+η^+ into Theorem 7 yields a high-probability end-to-end certificate. A practical audit has five steps. First, declare the observational properties and resulting equivalence classes. Second, freeze or record the model, tools, decoding parameters, and context. Third, sample each proposed replacement pair and classify outputs. Fourth, estimate class distances and confidence bounds. Fifth, compose the upper bounds across the workflow and separately verify the soundness premise of any commit guard. A failed compatibility test is informative: its distinguishing class identifies the semantic behavior changed by the replacement. A Checkable Certificate Object The previous results can be packaged as a finite object that accompanies a proposed prompt, model, tool, or agent replacement. For a pipeline with interfaces 0,…,n0,…,n, define a certificate =(R0,…,Rn;ϵ0;η1+,…,ηn+;δ;),C=(R_0,…,R_n; _0; _1^+,…, _n^+;δ;G), where RiR_i declares the observer at interface i, ϵ0 _0 bounds the initial quotient distance, ηi+ _i^+ is a proved or high-confidence upper bound on layer i’s compatibility defect, δ is the joint statistical failure probability, and G records the justification for each commit guard. A guard entry may be sound, may provide a false-accept upper bound β, or may be explicitly unsupported. The certificate is independently checkable from class definitions, samples or proofs, and trace data; it need not reveal prompts or generated source if privacy-preserving class evidence is sufficient. Theorem 9 (Certificate soundness). Suppose every numerical assertion in C holds simultaneously with probability at least 1−δ1-δ. Let A be any final event closed under RnR_n. For the original and replacement workflows, |PrW(A)−PrW′(A)|≤τ:=min1,ϵ0+∑i=1nηi+ | _W(A)- _W (A) |≤τ:= \1, _0+ _i=1^n _i^+\ with probability at least 1−δ1-δ. If a commit guard is sound, its unsafe-commit probability is zero. If instead its false-accept event has probability at most β, unsafe commit has probability at most β. Proof. The event bound follows from Theorem 7, because total variation upper-bounds the probability difference of every measurable quotient event. The confidence statement is inherited from the simultaneous bounds. The guard clauses follow from Theorem 4, or by inclusion of unsafe commit in the false-accept event. ∎ The theorem clarifies three different outcomes. A robust and safe certificate has small τ and a sound guard. A robust but uncertified replacement has small τ but no checker-soundness argument: it behaves like the baseline but may reproduce its errors. A correct but non-robust system may commit only verified programs while paraphrases yield very different rejection, repair, latency, or cost traces. These dimensions should be reported separately. Certificate composition is modular. Two adjacent certificates can be concatenated when they use the same intermediate equivalence; their defect bounds add and their statistical failure probabilities combine by a union bound. Observer refinement is also checkable: Proposition 3 permits projection from a stronger certificate to a weaker observation boundary, but never the reverse. Consequently, a repository can maintain certificates at different assurance levels—for example, functional, frame-safe, resource-aware, and information-flow-aware—without treating them as interchangeable. Sharpness and Failure Modes The hypotheses above are not merely sufficient proof conveniences. Small finite counterexamples show why an audit must expose each of them. Compatibility is necessary. Let xRXx′xR_Xx and let a,ba,b be distinct RYR_Y-classes. If K(x)=δaK(x)= _a and K(x′)=δbK(x )= _b, then K¯([x]) K([x]) would have to be both δ[a] _[a] and δ[b] _[b]. No quotient kernel exists. In a code agent, this is exactly a semantics-preserving paraphrase that systematically changes the generated behavior class; composition cannot repair the missing local congruence. Events must be quotient-closed. Suppose aRYbaR_Yb and two pipelines output δa _a and δb _b. They are equivalent at the declared interface, yet the concrete event a\a\ has probabilities one and zero. Corollary 1 therefore cannot promise equality for observations that the equivalence intentionally erased. This is why source-string equality, exact diagnostic wording, or a particular proof term cannot be queried from a certificate that preserves only functional behavior. Extensionality and soundness differ. A checker that accepts every program is perfectly extensional under any program equivalence, but it is not sound. Conversely, a sound checker could expose irrelevant syntactic diagnostics and thereby fail extensionality. The first breaks safe commitment; the second breaks replacement while preserving correctness. Proposition 1 requires both properties only when both conclusions are desired. Hidden state must enter the configuration. If a model service changes behavior after previous calls, a purported map from prompt to output distribution is not a kernel on prompts alone. Adding model version, decoding state, retrieved context, tool state, and relevant trace history to Γ restores the Markov property. Omitting them can create spurious compatibility: two prompts agree in one call order but diverge after different histories. The quantitative constants are tight. Non-expansiveness is tight for an identity quotient kernel, and a layer defect can contribute its full value when representatives attain def(K)def(K). The additive budget is therefore a worst-case guarantee; tighter bounds require additional structure. Executable Semantic Audit We instantiate the definitions on insertion sort. The purpose is to exercise every semantic object exactly, not to estimate a production model’s quality. The audit implementation uses only the Python standard library and emits all reported numbers. Observers and programs. Six concrete functions implement: built-in sorted copy, insertion-sort copy, built-in in-place sort, descending sort, duplicate-removing sort, and an off-by-one insertion sort. We execute each on all 121 arrays of length 0–44 over −1,0,1\-1,0,1\. A weak observer records return values; a strong observer also records the post-state of the input. Under the weak observer, the two pure implementations and the in-place implementation are equivalent. Under the strong observer, the in-place implementation is separated, while the two pure implementations remain equivalent. This provides a concrete distinguishing context rather than an asserted semantic difference. Prompts and kernels. The prompt texts are: pAp_A, “return a sorted copy and leave the input unchanged”; pBp_B, “produce a nondecreasing permutation without mutating the argument”; and pFp_F, a formal pre/postcondition specifying nondecreasing order, multiset equality, and frame preservation. They induce different distributions over two syntactically distinct but equivalent copy-sort contracts. Their quotient contract distribution is the point mass on copy-sort. The two contract-specific generation rows differ at artifact level but assign the same masses to five program-property classes: pure-correct 0.600.60, mutating-correct 0.150.15, descending 0.100.10, lossy 0.100.10, and partial-sort 0.050.05. A sound copy-sort checker commits only pure-correct programs. Comparison Contract TV Code TV Verdict TV pAp_A vs. pBp_B 0 <1.5⋅10−16<1.5· 10^-16 <6⋅10−17<6· 10^-17 pAp_A vs. pFp_F 0 <8⋅10−17<8· 10^-17 <3⋅10−17<3· 10^-17 pAp_A vs. pnearp_near .0500 .0275 .0050 Table 2: Quotient total-variation distances. Tiny nonzero values are floating-point roundoff. Table 3 makes the role of the observer explicit. The checker is stricter than the weak return-value observer because the copy contract contains a frame condition. Implementation Weak class Strong class Copy commit Built-in copy E1E_1 F1F_1 yes Insertion copy E1E_1 F1F_1 yes In-place sort E1E_1 F2F_2 no Descending E2E_2 F3F_3 no Deduplicate E3E_3 F4F_4 no Off-by-one E4E_4 F5F_5 no Table 3: Exhaustive equivalence classes for six concrete programs. The three equivalent prompts all yield commit probability 0.600.60 and identical rejection-class distributions, as predicted by Corollary 1. A near prompt places 0.050.05 mass on an in-place contract. The strong observer detects the new mutation behavior. Nevertheless, code-class distance is 0.02750.0275 and verdict distance is 0.00500.0050, both below the input distance 0.050.05 as required by Theorem 6. A fully in-place prompt yields mutation-class mass 0.700.70 and is not declared equivalent. Randomized law checks. We additionally sample 10,000 pairs of distributions and random finite kernels of dimensions two through eight. No trial violates total-variation contraction; the largest observed output/input ratio is 0.94710.9471 (mean 0.34350.3435). A second 10,000-trial test checks TV(μK,νL)≤TV(μ,ν)+supxTV(Kx,Lx)TV(μ K,ν L) (μ,ν)+ _xTV(K_x,L_x); again there are no violations. These tests do not replace proofs. They validate the implementation, numerical conventions, and artifact tables, and make the reported case study independently reproducible. Observer Design and Refinement A robustness claim is meaningful only relative to an observation boundary. Let an observer be a map h:C→Bh:C→ B from concrete executions to observable records. It induces cRhc′cR_hc exactly when h(c)=h(c′)h(c)=h(c ). Return values, mutated state, exceptions, proof certificates, resource use, information-flow events, and tool calls can be included independently. This makes the abstraction explicit and reviewable rather than hidden inside a benchmark metric. Definition 3 (Observer refinement). Observer h2:C→B2h_2:C→ B_2 refines h1:C→B1h_1:C→ B_1 when there exists a map r:B2→B1r:B_2→ B_1 such that h1=r∘h2h_1=r h_2. Thus h2h_2 retains at least the information exposed by h1h_1. Proposition 3 (Monotonicity under observer refinement). If h2h_2 refines h1h_1, then Rh2⊆Rh1R_h_2 R_h_1. Consequently, exact equivalence under h2h_2 implies equivalence under h1h_1, but not conversely. For distributions, dRh1(μ,ν)≤dRh2(μ,ν).d_R_h_1(μ,ν)≤ d_R_h_2(μ,ν). Proof. If h2(c)=h2(c′)h_2(c)=h_2(c ), applying r gives h1(c)=h1(c′)h_1(c)=h_1(c ). The quotient for h1h_1 is therefore a further coarsening of the quotient for h2h_2, and total variation cannot increase under the induced deterministic map. ∎ This proposition gives a simple discipline for safety-critical audits: begin with the deployment observations and refine them until every property that can invalidate substitution is represented. A unit-test observer may equate two programs that agree on sampled inputs; adding exhaustive bounded executions, frame conditions, exceptions, or a sound verifier can split that class. A certificate produced under a coarse observer remains valid only for the coarse question. The insertion-sort audit below demonstrates the issue: return-only observation equates copying and mutating sorts, while the post-state observer separates them. Nondeterminism and Agent Control Real agents contain both probabilistic model calls and nondeterministic choices: a scheduler selects an agent, an orchestrator selects a tool, or a human chooses whether to retry. A fixed orchestration policy resolves these choices and induces the kernels used above. With unresolved choices, the semantics is a probabilistic automaton or Markov decision process rather than a Markov chain Segala and Lynch (1995); Baier and Katoen (2008). There are two useful certificate strengths. A policy-specific certificate proves compatibility for the deployed scheduler and tool-selection policy. A policy-robust certificate requires every enabled action to be matchable by an action with equivalent successor-class mass; this is the standard alternating form of probabilistic bisimulation. The latter implies replacement under every scheduler that respects the action interface. Event probabilities can then be bounded by taking the supremum or infimum over schedulers. This distinction matters for agentic code generation: a compatible generator does not compensate for an orchestrator that routes semantically equivalent diagnostics to different repair tools. For bounded repair horizons, Theorem 7 gives a conservative drift bound. If the initial prompt distance is ϵε, and each of at most T generation, validation, or repair actions has defect at most ηt _t, every quotient-trace event differs by at most ϵ+∑t=1Tηtε+ _t=1^T _t. Under exact action compatibility, Theorem 3 removes the dependence on T entirely: loops and interleavings preserve equivalence because the relation is an invariant of every transition, not a one-pass approximation. Protocol for a Model-Based Evaluation The finite audit establishes that the definitions, theorems, and implementation agree. A full model evaluation should test whether contemporary code models satisfy the local obligations. Table 4 defines an executable protocol that avoids conflating textual paraphrase invariance, functional correctness, and safe commitment. Stage Construction Reported quantity Tasks HumanEval, MBPP, formal tasks Task, language, contract, observer Prompts Paraphrases, formalizations, frame variants Contract-class input distance Samples N frozen calls per prompt and model Empirical code-class distributions Checking EvalPlus tests and sound tools where available Verdict classes and commit events Analysis Pairwise and joint bounds Defects, distinguishing classes, budget Repair Fixed diagnostic templates and retry cap Conditional success by failure history Table 4: Protocol for testing a model-mediated GenOS pipeline. Prompt families. Each task should contain: (i) meaning-preserving lexical and syntactic paraphrases; (i) natural-language and formal or semi-formal versions of the same contract; and (i) deliberately non-equivalent near misses, such as changing an in-place requirement, exception policy, numerical precondition, or complexity constraint. The third group is essential: a metric that declares both paraphrases and near misses equivalent has selected an inadequate observer. Artifact classification. Programs are first compiled and executed in a sandbox. Functional observations can combine reference tests with augmented suites such as EvalPlus Liu et al. (2023); frame, exception, and resource observations are recorded separately. When a formal specification and a sound tool are available, proof acceptance forms a distinct, stronger commit guard rather than being merged with test success. Syntactically different outputs are aggregated only after their observable behavior has been classified. Statistics and diagnosis. Each pair is reported with quotient total variation, a simultaneous bound from Theorem 8, and its distinguishing classes. Measuring these quantities at every interface localizes drift to interpretation, generation, validation, repair, or orchestration. Repair results are stratified by failure history, because an unconditional average does not establish Theorem 5’s premise. Decision rule. A replacement is certified for event family A only when the composed bound meets its tolerance and every event is quotient-closed. Safe commitment separately requires checker soundness; robustness and correctness are distinct claims. Implications and Limitations A deployable certificate records the observers, model and tool identities, sample counts, confidence level, per-layer defects, composed bound, and commit-guard evidence. It can cover functional behavior, mutation, exceptions, cost, or security, but only observations represented by its equivalences. The PLTS result supports local replacement inside generate–verify–repair loops and communicating agents; guarded safety remains an orthogonal obligation. The guarantees are conditional on well-chosen observers and proved or measured compatibility. Exact model kernels are unobservable, so empirical audits depend on frozen environments, confidence procedures, and adequate sampling. Nontermination and continuous artifact spaces require measurable quotients or subdistributions beyond the finite presentation developed here. Finally, the controlled audit validates the semantics rather than benchmarking an LLM. A model study should execute the stated protocol with paraphrase families, formalizations, repeated generations, and strong behavioral or proof-based observers; FormalBench and EvalPlus are natural starting points Le-Cong et al. (2025); Liu et al. (2023). Conclusion GenOS treats an AI coding workflow as a probabilistic program with auditable semantic interfaces. Compatible kernels commute with quotienting and composition; approximate defects form an explicit robustness budget; sound guards establish commit safety. The framework does not assume model invariance. It turns invariance into a local, testable obligation and composes the resulting evidence end to end. References J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. V. Le, and C. Sutton (2021) Program synthesis with large language models. arXiv preprint arXiv:2108.07732. Cited by: AI code generation and validation.. C. Baier and J. Katoen (2008) Principles of model checking. MIT Press. Cited by: Nondeterminism and Agent Control, Operational and probabilistic semantics.. L. Beurer-Kellner, M. Fischer, and M. Vechev (2023) Prompting is programming: a query language for large language models. In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation, p. 1946–1965. Cited by: Introduction, Prompts and formal specifications.. M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, A. Ray, R. Puri, G. Krueger, M. Petrov, H. Khlaaf, G. Sastry, P. Mishkin, B. Chan, S. Gray, N. Ryder, M. Pavlov, A. Power, L. Kaiser, M. Bavarian, C. Winter, P. Tillet, F. P. Such, D. Cummings, M. Plappert, F. Chantzis, E. Barnes, A. Herbert-Voss, W. H. Guss, A. Nichol, A. Paino, N. Tezak, J. Tang, I. Babuschkin, S. Balaji, S. Jain, W. Saunders, C. Hesse, A. N. Carr, J. Leike, J. Achiam, V. Misra, E. Morikawa, A. Radford, M. Knight, M. Brundage, M. Murati, K. Mayer, P. Welinder, B. McGrew, D. Amodei, S. McCandlish, I. Sutskever, and W. Zaremba (2021) Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374. Cited by: AI code generation and validation.. M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel (2023) Nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, p. 68–79. Cited by: Prompts and formal specifications.. A. Councilman, D. J. Fu, A. Gupta, C. Wang, D. Grove, Y. Wang, and V. Adve (2025) Towards formal verification of large-language-model-generated code from natural language prompts. arXiv preprint arXiv:2507.13290. Cited by: AI code generation and validation.. N. Jain, S. Vaidyanath, A. S. Iyer, N. Natarajan, S. Parthasarathy, and S. Rajamani (2022) Jigsaw: large language models meet program synthesis. In Proceedings of the 44th International Conference on Software Engineering, p. 1219–1231. Cited by: Introduction, AI code generation and validation.. K. G. Larsen and A. Skou (1991) Bisimulation through probabilistic testing. Information and Computation 94 (1), p. 1–28. Cited by: Operational and probabilistic semantics.. T. Le-Cong, B. Le, and T. Murray (2025) Can large language models reason about program semantics? a comprehensive evaluation on formal specification inference. arXiv preprint arXiv:2503.04779. Cited by: Contributions., Implications and Limitations, Prompts and formal specifications.. J. Liu, C. S. Xia, Y. Wang, and L. Zhang (2023) Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation. Advances in Neural Information Processing Systems 36. Cited by: Artifact classification., Implications and Limitations, AI code generation and validation.. R. Milner (1999) Communicating and mobile systems: the pi-calculus. Cambridge University Press. Cited by: Operational and probabilistic semantics.. G. D. Plotkin (2004) A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60–61, p. 17–139. Cited by: Operational and probabilistic semantics.. C. Priami (1995) Stochastic pi-calculus. The Computer Journal 38 (7), p. 578–589. Cited by: Operational and probabilistic semantics.. R. Segala and N. Lynch (1995) Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2 (2), p. 250–273. Cited by: Nondeterminism and Agent Control, Operational and probabilistic semantics.. M. Sevenhuijsen, K. Etemadi, and M. Nyberg (2024) VeCoGen: automating generation of formally verified c code with large language models. arXiv preprint arXiv:2411.19275. Cited by: Introduction, AI code generation and validation.. C. Sun, Y. Sheng, O. Padon, and C. Barrett (2024) Clover: closed-loop verifiable code generation. arXiv preprint arXiv:2310.17807. Cited by: Introduction, AI code generation and validation.. C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S. Cheung, and C. Tian (2024) Enchanting program specification synthesis by large language models using static analysis and program verification. arXiv preprint arXiv:2404.00762. Cited by: Introduction, AI code generation and validation..