GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation

GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation

arXiv:2608.03588v1 [cs.PL] 4 Aug 2026

Corrado Priami Dipartimento di Informatica, Università di Pisa and Fondazione Start Attractor corrado.priami@unipi.it

Abstract

Introduction

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 workflowbisimulation 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 modelparametric: compatibility is a measurable property to test, not an assumption that language models automatically satisfy.

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 1

at each interface into an end-to-end semantic certificate.

complementary: it treats prompt interpretation and formalization as kernels, then relates their quotient behavior to generated programs and commit decisions.

Contributions. (1) We define an observerrelative 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 welldefined quotient kernels, and quotienting commutes with Kleisli composition. (3) We derive promptreplacement and workflow-bisimulation corollaries, plus guarded-commit safety. (4) We introduce a quotient total-variation metric and prove nonexpansiveness 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 semanticspreserving transformations Le-Cong et al. [2025]. GenOS makes such instability a quantified interface defect and shows how it propagates.

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, D(X) is the set of finitely supported probability distributions on X, and δx is the point distribution at x. A kernel K : X → D(Y ) has affine extension X K † (µ)(y) = µ(x)K(x)(y).

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.

x

For K : X → D(Y ) and L : Y → D(Z), sequential composition is (K ; L)(x) = L† (K(x)). A minimal pipeline has prompt sources P , contracts S, generated artifacts C, and observations O: Front

Gen

Obs

