Execution gates and durable state [ftip-00HA]
✍️source

    Definition 1. An execution gate [ftip-00HB]

      An execution gate is a predicate \(g_i(e_i)\) over a recorded stage result \(e_i\). It names its owner, required inputs, pass/fail/unknown outputs, and the artifact versions to which the result applies.

      Definition 2. An ordered gate chain [ftip-00HC]

        An ordered gate chain is \((g_1,\ldots ,g_k)\) with stage outputs \(e_1,\ldots ,e_k\); gate \(g_i\) may execute only after its declared prerequisites and records a monotone status in \(\{pass,fail,unknown\}\).

        Theorem 3. A failed gate blocks a release conjunction [ftip-00HD]

          For a finite chain, define release status as \(G=\bigwedge _{i=1}^k g_i(e_i)\). If any gate is false, then \(G\) is false.

          Proof. 

            This is the defining conjunction of finitely many Boolean gate predicates. It says nothing about whether a later gate would have passed.

            Definition 4. A durable execution record [ftip-00HE]

              A durable execution record is

              \[d=(run,revision,environment,inputs,events,artifacts,checks)\]

              It is append-only, versioned, and sufficient to locate each gate input and output without relying on worker-local memory.

              Definition 5. A replay contract [ftip-00HF]

                A replay contract for \(d\) fixes the executable revision, environment image, input artifact hashes, seed law, and event order. A replay is faithful only when those coordinates are available and the resulting events satisfy the recorded schema.

                Theorem 6. Deterministic replay reproduces a recorded trace [ftip-00HG]

                  If the execution map is deterministic in the coordinates fixed by Definition 5, replaying the same inputs, revision, environment, and seed produces the same event trace.

                  Proof. 

                    Induct over the finite event sequence. Equal initial coordinates give equal first events; determinism and equal prefixes give the next event.

                    Example 7. Replayability is not correctness [ftip-00HH]

                      A reproducible run can deterministically reproduce a wrong patch or a misconfigured evaluator. Replay establishes trace identity under its contract; it does not establish that the trace met the intended utility or safety goal.

                      Definition 8. A state-integrity digest [ftip-00HI]

                        For durable record \(d\), let \(H(d)\) be a cryptographic digest of its canonical serialized fields. A replay request fails closed when the supplied record digest or any referenced input hash differs from the declared value.

                        To bind a replay result to an audit decision, the replay trace must be included in the audited record and covered by its digest. A matching digest for other fields does not bind that trace to the decision.

                        Remark 9. Scope of execution methodology [ftip-00HJ]

                          Part III of [jarmak2026reliable] motivates containment, durable execution, and recovery records. Deterministic replay and matching digests establish execution consistency; they do not ensure correctness.

                          References

                            Reference. Engineering Reliable Coding Agents: Evaluating and Operating the System Around the Model [jarmak2026reliable]

                            @article{jarmak2026reliable,
  title = {Engineering Reliable Coding Agents: Evaluating and Operating the System Around the Model},
  author = {Jarmak, Stephanie},
  year = {2026},
  url = {https://arxiv.org/abs/2608.13867v1},
  journal = {arXiv preprint arXiv:2608.13867}
}

                            Context

                              Reliability protocol and failure taxonomy [ftip-00GR]

                                A reliability protocol binds an evaluation to its durable state, replay inputs, and audit record. Execution and grading failures can invalidate a measurement even when the reported benchmark score improves.

                                Measurement and contamination controls [ftip-00GS]

                                  Convention. Evidence required for a reliability claim [ftip-00GT]

                                    Interpreting a reliability claim requires a named estimand, task and evaluation laws, artifact revision, inference protocol, evaluator version, sample rule, and failure policy. Missing coordinates are unknown rather than implicitly held fixed.

                                    Definition. Contamination record [ftip-00GU]

                                      For a candidate evaluation item \(z\), a contamination record is

                                      \[c(z)=(source,split,exposure,overlap,decision)\]

                                      The fields identify source provenance, split membership, prior agent exposure, overlap evidence, and the admission decision; an absent field is an explicit unknown.

                                      Definition. A contamination predicate [ftip-00GV]

                                        Given a contamination record \(c(z)\), write \(\operatorname {cont}(z)=1\) when its declared overlap or exposure rule rejects \(z\), and write \(\operatorname {cont}(z)=0\) when the rule clears it. The predicate belongs to the protocol, not to a model’s score.

                                        Definition. An uncontaminated evaluation slice [ftip-00GW]

                                          For an evaluation law \(\mathsf Q\), an admitted slice is \(\mathcal Z_0=\{z:\operatorname {cont}(z)=0\}\). Its reported score is conditioned on the declared slice law; removing contaminated items does not preserve the original estimand unless the law is unchanged by construction.

                                          Definition. A paired comparison design [ftip-00GX]

                                            A paired design fixes one evaluation law, one item order, and one sampling kernel for two artifacts, then records the paired difference from Definition [ftip-00FE]. Any item-level exclusion is applied before seeing the paired outcomes or is declared as an adaptive rule.

                                            Lemma. Pairing preserves the declared marginal target [ftip-00GY]

                                              Under a fixed nonadaptive slice and the iid coupling of Definition [ftip-00FE], the paired estimator remains unbiased for the two marginal scores in Theorem [ftip-00FF].

                                              Proof. 

                                                Condition on the fixed slice. The coupling has the stated marginals, so the proof of Theorem [ftip-00FF] applies without changing either expectation.

                                                Example. A contamination decision can change the estimand [ftip-00GZ]

                                                  If one paired run scores all ten items but a second run removes two items after inspecting outputs, the two means answer different questions. A report must expose the removal rule and the resulting slice law.

                                                  Remark. Scope of measurement methodology [ftip-00H0]

                                                    The measurement and paired-comparison guidance in [jarmak2026reliable], Part I, is a methodology source. It motivates contamination ledgers and matched comparisons; it supplies no universal contamination detector or statistical guarantee.

                                                    Grader calibration [ftip-00H1]

                                                      Definition. A typed grading rubric [ftip-00H2]

                                                        A grading rubric is \(R=(\mathcal Z,\mathcal L,g,v)\): outcome space, finite label set, scoring map \(g:\mathcal Z\to \mathcal L\), and evaluator version \(v\). The rubric declares which labels count as success and which observations are abstentions.

                                                        Definition. A grader response law [ftip-00H3]

                                                          For rubric \(R\), a grader response law is a kernel \(K(\ell \mid z)\) on \(\mathcal L\) given outcome \(z\). A deterministic grader is the point-mass case; stochastic or model-based graders must retain their version and sampling coordinates.

                                                          Definition. A calibration set [ftip-00H4]

                                                            A calibration set is a finite set \(\mathcal C\subseteq \mathcal Z\) with an adjudicated label \(y^star(z)\) for each \(z\in \mathcal C\). The adjudication source, disagreement policy, and release version are part of the set’s provenance.

                                                            Definition. Calibration agreement [ftip-00H5]

                                                              For grader kernel \(K\) and calibration set \(\mathcal C\), the agreement rate is \(A(K,\mathcal C)=|\mathcal C|^{-1}\sum _{z\in \mathcal C} K(y^star(z)\mid z)\). It is a calibration-set statistic, not a population accuracy claim.

                                                              Lemma. Agreement threshold admission [ftip-00H6]

                                                                If \(|\mathcal C|=n\geq 1\) and \(A(K,\mathcal C)\geq 1-\eta \), then the empirical disagreement mass \(1-A(K,\mathcal C)\) is at most \(\eta \).

                                                                Proof. 

                                                                  Rearrange the defining finite average in Definition [ftip-00H5]. No generalization beyond \(\mathcal C\) is implied.

                                                                  Example. High aggregate agreement can hide a subgroup failure [ftip-00H7]

                                                                    A grader that agrees on 99 of 100 easy cases but disagrees on the one safety case has overall agreement \(99/101\approx 0.9802\). Its agreement within the safety subgroup is zero. Any positive safety-subgroup agreement threshold therefore rejects this grader despite its high overall agreement. A calibration report stratifies by failure-relevant labels.

                                                                    Definition. A grader release gate [ftip-00H8]

                                                                      A grader release gate accepts \(K\) only when its calibration version, agreement thresholds, abstention handling, and stratified failure checks are recorded. A failed gate blocks interpretation of downstream score changes.

                                                                      Remark. Scope of grading methodology [ftip-00H9]

                                                                        Part II of [jarmak2026reliable] organizes grading and reviewer calibration practices. The finite agreement quantities do not establish a universal threshold or blinded-human reliability theorem.

                                                                        Execution gates and durable state [ftip-00HA]
                                                                        ✍️source

                                                                          Definition. An execution gate [ftip-00HB]

                                                                            An execution gate is a predicate \(g_i(e_i)\) over a recorded stage result \(e_i\). It names its owner, required inputs, pass/fail/unknown outputs, and the artifact versions to which the result applies.

                                                                            Definition. An ordered gate chain [ftip-00HC]

                                                                              An ordered gate chain is \((g_1,\ldots ,g_k)\) with stage outputs \(e_1,\ldots ,e_k\); gate \(g_i\) may execute only after its declared prerequisites and records a monotone status in \(\{pass,fail,unknown\}\).

                                                                              Theorem. A failed gate blocks a release conjunction [ftip-00HD]

                                                                                For a finite chain, define release status as \(G=\bigwedge _{i=1}^k g_i(e_i)\). If any gate is false, then \(G\) is false.

                                                                                Proof. 

                                                                                  This is the defining conjunction of finitely many Boolean gate predicates. It says nothing about whether a later gate would have passed.

                                                                                  Definition. A durable execution record [ftip-00HE]

                                                                                    A durable execution record is

                                                                                    \[d=(run,revision,environment,inputs,events,artifacts,checks)\]

                                                                                    It is append-only, versioned, and sufficient to locate each gate input and output without relying on worker-local memory.

                                                                                    Definition. A replay contract [ftip-00HF]

                                                                                      A replay contract for \(d\) fixes the executable revision, environment image, input artifact hashes, seed law, and event order. A replay is faithful only when those coordinates are available and the resulting events satisfy the recorded schema.

                                                                                      Theorem. Deterministic replay reproduces a recorded trace [ftip-00HG]

                                                                                        If the execution map is deterministic in the coordinates fixed by Definition [ftip-00HF], replaying the same inputs, revision, environment, and seed produces the same event trace.

                                                                                        Proof. 

                                                                                          Induct over the finite event sequence. Equal initial coordinates give equal first events; determinism and equal prefixes give the next event.

                                                                                          Example. Replayability is not correctness [ftip-00HH]

                                                                                            A reproducible run can deterministically reproduce a wrong patch or a misconfigured evaluator. Replay establishes trace identity under its contract; it does not establish that the trace met the intended utility or safety goal.

                                                                                            Definition. A state-integrity digest [ftip-00HI]

                                                                                              For durable record \(d\), let \(H(d)\) be a cryptographic digest of its canonical serialized fields. A replay request fails closed when the supplied record digest or any referenced input hash differs from the declared value.

                                                                                              To bind a replay result to an audit decision, the replay trace must be included in the audited record and covered by its digest. A matching digest for other fields does not bind that trace to the decision.

                                                                                              Remark. Scope of execution methodology [ftip-00HJ]

                                                                                                Part III of [jarmak2026reliable] motivates containment, durable execution, and recovery records. Deterministic replay and matching digests establish execution consistency; they do not ensure correctness.

                                                                                                Audit before commit and failure taxonomy [ftip-00HK]

                                                                                                  Definition. An audit-before-commit record [ftip-00HL]

                                                                                                    An audit-before-commit record is \(a=(d,scope,checks,reviewer,decision)\). It binds the durable execution record \(d\) to the audited scope, check list, review identity, and a decision in \(\{commit,hold,reject\}\).

                                                                                                    Theorem. Audit-before-commit safety gate [ftip-00HM]

                                                                                                      A commit decision is admissible only if every required check in an Definition [ftip-00HL] record is pass, the audited digest equals the proposed record digest, and the decision is \(commit\).

                                                                                                      Proof. 

                                                                                                        Admissibility is defined as the conjunction of these three recorded conditions; failure of any conjunct yields hold or reject.

                                                                                                        Definition. An independent audit scope [ftip-00HN]

                                                                                                          An audit is independent for scope \(S\) when its inputs are frozen before review, its reviewer or checker is distinct from the proposing action, and its decision cannot rewrite \(S\) without a new record. Independence is a protocol condition, not a claim of infallibility.

                                                                                                          Example. A latent failure caught before commit [ftip-00HO]

                                                                                                            A run may pass unit tests while an independent audit finds that the evaluator version in \(d\) differs from the declared version. The audit holds the commit and records the mismatch; replay alone would not have caught it.

                                                                                                            Definition. A reliability failure taxonomy [ftip-00HP]

                                                                                                              Classify a failed run by its earliest violated contract: measurement failure (M), grading failure (G), execution/state failure (E), audit failure (A), or transfer failure (T). A single run may receive secondary labels, but the primary label is the earliest failed gate in recorded order.

                                                                                                              Lemma. Earliest-failure labels are unique [ftip-00HQ]

                                                                                                                For a finite ordered gate chain with at least one failed gate, the earliest failed index is unique and therefore determines one primary taxonomy label.

                                                                                                                Proof. 

                                                                                                                  Every nonempty finite subset of ordered indices has a unique least element.

                                                                                                                  Definition. A remediation record [ftip-00HR]

                                                                                                                    A remediation record maps a primary label from Definition [ftip-00HP] to an owner, corrective action, re-test scope, and closure condition. Closure requires a new durable record and cannot mutate the failed record in place.

                                                                                                                    Remark. Scope of audit methodology [ftip-00HS]

                                                                                                                      Parts III and V of [jarmak2026reliable] motivate durable execution, review, and accountability practices. The audit taxonomy and conjunction gates are proposed operational specifications; they do not establish that an audit is complete or that a committed artifact is correct.

                                                                                                                      Audit budgets and the scope of run-level evidence [ftip-00HT]

                                                                                                                        Remark. A protocol is not a causal estimator [ftip-00HU]

                                                                                                                          The gates above make evidence auditable. They do not identify the causal effect of an intervention when task law, artifact, grader, budget, or harness state changes together. Those coordinates must be controlled in the matched evaluation of Definition [ftip-00GF].

                                                                                                                          Example. Counterexample: a perfect replay can repeat a contaminated result [ftip-00HV]

                                                                                                                            Let a deterministic run train and evaluate on one leaked item. Its digest, event trace, and replay are all identical across reruns, yet the measurement is contaminated under Definition [ftip-00GV]. Replayability and contamination control are independent obligations.

                                                                                                                            Example. Counterexample: a calibrated grader can still face a changed domain [ftip-00HW]

                                                                                                                              A grader can meet its threshold on \(\mathcal C\) in Lemma [ftip-00H6] while every deployment item lies outside that calibration domain and receives an unvalidated label. Agreement on \(\mathcal C\) alone does not transport to a new law.

                                                                                                                              Theorem. Budgeted audit admission [ftip-00HX]

                                                                                                                                If an audit plan has finite nonnegative stage costs and its declared sum is at most budget \(B\), then the plan is budget-admissible; adding any positive stage beyond the remaining slack makes it inadmissible.

                                                                                                                                Proof. 

                                                                                                                                  Apply additive cost monotonicity from Lemma [ftip-00GG].

                                                                                                                                  Example. A cost-balanced audit plan [ftip-00HY]

                                                                                                                                    With budget \(B=100\), a plan may allocate 50 units to execution, 30 to grading calibration, and 20 to audit. A proposed 10-unit extra audit must be funded by reducing another stage or the admission gate fails.

                                                                                                                                    Remark. What this protocol can establish [ftip-00HZ]

                                                                                                                                      A passing protocol establishes that declared evidence contracts, hashes, checks, and budgets were satisfied for the recorded run. It does not establish capability acquisition, broad generalization, or absence of unobserved faults.

                                                                                                                                      Backlinks

                                                                                                                                        Reference. Finite discovery, replay, and audit [ftip-00IV]

                                                                                                                                          Finite sampling is treated in § [ftip-0076], deterministic replay in § [ftip-00HA], and audit conditions in § [ftip-00HK].