P −−−→ D(S) −−→ D(C) −−→ D(O). When validation depends on the contract, generd ation preserves the contract tag: Gen(s) is a distribution on S × C with first component s, and Obs : S ×C → D(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. The same kernels generate a PLTS. A configuration contains a control location, semantic value, context, and provenance trace. A model call steps to a

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

2

Layer

Typical equivalence

Local audit obligation

Intent

Same contract mass Same behavior mass Same verdict class Same abstract trace

Paraphrases formalize alike

Generate

Validation Control

contract relation is sRS s′

⇐⇒

∀c, c′ . cRC c′ ⇒ (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] and [c].

Syntax preserves behavior Tools distinguish selected classes Replacement is safe in context

Proposition 1 (Validator compatibility). If contract satisfaction is closed under (RS , RC ) and a validator is extensional, then the tagged validation kernel on S × C is compatible with the product equivalence. If its accept verdict is also sound, the resulting commit observation is both equivalence-preserving and safe.

Table 1: Semantic interfaces and their local compatibility obligations. distribution; deterministic parsing, communication, and commit rules step to point distributions. For example,

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.

sample

⟨generate(s), Γ, κ⟩ −−−−→ X Gen(s)(c) δ⟨check(s,c),Γ,κc⟩ . c

Compositional Certificates

Thus the kernel and operational views describe the same transition structure at different granularities.

Theorem 1 (Quotient kernel and commuting square). If K : X → D(Y ) is (RX , RY )-compatible, then K([x]) = (qY )# (K(x))

Observer-relative equivalence. Let RX be an equivalence on X and qX : X → X/RX its quotient map. The lifting to distributions compares probability mass on equivalence classes.

defines a unique kernel K : X/RX → D(Y /RY ). Moreover, for every µ ∈ D(X),

Definition 1 (Lifted equivalence). For µ, ν ∈ D(X), write µ RX ν iff, for every class E ∈ X/RX , µ(E) = ν(E). Equivalently, (qX )# µ = (qX )# ν.

† (qY )# K † (µ) = K (qX )# µ . Proof. Compatibility makes the definition independent of the representative x. For a class B ∈ Y /RY , P both sides equal x µ(x)K(x)(qY−1 (B)) after grouping the outer sum by RX -classes. Uniqueness follows because point distributions on quotient classes determine a kernel.

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.

Theorem 2 (Quotients commute with composition). Let K : X → D(Y ) and L : Y → D(Z) be compatible with (RX , RY ) and (RY , RZ ), respectively. Then K ; L is (RX , RZ )-compatible and

Definition 2 (Compatible kernel). A kernel K : X → D(Y ) is (RX , RY )-compatible when xRX x′ implies K(x) RY K(x′ ).

K ; L = K ; L.

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.

Proof. Apply Theorem 1 first to L† (K(x)), then to † K(x). The resulting pushforward is L (K([x])). Corollary 1 (End-to-end prompt replacement). If all layers of a GenOS pipeline are compatible and prompts p, p′ induce equivalent contract distributions, then the final observation distributions agree

Contracts and extensional validators. Let |= ⊆ S × C be target-language satisfaction. A useful 3

on every RO -class. Hence every equivalence-closed event A ⊆ O, including a commit event, has equal probability under p and p′ .

Repair, Iteration, and Provenance

This result separates syntax-level variation from observable semantic variation. Artifact probabilities may differ substantially; only class mass must be preserved.

A core workflow grammar is sufficient to expose iterative behavior:

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.

The configuration trace records events such as generated artifacts, checker results, diagnostics, and commits. Rules only append events.

W ::= generate(s) | check(s, c) | repair(s, c, d) | commit(s, c) | W ; W | repeat(W ).

Proposition 2 (Trace monotonicity). If ⟨W, Γ, κ⟩ → µ, every configuration in supp(µ) has a trace with prefix κ. Therefore provenance is monotone along every finite execution.

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.

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 An 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.

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 |= c mean that target artifact c satisfies contract s. A checker is sound when Check(s, c) = accept implies s |= c. The commit rule is guarded when only accepted pairs can reach commit(c).

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. Then Pr(no acceptance in the first n attempts) ≤ (1−p)n .

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.

Thus acceptance occurs almost surely if retries continue indefinitely; every artifact eventually committed is correct by Theorem 4.

Proof. The final transition into a committed state requires a preceding accept observation. Soundness converts this observation into s |= c; earlier stochastic choices are irrelevant.

Proof. By the chain rule, the probability of n consecutive failures is the product of their conditional probabilities. Each is at most 1−p, giving the bound. No independence premise is used.

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.

This theorem identifies what an empirical repair study should estimate: a history-uniform or historystratified 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 dis4

Theorem 8 (Finite-sample certificate). For a fixed input x and 0 < δ < 1, with probability at least 1 − δ, r b N (x)(E) − K(x)(E)| ≤ log(2m/δ) . max |K E 2N

tance dRX (µ, ν) = TV((qX )# µ, (qX )# ν), X |α(u) − β(u)|. TV(α, β) = 12 u

Theorem 6 (Non-expansiveness). (RX , RY )-compatible, then

If

K

For M tested input pairs, let dbj and dj be their empirical and population quotient total variations. If

is

dRY (K † µ, K † ν) ≤ dRX (µ, ν).

N≥

Proof. By Theorem 1, both outputs are obtained by applying the same quotient kernel K to the quotient inputs. Total variation contracts under every Markov kernel.

4mM m2 log , 2τ 2 δ

then |dbj −dj | ≤ τ simultaneously for every pair, with probability at least 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, each endpoint has ℓ1 error at most τ ; the reverse triangle inequality for ℓ1 gives total-variation error at most τ.

To diagnose imperfect layers, define their compatibility defect def(K) = sup dRY (K(x), K(x′ )). xRX x′

A defect of zero recovers exact compatibility. The next theorem turns interface defects into an end-toend error budget.

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 dependenceaware confidence method. For an observed empirical defect ηb, 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.

Theorem 7 (Additive robustness budget). For any kernel K : X → D(Y ), dRY (K † µ, K † ν) ≤ dRX (µ, ν) + def(K). For a chain K1 ; · · · ; Kn , the final P distance is at most the initial quotient distance plus i def(Ki ). Proof sketch. Match the common mass that (qX )# µ and (qX )# ν assign to each input class, coupling matched samples within that class. Their output quotient distributions differ by at most def(K). Unmatched quotient mass is at most dRX (µ, ν) 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.

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, . . . , n, define a certificate

Estimating Compatibility from Samples

C = (R0 , . . . , Rn ; ϵ0 ; η1+ , . . . , ηn+ ; δ; G),

For a black-box model, K(x) is estimated by repeated calls under a frozen model version, context, decoding policy, and tool environment. Let the b N (x) be output quotient have m classes and let K the empirical class distribution from N independent samples.

where Ri declares the observer at interface i, ϵ0 bounds the initial quotient distance, η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 5

Compatibility is necessary. Let xRX x′ and let a, b be distinct RY -classes. If K(x) = δa and K(x′ ) = δb , then K([x]) would have to be both δ[a] and δ[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.

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 − δ. Let A be any final event closed under Rn . For the original and replacement workflows, Pn Pr(A) − Pr′ (A) ≤ τ := min{1, ϵ0 + i=1 ηi+ } W

Events must be quotient-closed. Suppose aRY b and two pipelines output δa and δb . They are equivalent at the declared interface, yet the concrete event {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.

W

with probability at least 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 falseaccept event.

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.

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, resourceaware, and information-flow-aware—without treating them as interchangeable.

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. Nonexpansiveness is tight for an identity quotient kernel, and a layer defect can contribute its full value when representatives attain def(K). The additive budget is therefore a worst-case guarantee; tighter bounds require additional structure.

Executable Semantic Audit Sharpness and Failure Modes

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

The hypotheses above are not merely sufficient proof conveniences. Small finite counterexamples show why an audit must expose each of them. 6

Comparison Contract TV pA vs. pB pA vs. pF pA vs. pnear

0 0 .0500

Code TV

Verdict TV

Implementation Weak class Strong class Copy commit

< 1.5 · 10−16

< 6 · 10−17

< 8 · 10−17 .0275

< 3 · 10−17 .0050

Built-in copy Insertion copy In-place sort Descending Deduplicate Off-by-one

Table 2: Quotient total-variation distances. Tiny nonzero values are floating-point roundoff.

E1 E1 E1 E2 E3 E4

F1 F1 F2 F3 F4 F5

yes yes no no no no

Table 3: Exhaustive equivalence classes for six concrete programs.

audit implementation uses only the Python standard library and emits all reported numbers.

yields mutation-class mass 0.70 and is not declared equivalent.

Observers and programs. Six concrete functions implement: built-in sorted copy, insertionsort 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–4 over {−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.

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.9471 (mean 0.3435). A second 10,000-trial test checks TV(µK, νL) ≤ TV(µ, ν) + supx TV(Kx , Lx ); 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

Prompts and kernels. The prompt texts are: pA , “return a sorted copy and leave the input unchanged”; pB , “produce a nondecreasing permutation without mutating the argument”; and pF , 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.60, mutating-correct 0.15, descending 0.10, lossy 0.10, and partial-sort 0.05. A sound copy-sort checker commits only pure-correct programs. 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. The three equivalent prompts all yield commit probability 0.60 and identical rejection-class distributions, as predicted by Corollary 1. A near prompt places 0.05 mass on an in-place contract. The strong observer detects the new mutation behavior. Nevertheless, code-class distance is 0.0275 and verdict distance is 0.0050, both below the input distance 0.05 as required by Theorem 6. A fully in-place prompt

A robustness claim is meaningful only relative to an observation boundary. Let an observer be a map h : C → B from concrete executions to observable records. It induces cRh c′ exactly when 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 → B2 refines h1 : C → B1 when there exists a map r : B2 → B1 such that h1 = r ◦ h2 . Thus h2 retains at least the information exposed by h1 . Proposition 3 (Monotonicity under observer refinement). If h2 refines h1 , then Rh2 ⊆ Rh1 . Consequently, exact equivalence under h2 implies equivalence under h1 , but not conversely. For distributions, dRh1 (µ, ν) ≤ dRh2 (µ, ν). Proof. If h2 (c) = h2 (c′ ), applying r gives h1 (c) = h1 (c′ ). The quotient for h1 is therefore a further

7

coarsening of the quotient for h2 , and total variation cannot increase under the induced deterministic map.

Stage

Construction

Reported quantity

Tasks

Task, language, contract, observer

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 unittest 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.

Prompts

HumanEval, MBPP, formal tasks Paraphrases, formalizations, frame variants N frozen calls per prompt and model EvalPlus tests and sound tools where available Pairwise and joint bounds

Nondeterminism Control

and

Samples

Checking

Analysis

Repair

Agent

Fixed diagnostic templates and retry cap

Contract-class input distance

Empirical code-class distributions Verdict classes and commit events

Defects, distinguishing classes, budget Conditional success by failure history

Table 4: Protocol for testing a model-mediated GenOS pipeline.

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 ηP t , every T quotient-trace event differs by at most ϵ + t=1 η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 Evaluation

a

Model-Based

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. Prompt families. Each task should contain: (i) meaning-preserving lexical and syntactic paraphrases; (ii) natural-language and formal or semiformal versions of the same contract; and (iii) 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

8

Conclusion

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.

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.

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.

References Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc V. Le, and Charles Sutton. Program synthesis with large language models. arXiv preprint arXiv:2108.07732, 2021.

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.

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. Prompting is programming: A query language for large language models. In Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1946–1965, 2023.

Implications and Limitations A deployable certificate records the observers, model and tool identities, sample counts, confidence level, per-layer defects, composed bound, and commitguard 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 proofbased observers; FormalBench and EvalPlus are natural starting points Le-Cong et al. [2025], Liu et al. [2023].

Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021. Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 9

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, pages 68–79, 2023.

Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, ShingChi Cheung, and Cong Tian. Enchanting program specification synthesis by large language models using static analysis and program verification. arXiv preprint arXiv:2404.00762, 2024.

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, and Vikram Adve. Towards formal verification of large-language-model-generated code from natural language prompts. arXiv preprint arXiv:2507.13290, 2025. Naman Jain, Skanda Vaidyanath, Arun Shankar Iyer, Nagarajan Natarajan, Suresh Parthasarathy, and Sriram Rajamani. Jigsaw: Large language models meet program synthesis. In Proceedings of the 44th International Conference on Software Engineering, pages 1219–1231, 2022. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991. Thanh Le-Cong, Bach Le, and Toby Murray. Can large language models reason about program semantics? a comprehensive evaluation on formal specification inference. arXiv preprint arXiv:2503.04779, 2025. Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation. Advances in Neural Information Processing Systems, 36, 2023. Robin Milner. Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, 1999. Gordon D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60–61:17–139, 2004. Corrado Priami. Stochastic pi-calculus. The Computer Journal, 38(7):578–589, 1995. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995. Merlijn Sevenhuijsen, Khashayar Etemadi, and Mattias Nyberg. Vecogen: Automating generation of formally verified c code with large language models. arXiv preprint arXiv:2411.19275, 2024. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. arXiv preprint arXiv:2310.17807, 2024. 10

Related documents

• Toward Interactive Understanding of Code APIs#1116412
• SCOPE: Leveraging Subgoal Critiques for Code Generation#346586
• On the Viability of Requirements Generation From Code: An Experience Report#307076
• SEW: Self-Evolving Agentic Workflows for Automated Code Generation#141744
• CodeFlowBench: A Multi-turn, Iterative Benchmark for Complex Code Generation#144281