Paper deep dive
agent-risk: Risk Assessment for Changes to AI Agents
Yue Zhao, Zixiang Xu, Angela Huyue Zhang, S. Alex Yang, Xiyang Hu
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:Before changing a deployed AI agent (a stricter safety gate, a new model), organizations must approve the change, starting from existing logs. Extending classical risk analysis to partial records and partial changes to running systems, agent-risk replays logged episodes, assuming nothing else changes and the agent does not anticipate the change. The log settles episodes acting as before, a declared stop value settles stopped ones, and the rest need logged support, a saved-state rerun, or a bound. We prove what logs must record for exact replay and which saved states serve a gate family. For independent episodes, we bound the reruns a decision needs and tolerable drift from live behavior. In a bash sandbox, a 7,200-episode log alone decided neither of two retry gates, which let the agent act after refusals the log never shows. Rerunning only each gate's blocked episodes from saved states reached both live decisions at half the agent calls of a live test sized post hoc for them, given the log. Without per-step harm, a stopping gate's certified harm ceiling rose up to 2.5-fold, since the log hides whether harm preceded the stop. Approval thus needs evidence designed in advance: log fields, saved states, targeted reruns.
Tags
Links
- Source: https://arxiv.org/abs/2610.16280v1
- Canonical: https://arxiv.org/abs/2610.16280v1
Trouble viewing inline? Open PDF directly →
Full Text
227,774 characters extracted from source content.
Expand or collapse full text
agent-risk: Risk Assessment for Changes to AI Agents Yue Zhao Affiliation: University of Southern California Email: yue.z@usc.edu Zixiang Xu Affiliation: University of Southern California Email: zixiangx@usc.edu Angela Huyue Zhang Affiliation: University of Southern California Email: azhang@law.usc.edu S. Alex Yang Affiliation: London Business School Email: sayang@london.edu Xiyang Hu Affiliation: Arizona State University Email: xiyanghu@asu.edu Abstract Before changing a deployed AI agent (a stricter safety gate, a new model), organizations must approve the change, starting from existing logs. Extending classical risk analysis to partial records and partial changes to running systems, agent-risk replays logged episodes, assuming nothing else changes and the agent does not anticipate the change. The log settles episodes acting as before, a declared stop value settles stopped ones, and the rest need logged support, a saved-state rerun, or a bound. We prove what logs must record for exact replay and which saved states serve a gate family. For independent episodes, we bound the reruns a decision needs and tolerable drift from live behavior. In a bash sandbox, a 7,200-episode log alone decided neither of two retry gates, which let the agent act after refusals the log never shows. Rerunning only each gate’s blocked episodes from saved states reached both live decisions at half the agent calls of a live test sized post hoc for them, given the log. Without per-step harm, a stopping gate’s certified harm ceiling rose up to 2.5-fold, since the log hides whether harm preceded the stop. Approval thus needs evidence designed in advance: log fields, saved states, targeted reruns. 1 Introduction AI agents now act for organizations, answering customers and writing and running code (ElevenLabs, 2026; Cursor, 2026). The institutions that absorb the risk of these actions (insurers, certifiers, deployment approvers, and courts that allocate liability) need a stated loss, evidence, and uncertainty before the agent acts. Insurability and premium follow technical due diligence (Munich Re, 2023), whereas one provider separated development from production databases only after a coding agent deleted production data (Masad, 2025). We call the organization that runs an agent and holds its logs the deployer. Take a coding agent whose tool calls pass a monitor (a second model scoring each call’s risk) and a gate, which uses the score to run the call, stop the episode, or refuse the call so the agent retries. The deployer keeps changing such an agent, tightening the gate or releasing a new model. Before a change runs, the deployer, or an insurer or auditor with its logs, faces one question: how much of its risk do existing logs establish (Figure 1)? Logs (per-step records of tool calls, monitor scores, and outcomes) come first because they are already in hand: a live trial exposes users to the risk under assessment, and a new test campaign costs runs and may not match deployment. Figure 1: Replaying a logged episode under a proposed change. With sufficient records, the log gives the agreeing case and a declared stop value the stopped case; a snapshot run, logged support, or bounds the continuing case. Six characteristics (§2.1) make this question hard for AI (e.g., LLM) agents (Table 1): 1 approval gates, 2 partial records, 3 long horizons, 4 model releases, 5 shared state, and 6 oversight cues, signs that the agent is being tested. Current Gaps. Benchmarks and control evaluations run and score a given system (Yao et al., 2025; Kwa et al., 2025; Greenblatt et al., 2024). Some also reuse logged monitor scores to set audit thresholds and resample actions (Bhatt et al., 2025; Inglis et al., 2025); we state when such replay is valid. Off-policy evaluation (Horvitz and Thompson, 1952; Precup et al., 2000), optimal stopping (Goel et al., 2017), and partial identification (Manski, 2003) ask what logs of the current system imply about a changed one, but a stricter gate’s stops never occur in the log, and a retry gate lets the agent act after a refusal no log contains. We specialize these tools to agent changes and add evidence design: which logged fields, saved states, and new runs certify a decision about a change. Our framework, agent-risk, replays each logged episode (Li et al., 2011): on the recorded inputs, without executing new environment steps, it recomputes the new rule’s actions up to the first deviation, where the two rules first differ, and sorts it into the three cases of Figure 1; a continuing case may need new runs from a saved sandbox state (a snapshot). The key contributions are: • Problem Formulation (Section 2): We formalize the risk of an agent change before it runs as a specification that extends scenario risk analysis (Kaplan and Garrick, 1981) with partial records and admissible changes, guided by six agent characteristics (Table 1), and ask which risk values the logs leave possible (partial identification). • Theoretical Results (Section 3): We prove (i) exactly what a log must record to settle agreeing and stopped episodes for any current system; (i) for independent episodes, a lower bound on the reruns needed to certify a harm level, tests that approach it asymptotically, and the restoration error beyond which no valid test certifies reliably; and (i) the fewest saved states, among those where a gate first acts, serving a whole threshold family. • Empirical Verification (Section 4): To test these results against paired live runs in a bash sandbox, we reran only what one log left open (targeted execution), which predicted two retry gates’ harm within the registered margin of 0.015 and reached the live decision on both, which the log alone could not. Clean starts in a shared workspace and an announced gate mispredicted live runs (Table 2). In all, 16 runs log about 49,000 episodes. • Reproducibility and Access: We release a Python package for replay, harm bounds, and logging comparisons, and scripts that check the formal results on finite instances (Appendix H); the harness, logs, and registrations are available from https://github.com/yzhao062/agent-risk. Characteristic (where it enters) What the logs can establish 1 Approval gates (execution) Stricter stopping gates: replay plus a declared stop value (§3.1). Retry gates: similar logged cases, reruns, or bounds (§3.4) 2 Partial records (records) Replay is exact only if the log keeps each episode’s contribution, e.g., harm timing relative to a stop (§3.2) 3 Long horizons (execution) Stopping changes replay at any length; for continuing ones, the share that agrees can stay the same or fall (§3.3) 4 Model releases (admissible changes) A new model rerun on logged inputs and seeds settles episodes where it acts as logged; the rest need similar cases, reruns, or bounds (§3.4) 5 Shared state (execution) With the shared state’s law known, single-agent tests bound joint risk; reruns from saved shared state settle it (§3.5) 6 Oversight cues (execution) Results carry over only for cues seen in testing; an agent told of the gate can act differently, breaking (A2) (§3.6) Table 1: Six organizing agent characteristics and what logs can establish under each. Characteristic k enters the part of the risk specification (Section 2.3) in parentheses; its result is in Section 3.k and demonstration in Section 4.k. 2 Problem Formulation 2.1 Six Organizing Characteristics of Agents Six characteristics make a change’s risk hard to read from logs; each adds a part or an assumption to the risk specification of Section 2.3 (Table 1). Approval gates 1 are the running case: a stricter gate would stop episodes that the log shows running on, and no log shows what such a stop leads to. Partial records 2 keep only the fields a log’s designer chose (Chan et al., 2024), and long horizons 3 add steps at which a changed rule can depart from the log (Kwa et al., 2025). A model release 4 changes the agent itself, shared state 5 links agents through common memory, budgets, or tools, and oversight cues 6 let models tell a test from deployment (Needham et al., 2025). We chose the six from a review of 85 sources (Appendices B.1 and B.2). 2.2 One Agent and One Logged Episode We follow one agent and one logged episode (one recorded run). A sandboxed agent proposes a tool call utu_t at step t; a trusted monitor scores it mtm_t (higher means riskier), and the gate acts on it. The current gate runs every call (pass-all) and is absent from the prompt. Episodes last at most T steps, with loss (task failure, harm, cost); harm is an executed policy violation; cost counts tokens and calls. A stopping gate κθ _θ ends the episode at the first mt>θm_t>θ; a retry gate refuses such calls and lets the agent try again. A stop ends the episode as a failure, keeps harm and cost accrued so far, and adds no later harm; the deployer declares this valuation. Example (a toy episode; made-up scores). A logged episode has four steps with monitor scores 0.100.10, 0.200.20, 0.970.97, and 0.300.30. A gate with θ=0.94θ=0.94 would stop it at step 2, its first deviation from the log. Up to that step, the log shows what the new gate does; three questions remain. (i) What does the stop cost? No log contains a stop, so the deployer declares it. (i) Did the stop prevent the harm? A log keeping only whether harm occurred cannot tell: harm at step 1 precedes the stop, while harm at step 3 would be prevented. (i) What if the gate let the agent retry? The agent would act after a refusal that no log contains, so logs alone can only bound what follows. 2.3 Writing Down the Risk Specification ℜ=(E,ℓ,K,) R=(E, , [rgb]0.7031,0.1484,0.1172K, [rgb]0,0.4727,0.418C) E,ℓE, ⟨si,pi,xi⟩i=1N\ s_i,p_i,x_i \_i=1^N (Kaplan and Garrick, 1981) K partial observation (Bäuerle and Rieder, 2017) C interventions (Pearl, 1995) The colored K and C extend scenario triplets with partial observation and intervention (Appendices A.1 and A.7; Table B.1); badges mark where each characteristic enters. Execution E (what runs) names kernels, random maps from declared inputs to outputs, over at most T steps 3: the agent, monitor, gate 1, sandbox, shared state 5, and oversight cues 6. Serving configuration is a declared input, since batching and the server process can change outputs (Section 4.4). Consequences ℓ (what counts as loss) map a complete episode to loss L, here (failure, harm, cost), keeping pre-stop harm 1. Records K (what the log keeps) specify what the evaluator logs from each step’s available history 2, possibly differing from the agent’s context. Write P0P^0 for the current system’s law on the finite path space. Admissible changes C (what may change) specify which kernels may be replaced, when, using what information, and by whom, such as model releases 4 and agent connections 5. 2.4 A Change’s Risk and Identified Set With the deployment written down, we can ask what the logs justify about one change. Let Rt=rR_t=r be the evaluator’s record up to step t when κ∈κ takes effect, and X=ϕ(L)X=φ(L) the queried loss coordinate. Models that produce the same logs can disagree about the changed system, as each gap in the toy episode shows (Appendix A.3), so the deployer declares a family ℳ0M_0 of structural models; their kernels and records can vary, except where the specification fixes those kernels or their inputs. The deployer then asks which risks remain possible under the models that reproduce the observed record law of every evidence source, PMR=PobsRP^R_M=P^R_obs (Manski, 2003). The risk of the change, and the values the records leave for it, are qtκ(r) q^κ_t(r) =ρ(ℒPκ(X∣Rt=r)), =ρ (L_P^κ(X R_t=r) ), (1) Θtκ(r) ^κ_t(r) =qκt,M(r):M∈ℳ0,PRM=PRobs. = \q^κ_t,M(r):\ M _0,\ P^R_M=P^R_obs \. Here PκP^κ is the specified law of the changed system, and qt,Mκq^κ_t,M the risk under M (Appendix A.2, which also covers records of positive probability and endpoint confidence bounds). The functional ρ summarizes X’s law as harm probability, mean cost, or conditional value-at-risk (CVaR) of tokens (Rockafellar and Uryasev, 2002). The identified set Θtκ(r) ^κ_t(r) is what the records justify before the change runs, and so what a deployer or auditor can claim. The risk is identified when the set has one value; otherwise we bound it sharply or from outside. Logs describe the current system, so they speak about the changed one only under two assumptions that need justification beyond the records (exact: Appendix A.2). Without (A1, invariance), an undeclared change to a tool, the serving stack, or a model behind a fixed name makes logged steps unrepresentative. Without (A2, no anticipation), an agent told about the gate may act differently before the gate acts. If either fails, the deployer must model the extra change. (A1) Invariance, informal. Nothing the change leaves in place changes: the initial law and every kernel the change does not replace, random inputs included, stay as logged. Installing the gate thus leaves the model, tools, users, and sampler as logged. This covers unobserved environment state, whose initial law and transitions are part of E. (A2) No anticipation, informal. Both systems run in the same causal order and coincide before the change. Every kernel left in place keeps its declared inputs. A replaced kernel may read other earlier inputs that the change declares, and for replay both rules read one common input that holds what either uses. Nothing left in place, and no declared input, reads which change was installed or its announcement, so announcing the gate in the agent’s prompt violates (A2). 3 Evidence Design for Agent Changes A deployer who proposes a change needs a statement of its risk or the evidence that would settle it. Five steps give one or the other (in symbols: Algorithm 1, Appendix A.6): 1. Declare the change, its stop value, and the decision rule; justify (A1) and (A2), or model the extra change. 2. Replay both rules on recorded inputs, where the records permit, up to the first deviation (toy episode: step 2). 3. Read agreement and stop contributions when the log is sufficient; the stop value keeps harm and cost accrued before the stop (§3.1 to §3.3; toy questions (i) and (i)). 4. Resolve the rest by matching logged cases, snapshot runs, or bounds (§3.4; question (i)); other settings need a transfer link (§3.5, §3.6). 5. Decide by jointly valid one-sided bounds, with an allowance for restoration error, against a declared harm ceiling and success floor, or name the evidence needed to settle it (§4.1). To make steps 2 and 3 precise, fix κ,rκ,r from (1) (Appendix A.4). Baseline paths Ω0 ^0 follow the logged rule. The first deviation σκ _κ is the first step where the new rule differs on logged input; κ=σκ>T A_κ=\ _κ>T\ means no deviation. The replayed prefix hκ+h^+_κ comprises the full history before that decision, including unrecorded coordinates, followed by the new output. It is terminal if the output stops the episode and continuing otherwise. (R) Replay interface, informal. Both rules are known and deterministic given each step’s declared input ItI_t, possibly including a seed. The full record contains that input, so both rules can be rerun on logged proposals, scores, and seeds. (A3) Declared stop value, informal. After a stop, the loss follows a law bκ(⋅∣hκ+)b_κ(· h^+_κ) that the deployer declares, including losses accrued before the stop. It describes what happens after the stop, so the loss map is unchanged. Changes that stop with the same replayed prefix share it, and it must agree with any post-stop behavior baseline operation can show. The three events are agree (κ A_κ), stop (σκ≤T,terminal\ _κ≤ T,\ terminal\), and continue (σκ≤T,continuing\ _κ≤ T,\ continuing\), the three columns of Figure 1, whose bottom row is display (2) with matching labels; only the last needs evidence beyond the log and the stop value. Here E0[⋅∣r]E^0[\,· r] averages under P0(τ∣r)P^0(τ r), with hκ+=hκ+(τ)h^+_κ=h^+_κ(τ). Under (R) and (A1) to (A3), for every B⊆B , Pκ(L∈B∣r)=P0(L∈B,agree∣r)⏟agree: read from the log+E0[bκ(B∣hκ+) 1stop|r]⏟stop: declared stop value+Pκ(L∈B,continue∣r)⏟continue: support, rerun, or bounds. aligned &P^κ(L∈ B r)\\ & = P^0(L∈ B,\ agree r)_ mintagree: read from the log\\ & =+ E^0 [b_κ(B h^+_κ)\,1\stop\ |r ]_ black!60whitestop: declared stop value\\ & =+ P^κ(L∈ B,\ continue r)_continue: support, rerun, or bounds. aligned (2) The first two terms restrict the deterministic-regime g-formula (Robins, 1986) to paths that follow the new rule, as censoring at deviation does (Cain et al., 2010). The third is identified under the support and recording conditions of Section 3.4; otherwise, worst-case bounds (Manski, 2003) give each continuing episode its least and greatest feasible outcome, attained when unseen continuations can be chosen freely and jointly (condition (S), Proposition E.1.1; coarser records: Algorithm 1). 3.1 Approval Gates: Can Logs Replay a Stop? Deviation replay (Robins, 1986; Cain et al., 2010), informal; exact: Proposition A.4.1. Assume (R), (A1), and (A2), and condition on the record r. The agreement term of (2) then holds: the changed system has the logged loss law on episodes that agree at every step. With (A3), the stop term holds even if the baseline never stops. For the deployer. Log the most permissive safe gate, declare the stop value (tolerated post-stop harm: Appendix D.3), and replay stricter gates; a looser gate evaluated from a stricter log is a continuing change that needs support or bounds. 3.2 Partial Records: What Must Logs Keep? Section 3.1 uses records sufficient for agreement and stops; with partial records 2, Figure 2 shows why missing harm timing leaves stop risk unresolved even with more episodes. Figure 2: Missing harm timing leaves stop risk unresolved. Identical records hide whether executed harm (coral) came before (A) or after (B) the θ=0.94θ=0.94 stop at step 2; the gate keeps A’s harm and removes B’s. For every baseline law, a log determines the sum of the first two terms of (2) exactly when it preserves each episode’s combined contribution. Within the conditioning event, a log may merge two episodes only if they contribute equally, which those of Figure 2 do not. Contributions are logged loss on agreement, declared loss law on stops, and zero on continuation. In Proposition 3.1, uκ(τ)u_κ(τ) indicates a continuing deviation; its conditional expectation is unresolved mass. Here g#Pg_\#P is the log’s law under P, and g−1(y)g^-1(y) the paths producing log value y (scope of necessity: Appendix E.5). Proposition 3.1 (Logging sufficiency). Assume (R), (A1), and (A2), with (R) referring to the full record; the logging map g below need not record ItI_t. Let Cκ(τ)C_κ(τ) be δℓ(τ) _ (τ) on agreement, bκ(⋅∣hκ+(τ))b_κ(· h^+_κ(τ)) at a terminal deviation, and 00 at a continuing one, and let uκ=1−Cκ()u_κ=1-C_κ(L). Let rP_r be the laws on Ω0 ^0 with P(Rt=r)>0P(R_t=r)>0, and let sκ,r(P)=(∫CκdP(⋅∣r),∫uκdP(⋅∣r))s_κ,r(P)=( C_κ\,dP(· r), u_κ\,dP(· r)). For a logging map g that determines the event Rt=r\R_t=r\, there is a map Ψ with sκ,r(P)=Ψ(g#P)s_κ,r(P)= (g_\#P) for every P∈rP _r if and only if (Cκ,uκ)(C_κ,u_κ) is constant on every set g−1(y)∩Ω0∩Rt=rg^-1(y)∩ ^0∩\R_t=r\. For the deployer: what to log. Keep fields that reconstruct each episode’s contribution, including harm timing relative to deviation (Table D.3). Otherwise, distinct baseline distributions with identical records can yield different combined replay contributions, which neither more episodes nor coarser logs resolve (Corollary E.6.1; Blackwell, 1951; Blackwell, 1953). Log the serving mode: batch-dependent serving fails (R) when a change reruns the agent. 3.3 Long Horizons: Does Length Matter? Each extra step is another chance to leave the log, so the share agreeing throughout cannot rise with the horizon (Corollary E.7.1). With sufficient records and (A3, declared stop value), stopping changes stay identified at every horizon; a continuing change’s worst-case mean interval (Proposition E.1.1) can widen as agreement falls (§4.3). 3.4 Continuing Changes: Runs and Snapshots Retry gates 1 and model releases 4 continue past the first deviation into the continuing term of (2), where the agent may read inputs the log never shows. The log suffices when it covers and records every input the changed system reads (supported continuation); otherwise the deployer reruns or bounds, and saves states for the reruns. Supported continuation, informal; exact: Proposition A.5.1. Assume (A1) and (A2), and let the change replace kernels by known ones after the record r was taken. Suppose (G1) baseline support: at each position, each input the change leads an unchanged kernel to read has positive baseline probability there; inputs where the specification fixes that kernel’s output, as after a stop, are exempt. Suppose also that the log records (G2) those kernels’ declared inputs, (G3) every coordinate the loss reads, and (G4) every input the change reads. Then the g-formula identifies the changed system’s loss law, within mechanisms that share the declared kernel inputs and the values the specification fixes, even if no episode agrees. Without (G1), keeping (G2) to (G4) and every response law the specification fixes, allow any response law at each remaining input of zero baseline probability (U, free responses). Choosing these laws separately for each position gives the identified set under the g-formula; a law shared across positions, or an input merely absent from a finite log, gives an outer set. Both parts are classical (Robins, 1986; Manski, 2003); Appendix F.5 unifies them. Because baseline never refuses, a retry gate fails (G1) if an unchanged kernel without a declared value reads the refusal or its message. Under (R), a seed-addressable model release (deterministic at each logged decision input, random tape on fixed serving) has identified agreement mass, at most the first-decision agreement (Corollary F.6.1). When and how much to rerun. Where the log has no matching cases, as after a refusal or a new model’s new text, the deployer can bound the outcome or use targeted execution: restore the sandbox at a logged prefix and run only the continuation. Assumption (T), restoration fidelity, links these runs to ℳ0M_0: restored state, agent context, and remaining budgets give the continuation its live law after that prefix. A restored law within γ in total variation of the live one at each continuing prefix shifts P(harm) by at most γ times the continuing mass (Lemma F.7.2). A uniform random sample of unresolved continuations can replace executing all of them (Proposition F.7.1). Live testing spreads the gap between true harm and the target over all episodes; execution concentrates it on the open ones, and restoration error eats into it. Execution budget: limits and achievability, informal; exact: Propositions F.8.1 and F.8.2, Corollary F.8.3. Assume (S), binary harm, independent episodes, and one harm probability p for every unresolved continuation (Appendix F.9 allows strata). Treat the log’s resolved harmful mass q0q_0 and unresolved mass m as known. The change’s P(harm) q=q0+mpq=q_0+mp falls short of a target q⋆<q0+mq <q_0+m by ζ=q⋆−q>0ζ=q -q>0. Restored runs err by at most γ in total variation, and klkl is Bernoulli relative entropy. (i) If mγ≥ζmγ≥ζ, restoration error can hide the whole gap: no procedure that executes logged continuations has power above its size, that is, none certifies a safe change at exact restoration more often than it can certify an unsafe one. (i) Otherwise, let p¯=p+ζ/m−γ p=p+ζ/m-γ. A procedure valid at level α that certifies with probability at least 1−β1-β at exact restoration executes at least kl(1−β,α)/kl(p,p¯)kl(1-β,α)/kl(p, p) continuations in expectation (Kaufmann et al., 2016). Live testing that does not trust the log needs at least kl(1−β,α)/kl(q,q⋆)kl(1-β,α)/kl(q,q ) episodes. As α,β→0α,β→ 0 with a log that grows fast enough, sequential probability ratio tests (Wald, 1945) approach both bounds. Here p¯ p is the open episodes’ harm rate that would just reach the target, less the restoration error; the closer p is to p¯ p, the more runs a decision needs. Appendix F.9 extends both bounds to strata with their own harm rates, errors, and costs. Strata where restoration error can make harm certain get no runs, and the others’ run shares are part of the test’s validity (Propositions F.9.1 and F.9.2; Remark F.9.3; allocation: Neyman, 1934). What to store: snapshot design for threshold gates, informal; exact: Proposition F.10.1. A gate that blocks above a threshold in [θmin,1)[ _ ,1) first blocks only at a running maximum: a step whose score exceeds θmin _ and every earlier score since the change took effect. A running maximum is open if some such gate that first blocks there leaves the query’s outcome unsettled. Under full-history kernels, (T), and free responses at unsupported inputs (U), the open running maxima before the last step form the least set among first-block snapshots whose continuation laws identify the query for every gate in the family. An earlier snapshot can replace one by re-executing the agreeing steps. For the deployer. Record (G2) to (G4), rerun open continuations from snapshots meeting (T), and for threshold gates save first-block snapshots at open running maxima, the least such set. 3.5 Shared State: Does Evidence Transfer? Sections 3.1 to 3.4 evaluate a change from the deployer’s own logs; evidence from components tested alone needs a transfer link (Pearl and Bareinboim, 2011). When agents share state S (memory, budget, tools) 5, component logs identify each failure probability given S, leaving dependence open; the Fréchet range contains every compatible joint failure probability, and each value in it is attainable when dependence given S is unrestricted (Fréchet, 1951; Nelsen, 2006; Mosleh et al., 1998). Suppose the state law is known, component loss laws given S match alone and composed, and components read only S and private randomness. With unrestricted responses on unseen states, standalone evidence identifies a nontrivial loss event up to width PS(Ui)P_S(U_i), where UiU_i comprises composed states never seen alone (Proposition G.1.1). 3.6 Oversight Cues: Do Tests Transfer? Oversight cues raise the same transfer question with a different state variable: an agent that can tell a test from deployment may act differently in each. Recorded cues 6, including evaluation signs (Needham et al., 2025) and gate notices, play the role of S in Section 3.5 when the agent reads only the cue and private randomness. Test evidence determines risk only for deployment cues occurring in testing (Remark G.4.3). A cue created by the change, such as an announced gate, violates (A2, no anticipation); Section 4.6 tests one. 4 Applying the Framework in a Sandbox We test each characteristic in ControlArena’s bash setting (Inglis et al., 2025; Bhatt et al., 2025), where harm is an executed violation of a declared sandbox policy, and repeat gates and logging in τ2τ^2-bench’s airline environment (Barres et al., 2025), where harm is an executed booking write that breaks the airline’s written policy. The 16 runs of Table D.1 log about 49,000 episodes, using vLLM mostly on NVIDIA H100 80GB hosts (Appendix D.2). Every log is from a pass-all gate; eight of the nine registered runs fixed sample, analysis, and margin before launch, and three froze predictions before new live records were read. The agent never sees an unannounced gate and a stop ends the episode, so (A2) holds by construction for stopping gates. (A1) holds where serving and environment are stable; where outputs vary by run (the stronger agent, the airline setting), replay is compared with live gates in distribution, within a registered margin. Change Log alone New runs Live Result What the framework establishes 1 Stopping gate, 3 settings 0.039 (bash; see App. D.3) 0.030 ✓Match within 0.03 in all 3 1 Retry gate 1 ? [0.244,0.345][0.244,0.345] 0.279 0.288 ✓Match within 0.015 1 Retry gate 2 ? [0.100,0.451][0.100,0.451] 0.158 0.165 ✓Match within 0.015 1 Gates 1 / 2: approved at 0.25 ? Undecided No / yes No / yes ✓Same decision as live 1 Retry gate, bash ? [0.023,0.422][0.023,0.422] 0.029 0.030 ✓Match within 0.02 2 Stopping gate, per-step harm ≤ 0.064 with, ≤ 0.159 without Not needed ∙ Log must keep harm timing 5 Relay: snapshot start 0.118 to 0.119 0.115 ✓Match within 0.03 Simpler readings and broken assumptions 1 Gates 1 / 2: retry as stop Registered: 0.2445 / 0.1002 0.288 / 0.165 ✗Low by 0.043 / 0.065 1 Gates 1 / 2: gate ignored Registered: 0.3445 for both 0.288 / 0.165 ✗High by 0.057 / 0.179 1 Gates 1 / 2: blocks skipped Post hoc: 0.3108 / 0.1904 0.288 / 0.165 ✗High by 0.023 / 0.025 5 Relay: clean start 0.178 0.115 ✗High by 0.063 6 Announced gate, abort rate Unannounced-log replay 181 of 400 ✗Replay low; CI excludes 0 Table 2: The log alone leaves retry gates open (?); rerunning only what it leaves open matches live runs (✓); simpler readings misestimate harm, and clean starts and an announced gate miss live runs (✗). ∙ : a logging requirement. P(harm) unless labeled. Match: Newcombe 90% interval inside the registered margin. Certified limits are exact one-sided 95%; log intervals are plug-in bounds. In x / y cells, x is gate 1; blank: not used. 4.1 Approval Gates: Stopping and Retry Retry Gates: Estimating Harm. A retry gate lets the agent act after a refusal, which no pass-all log contains. The log alone bounds retry-gate harm; targeted execution pins it down if restored runs behave like live runs (restoration fidelity) (Figure D.2). One pass-all log of 7,200 stronger-agent episodes serves two retry gates (thresholds on a log-scale monitor score), which first block in 14% and 41% of episodes; before every high-scoring step, a snapshot rule that names no gate saved the sandbox. Following the five steps of Section 3, executing only the continuations from these snapshots identifies harm for both gates (worked example: Appendix D.3). Each P(harm), frozen before live records were read, matched paired live gates within 0.015; the simpler readings misestimated it (Table 2; Figure D.1). Retry Gates: Deciding. A rule declared in advance approves a gate whose exact one-sided 95% bounds put harm at most 0.25 and task success at least 0.37. The log alone cannot decide either gate; with the continuations rerun, the rule approves gate 2 and declines gate 1, as on the live runs. Read at face value (post hoc), counting retries as stops would approve gate 1, which live runs refuse; skipping blocked calls reaches both live decisions but misses live harm (Table 2). Given the log, the continuations cost 15% of the agent calls of testing both gates live and half those of a live test sized to reach both decisions in 90% of 500 random subsets (post hoc; Appendix D.3). Targeted execution also matched live runs for a bash agent and the airline environment; in all four, live harm ran 0.001 to 0.008 higher (Appendix D.3). 4.2 Partial Records: What the Log Must Keep In our logs, one field, per-step harm, decided how low a harm ceiling we could certify. On 300 held-out bash episodes, a reduced log of scores, per-step harm and cost, and outcome certifies the same stopping-gate harm ceiling as the full record (per field, an instance, not a general list: Table D.3). Without per-step harm, they certify 0.159 instead of 0.064, since the log cannot tell whether harm came before the stop (Figure 2); a replication log (0.111 instead of 0.051) and the stronger agent agree, illustrating both directions of Proposition 3.1. 4.3 Long Horizons: Replay Across 40 Steps Replay still pins down stopping-gate harm as episodes get longer; fewer logged episodes agree with a retry gate, leaving more of its harm to bounds or targeted execution. On a 600-episode bash log with a 40-step cap, replayed stopping-gate P(harm) stays at 0.043 to 0.067 (unknown outcomes) from 15 steps on; the retry gate’s agreement mass falls from 0.77 to 0.57 and its plug-in bounds reach [0.043,0.473][0.043,0.473] at 40 steps (Appendix D.5). 4.4 Model Releases: Old Logs, New Model The new model reproduced none of 99 logged episodes, so replay settled none. At logged inputs and seeds, the same model reproduced every episode, so the release needs support, bounds, or new runs from step 0 (Appendix D.6). 4.5 Shared State: Two Agents in Relay A first agent takes up to 7 steps; a fresh-context second agent continues from its workspace for up to 8 (Appendix D.7). Testing the second agent from a clean start overstates its harm in the relay; testing it from the handoff snapshot matches the relay (Table 2). A clean start leaves out the first agent’s changes to the workspace, which the second agent reads. Both agents violated the policy in four times as many relays as the product of their rates; per-agent logs that record the task’s risk class narrow this joint probability to [0.031,0.115][0.031,0.115] (Proposition G.1.1(i)). 4.6 Oversight Cues: Announcing the Gate Announcing the gate in our prompt raised the abort rate above what replay from unannounced logs predicted (same tasks and seeds; Table 2). The unannounced gate, a negative control, stays compatible with replay (Appendix D.8). 5 Related Work Evaluation from Logs. Off-policy evaluation, optimal stopping, and dynamic treatment regimes hold the closest precursors of our stopping replay and supply its core. Full trajectories evaluate any stopping rule with a known reward (Goel et al., 2017), and regime comparisons censor at deviation (Cain et al., 2010). The cited replay and weighting methods use randomized logging (Li et al., 2011; Bottou et al., 2013), which our logs lack. Execution from saved states appears in driving simulation (Gulino et al., 2023), rare-event splitting (Glasserman et al., 1999), agent resampling (Bhatt et al., 2025), and reset access (Yin et al., 2022; Song et al., 2023). Agent checkpoint and replay systems (Wu et al., 2026; Chawla and Koul, 2026) restore recorded prefixes without identification guarantees. What Is New. Without overlap, partial identification gives sets (Manski, 2003; Khan et al., 2024), and sharp bounds exist for dynamic regimes (Alvarez and Ferrando, 2026) and discrete causal models (Duarte et al., 2023); our unsupported-input result specializes them to replacement kernels with declared values. Robust sequential tests (Saha and Ramdas, 2026) and cost-aware pure exploration (Kanarios et al., 2024) supply the tools behind our execution bounds. New here are the logging condition for replayed stop values (Proposition 3.1), the restoration threshold and execution-to-live cost ratio (Appendix F.8), allocation across strata (Appendix F.9), and the least set of first-deviation snapshots per threshold family (Proposition F.10.1). Agent Risk and Governance. Ray (2026) bounds a multi-judge gate’s errors and shows that ungated trajectories need not identify a blocking regime’s safety frontier. Our joint-risk range conditions on shared state (Section 3.5; certificates from joint runs: Bhardwaj et al., 2026). Taxonomies list our characteristics (Chan et al., 2023; Slattery et al., 2024, e.g.,), rigorous audits need more than black-box access (Casper et al., 2024), and underwriting proposals model claim costs (Xu et al., 2026); evidence design specifies needed records (Appendices B.4 and C). 6 Conclusion and Future Directions agent-risk establishes when logs can support approving changes to deployed agents and when more evidence is needed. If nothing else changes and the agent does not anticipate the change, it shows what a log settles and must record and, for independent episodes, the reruns a decision needs. In our bash sandbox, the log alone decided neither retry gate; rerunning only what it left open reached both live decisions at half the agent calls of a live test sized post hoc for them, given the log. Future work could restore state beyond saved files and bound the risk of oversight-aware agents (Needham et al., 2025). Limitations Each result rests on stated conditions; Table D.2 lists the evidence each demonstration still needs. Identification results concern population record laws on finite path spaces. Execution results add sampling guarantees for independent episodes; agents sharing state use the component evidence of Section 3.5. Replay assumes that nothing else changes (A1) and that the agent does not anticipate the change (A2). A change the agent can perceive, such as an announced gate, violates (A2). Paired runs with and without the announcement expose this violation (Section 4.6); bounds for agents that recognize oversight remain open. Logs cannot confirm the stop value (A3), which our runs declare but do not test for harm. Restoration checks covered only the file tree compared by the harness. A frozen mechanical checker defines our harm label under four declared rules (Appendix D.2); the framework takes any declared loss. The demonstrations use honest agents (not evading oversight) from one open-weight model family, with 14B and 27B parameters, in a bash sandbox and an airline booking environment. The relay joins two copies of one agent, and supported continuation is untested. For the model release, replay settled none of 99 episodes, leaving its losses unestimated. Ethical Considerations Risk estimates can affect deployment, resource access, and responsibility for failures. Claims should identify affected parties, the loss definition, evidence, and uncertainty. Unobserved consequences and misspecified mechanisms can give false reassurance. The framework exposes assumptions to deployers and auditors, preserving unresolved uncertainty in downstream decisions. A deployer could choose a loss, stop value, or margin that favors approval. Declaring the specification and decision rule before reading results, as our registered runs do, guards against this choice. Episodes the log leaves open enter the decision as intervals. In deployment, replay’s per-step records and saved states can contain user data, subject to the deployer’s retention and access rules. Proposition 3.1 states when logs trimmed for privacy still determine the agreeing and stopped terms, allowing checks before use. Our logs from sandboxed coding tasks and simulated airline customers contain no personal data. Appendix I provides our AI Use Statement. References AI Safety Institute (2024) AI Safety Institute. 2024. AI Safety Institute Approach to Evaluations. Policy paper. Alvarez and Ferrando (2026) Alexander Alvarez and Sebastian E. Ferrando. 2026. Sharp causal bounds for dynamic treatment regimes. arXiv preprint arXiv:2609.06397. Anthropic (2024) Anthropic. 2024. Model Card Addendum: Claude 3.5 Haiku and Upgraded Claude 3.5 Sonnet. Technical report, Anthropic. Bareinboim and Pearl (2016) Elias Bareinboim and Judea Pearl. 2016. Causal inference and the data-fusion problem. Proceedings of the National Academy of Sciences, 113(27):7345–7352. Barres et al. (2025) Victor Barres, Honghua Dong, Soham Ray, Xujie Si, and Karthik Narasimhan. 2025. τ2τ^2-Bench: Evaluating conversational agents in a dual-control environment. arXiv preprint arXiv:2506.07982. Bäuerle and Rieder (2017) Nicole Bäuerle and Ulrich Rieder. 2017. Partially observable risk-sensitive Markov decision processes. Mathematics of Operations Research, 42(4):1180–1196. Bengio et al. (2026) Yoshua Bengio, Stephen Clare, Carina Prunkl, Malcolm Murray, Maksym Andriushchenko, Ben Bucknall, Rishi Bommasani, Stephen Casper, Tom Davidson, Raymond Douglas, David Duvenaud, Philip Fox, Usman Gohar, Rose Hadshar, Anson Ho, Tiancheng Hu, Cameron Jones, Sayash Kapoor, Atoosa Kasirzadeh, and 74 others. 2026. International AI Safety Report 2026. Report DSIT 2026/001, Department for Science, Innovation and Technology. Bengio et al. (2025) Yoshua Bengio, Sören Mindermann, Daniel Privitera, Tamay Besiroglu, Rishi Bommasani, Stephen Casper, Yejin Choi, Philip Fox, Ben Garfinkel, Danielle Goldfarb, Hoda Heidari, Anson Ho, Sayash Kapoor, Leila Khalatbari, Shayne Longpre, Sam Manning, Vasilios Mavroudis, Mantas Mazeika, Julian Michael, and 77 others. 2025. International AI Safety Report. Preprint, arXiv:2501.17805. Bhardwaj et al. (2026) Varun Pratap Bhardwaj, Garima Singh, and Arun Pratap Bhardwaj. 2026. Agent behavioral contracts I: Certifying compositional reliability without assuming independence. Preprint, arXiv:2608.12895. Bhatt et al. (2025) Aryan Bhatt, Cody Rushing, Adam Kaufman, Tyler Tracy, Vasil Georgiev, David Matolcsi, Akbir Khan, and Buck Shlegeris. 2025. Ctrl-Z: Controlling AI agents via resampling. arXiv preprint arXiv:2504.10374. Blackwell (1951) David Blackwell. 1951. Comparison of experiments. In Proceedings of the Second Berkeley Symposium on Mathematical Statistics and Probability, pages 93–102. University of California Press. Blackwell (1953) David Blackwell. 1953. Equivalent comparisons of experiments. The Annals of Mathematical Statistics, 24(2):265–272. Bottou et al. (2013) Léon Bottou, Jonas Peters, Joaquin Quiñonero-Candela, Denis X. Charles, D. Max Chickering, Elon Portugaly, Dipankar Ray, Patrice Simard, and Ed Snelson. 2013. Counterfactual reasoning and learning systems: The example of computational advertising. Journal of Machine Learning Research, 14(101):3207–3260. Cain et al. (2010) Lauren E. Cain, James M. Robins, Emilie Lanoy, Roger Logan, Dominique Costagliola, and Miguel A. Hernán. 2010. When to start treatment? A systematic approach to the comparison of dynamic regimes using observational data. The International Journal of Biostatistics, 6(2). Article 18. California State Legislature (2025) California State Legislature. 2025. SB-53 Artificial intelligence models: large developers. California Senate Bill 53 (Transparency in Frontier Artificial Intelligence Act), Chapter 138, Statutes of 2025; approved September 29, 2025. Casper et al. (2024) Stephen Casper, Carson Ezell, Charlotte Siegmann, Noam Kolt, Taylor Lynn Curtis, Benjamin Bucknall, Andreas Haupt, Kevin Wei, Jérémy Scheurer, Marius Hobbhahn, Lee Sharkey, Satyapriya Krishna, Marvin Von Hagen, Silas Alberti, Alan Chan, Qinyi Sun, Michael Gerovitch, David Bau, Max Tegmark, and 2 others. 2024. Black-box access is insufficient for rigorous AI audits. In Proceedings of the 2024 ACM Conference on Fairness, Accountability, and Transparency, pages 2254–2272. Center for AI Standards and Innovation , NIST(2025) (CAISI) Center for AI Standards and Innovation (CAISI), NIST. 2025. Technical Blog: Strengthening AI Agent Hijacking Evaluations. Technical blog. Last modified 2025-12-19. Chan et al. (2024) Alan Chan, Carson Ezell, Max Kaufmann, Kevin Wei, Lewis Hammond, Herbie Bradley, Emma Bluemke, Nitarshan Rajkumar, David Krueger, Noam Kolt, Lennart Heim, and Markus Anderljung. 2024. Visibility into AI agents. In Proceedings of the 2024 ACM Conference on Fairness, Accountability, and Transparency, pages 958–973. ACM. Chan et al. (2023) Alan Chan, Rebecca Salganik, Alva Markelius, Chris Pang, Nitarshan Rajkumar, Dmitrii Krasheninnikov, Lauro Langosco, Zhonghao He, Yawen Duan, Micah Carroll, Michelle Lin, Alex Mayhew, Katherine Collins, Maryam Molamohammadi, John Burden, Wanru Zhao, Shalaleh Rismani, Konstantinos Voudouris, Umang Bhatt, and 3 others. 2023. Harms from Increasingly Agentic Algorithmic Systems. In Proceedings of the 2023 ACM Conference on Fairness, Accountability, and Transparency (FAccT ’23), pages 651–666. ACM. Chatzi et al. (2025) Ivi Chatzi, Nina L. Corvelo Benz, Eleni Straitouri, Stratis Tsirtsis, and Manuel Gomez-Rodriguez. 2025. Counterfactual token generation in large language models. In Proceedings of the Fourth Conference on Causal Learning and Reasoning, volume 275 of Proceedings of Machine Learning Research, pages 1291–1315. PMLR. Chawla and Koul (2026) Tisha Chawla and Susheem Koul. 2026. Chronicle: Cut-point replay for regression testing of LLM agents. Preprint, arXiv:2609.20625. Chen (2026) Hao-Hsuan Chen. 2026. Foundations of a time-consistent counterfactual actuarial runtime for autonomous AI agents. Preprint, arXiv:2605.26508. Clopper and Pearson (1934) C. J. Clopper and E. S. Pearson. 1934. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika, 26(4):404–413. Corvelo Benz et al. (2026) Nina L. Corvelo Benz, Stratis Tsirtsis, Eleni Straitouri, Ivi Chatzi, Ander Artola Velasco, Suhas Thejaswi, and Manuel Gomez-Rodriguez. 2026. Evaluation of large language models via coupled token generation. In Proceedings of the 29th International Conference on Artificial Intelligence and Statistics, volume 300 of Proceedings of Machine Learning Research, pages 2215–2223. PMLR. Cursor (2026) Cursor. 2026. Cursor earns AIUC-1 certification for agent security and reliability. Cursor blog, August 13, 2026. Accessed October 4, 2026. Deng et al. (2025) Zehang Deng, Yongjian Guo, Changzhou Han, Wanlun Ma, Junwu Xiong, Sheng Wen, and Yang Xiang. 2025. AI Agents Under Threat: A Survey of Key Security Challenges and Future Pathways. ACM Computing Surveys, 57(7). Duarte et al. (2023) Guilherme Duarte, Noam Finkelstein, Dean Knox, Jonathan Mummolo, and Ilya Shpitser. 2023. An automated approach to causal inference in discrete settings. Journal of the American Statistical Association, pages 1–16. ElevenLabs (2026) ElevenLabs. 2026. ElevenLabs secures first-of-its-kind AI agent insurance. ElevenLabs blog, February 12, 2026. Accessed October 4, 2026. European Commission, AI Office (2025) European Commission, AI Office. 2025. General-Purpose AI Code of Practice: Safety and Security Chapter. Final version, 10 July 2025. European Parliament and Council of the European Union (2024) European Parliament and Council of the European Union. 2024. Regulation (EU) 2024/1689 of the European Parliament and of the Council of 13 June 2024 laying down harmonised rules on artificial intelligence and amending Regulations (EC) No 300/2008, (EU) No 167/2013, (EU) No 168/2013, (EU) 2018/858, (EU) 2018/1139 and (EU) 2019/2144 and Directives 2014/90/EU, (EU) 2016/797 and (EU) 2020/1828 (Artificial Intelligence Act). Official Journal of the European Union, L series, 12 July 2024; application dates amended by Regulation (EU) 2026/1744. Fréchet (1951) Maurice Fréchet. 1951. Sur les tableaux de corrélation dont les marges sont données. Annales de l’Université de Lyon, Section A, Série 3, 14:53–77. Garivier and Kaufmann (2016) Aurélien Garivier and Emilie Kaufmann. 2016. Optimal best arm identification with fixed confidence. In Proceedings of the 29th Annual Conference on Learning Theory, volume 49 of Proceedings of Machine Learning Research, pages 998–1027. Glasserman et al. (1999) Paul Glasserman, Philip Heidelberger, Perwez Shahabuddin, and Tim Zajic. 1999. Multilevel splitting for estimating rare event probabilities. Operations Research, 47(4):585–600. Goel et al. (2017) Karan Goel, Christoph Dann, and Emma Brunskill. 2017. Sample efficient policy search for optimal stopping domains. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, pages 1711–1717. Greenblatt et al. (2024) Ryan Greenblatt, Buck Shlegeris, Kshitij Sachan, and Fabien Roger. 2024. AI control: Improving safety despite intentional subversion. In Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 16295–16336. PMLR. Gulino et al. (2023) Cole Gulino, Justin Fu, Wenjie Luo, George Tucker, Eli Bronstein, Yiren Lu, Jean Harb, Xinlei Pan, Yan Wang, Xiangyu Chen, John Co-Reyes, Rishabh Agarwal, Rebecca Roelofs, Yao Lu, Nico Montali, Paul Mougin, Zoey Yang, Brandyn White, Aleksandra Faust, and 3 others. 2023. Waymax: An accelerated, data-driven simulator for large-scale autonomous driving research. In Advances in Neural Information Processing Systems, volume 36, pages 7730–7742. Hammond et al. (2025) Lewis Hammond, Alan Chan, Jesse Clifton, Jason Hoelscher-Obermaier, Akbir Khan, Euan McLean, Chandler Smith, Wolfram Barfuss, Jakob Foerster, Tomáš Gavenčiak, The Anh Han, Edward Hughes, Vojtěch Kovařík, Jan Kulveit, Joel Z. Leibo, Caspar Oesterheld, Christian Schroeder de Witt, Nisarg Shah, Michael Wellman, and 25 others. 2025. Multi-Agent Risks from Advanced AI. Technical Report 1, Cooperative AI Foundation. Hanna et al. (2017) Josiah P. Hanna, Philip S. Thomas, Peter Stone, and Scott Niekum. 2017. Data-efficient policy evaluation through behavior policy search. In Proceedings of the 34th International Conference on Machine Learning, volume 70 of Proceedings of Machine Learning Research, pages 1394–1403. PMLR. Hao et al. (2024) Meiling Hao, Pingfan Su, Liyuan Hu, Zoltan Szabo, Qingyuan Zhao, and Chengchun Shi. 2024. Off-policy evaluation with deeply-abstracted states. arXiv preprint. He et al. (2024) Yifeng He, Ethan Wang, Yuyang Rong, Zifei Cheng, and Hao Chen. 2024. Security of AI Agents. Preprint, arXiv:2406.08689. Horvitz and Thompson (1952) D. G. Horvitz and D. J. Thompson. 1952. A generalization of sampling without replacement from a finite universe. Journal of the American Statistical Association, 47(260):663–685. Hua et al. (2024) Wenyue Hua, Xianjun Yang, Mingyu Jin, Zelong Li, Wei Cheng, Ruixiang Tang, and Yongfeng Zhang. 2024. TrustAgent: Towards safe and trustworthy LLM-based agents. In Findings of the Association for Computational Linguistics: EMNLP 2024, pages 10000–10016, Miami, Florida, USA. Association for Computational Linguistics. Imbens and Manski (2004) Guido W. Imbens and Charles F. Manski. 2004. Confidence intervals for partially identified parameters. Econometrica, 72(6):1845–1857. Infocomm Media Development Authority (2026) Infocomm Media Development Authority. 2026. Model AI Governance Framework for Agentic AI. Framework Version 1.5, Infocomm Media Development Authority, Singapore. Published 20 May 2026, updated 5 June 2026. Inglis et al. (2025) Rogan Inglis, Ollie Matthews, Tyler Tracy, Oliver Makins, Tom Catling, Asa Cooper Stickland, Rasmus Faber-Espensen, Daniel O’Connell, Myles Heller, Miguel Brandao, Adam Hanson, Arathi Mani, Tomek Korbak, Jan Michelfeit, Dishank Bansal, Tomas Bark, Chris Canal, Charlie Griffin, Mojmir Stehlik, and 2 others. 2025. ControlArena. GitHub repository. UK AI Security Institute and Redwood Research. Bash setting: https://control-arena.aisi.org.uk/settings/bash.html. Accessed 2026-10-04. Juneja and Krishnasamy (2019) Sandeep Juneja and Subhashini Krishnasamy. 2019. Sample complexity of partition identification using multi-armed bandits. In Proceedings of the Thirty-Second Conference on Learning Theory, volume 99 of Proceedings of Machine Learning Research, pages 1824–1852. Kanarios et al. (2024) Kellen Kanarios, Qining Zhang, and Lei Ying. 2024. Cost aware best arm identification. Reinforcement Learning Journal. ArXiv:2402.16710. Kaplan and Garrick (1981) Stanley Kaplan and B. John Garrick. 1981. On the quantitative definition of risk. Risk Analysis, 1(1):11–27. Kaufmann et al. (2016) Emilie Kaufmann, Olivier Cappé, and Aurélien Garivier. 2016. On the complexity of best-arm identification in multi-armed bandit models. Journal of Machine Learning Research, 17(1):1–42. Khan et al. (2024) Samir Khan, Martin Saveski, and Johan Ugander. 2024. Off-policy evaluation beyond overlap: Sharp partial identification under smoothness. In Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 23734–23757. PMLR. Kolt (2025) Noam Kolt. 2025. Governing AI Agents. Notre Dame Law Review, 101. Forthcoming. Kwa et al. (2025) Thomas Kwa, Ben West, Joel Becker, Amy Deng, Katharyn Garcia, Max Hasin, Sami Jawhar, Megan Kinniment, Nate Rush, Sydney Von Arx, Ryan Bloom, Thomas Broadley, Haoxing Du, Brian Goodrich, Nikola Jurkovic, Luke Harold Miles, Seraphina Nix, Tao Lin, Chris Painter, and 7 others. 2025. Measuring AI ability to complete long software tasks. arXiv preprint arXiv:2503.14499. Kwon et al. (2023) Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with PagedAttention. In Proceedings of the 29th Symposium on Operating Systems Principles, pages 611–626. Lan and DeMets (1983) K. K. Gordon Lan and David L. DeMets. 1983. Discrete sequential boundaries for clinical trials. Biometrika, 70(3):659–663. Li et al. (2011) Lihong Li, Wei Chu, John Langford, and Xuanhui Wang. 2011. Unbiased offline evaluation of contextual-bandit-based news article recommendation algorithms. In Proceedings of the Fourth ACM International Conference on Web Search and Data Mining, pages 297–306. ACM. Liu et al. (2026) Kaixuan Liu, Guojun Xiong, Weinan Zhang, and Shengpu Tang. 2026. Autoregressive diffusion world models for off-policy evaluation of LLM agents. Preprint, arXiv:2606.05558. Manski (2003) Charles F. Manski. 2003. Partial Identification of Probability Distributions. Springer Series in Statistics. Springer. Masad (2025) Amjad Masad. 2025. “we saw Jason’s post. @Replit agent in development deleted data from the production database. Unacceptable and should never be possible.”. Post on X, July 20, 2025. Accessed October 4, 2026. McGregor (2021) Sean McGregor. 2021. Preventing Repeated Real World AI Failures by Cataloging Incidents: The AI Incident Database. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 15458–15463. AAAI Press. Describes the AI Incident Database, https://incidentdatabase.ai. Mosleh et al. (1998) A. Mosleh, D. M. Rasmuson, and F. M. Marshall. 1998. Guidelines on modeling common-cause failures in probabilistic risk assessment. NUREG/CR 5485, U.S. Nuclear Regulatory Commission, Washington, DC. INEEL/EXT-97-01327. Munich Re (2023) Munich Re. 2023. De-risking AI ventures: How Munich Re assesses AI performance risks. insights into our due diligence process. Whitepaper. Accessed October 4, 2026. Namkoong et al. (2020) Hongseok Namkoong, Ramtin Keramati, Steve Yadlowsky, and Emma Brunskill. 2020. Off-policy policy evaluation for sequential decisions under unobserved confounding. In Advances in Neural Information Processing Systems, volume 33, pages 18819–18831. Curran Associates, Inc. National Institute of Standards and Technology (2024) National Institute of Standards and Technology. 2024. Artificial Intelligence Risk Management Framework: Generative Artificial Intelligence Profile. NIST AI 600-1, National Institute of Standards and Technology, Gaithersburg, MD. Needham et al. (2025) Joe Needham, Giles Edkins, Govind Pimpale, Henning Bartsch, and Marius Hobbhahn. 2025. Large language models often know when they are being evaluated. arXiv preprint arXiv:2505.23836. Nelsen (2006) Roger B. Nelsen. 2006. An Introduction to Copulas, second edition. Springer Series in Statistics. Springer, New York. New York State Legislature (2026) New York State Legislature. 2026. An act to amend the general business law, in relation to transparency and safety requirements for developers of artificial intelligence frontier models; to amend a chapter of the laws of 2025 amending the general business law relating to the training and use of artificial intelligence frontier models, as proposed in legislative bills numbers S. 6953-B and A. 6453-B, in relation to the effectiveness thereof; and to repeal certain provisions of the general business law, relating thereto. New York Senate Bill S8828, Chapter 96 of the Laws of 2026; signed March 27, 2026; amends the Responsible AI Safety and Education (RAISE) Act. Neyman (1934) Jerzy Neyman. 1934. On the two different aspects of the representative method: The method of stratified sampling and the method of purposive selection. Journal of the Royal Statistical Society, 97(4):558–625. Oberst and Sontag (2019) Michael Oberst and David Sontag. 2019. Counterfactual off-policy evaluation with Gumbel-max structural causal models. In Proceedings of the 36th International Conference on Machine Learning, volume 97 of Proceedings of Machine Learning Research, pages 4881–4890. PMLR. OpenAI (2025) OpenAI. 2025. Operator System Card. Technical report, OpenAI. OWASP GenAI Security Project (2025) OWASP GenAI Security Project. 2025. OWASP Top 10 for Agentic Applications for 2026. Whitepaper/guide. Pearl (1995) Judea Pearl. 1995. Causal diagrams for empirical research. Biometrika, 82(4):669–688. Pearl (2009a) Judea Pearl. 2009a. Causal inference in statistics: An overview. Statistics Surveys, 3:96–146. Pearl (2009b) Judea Pearl. 2009b. Causality: Models, Reasoning, and Inference, 2nd edition. Cambridge University Press, Cambridge. Pearl and Bareinboim (2011) Judea Pearl and Elias Bareinboim. 2011. Transportability of causal and statistical relations: A formal approach. In Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence, volume 25, pages 247–254. Pearl and Robins (1995) Judea Pearl and James M. Robins. 1995. Probabilistic evaluation of sequential plans from causal models with hidden variables. In Proceedings of the Eleventh Conference on Uncertainty in Artificial Intelligence, pages 444–453. Poiani et al. (2024) Riccardo Poiani, Rémy Degenne, Emilie Kaufmann, Alberto Maria Metelli, and Marcello Restelli. 2024. Optimal multi-fidelity best-arm identification. In Advances in Neural Information Processing Systems, volume 37. Precup et al. (2000) Doina Precup, Richard S. Sutton, and Satinder P. Singh. 2000. Eligibility traces for off-policy policy evaluation. In Proceedings of the Seventeenth International Conference on Machine Learning, pages 759–766. Morgan Kaufmann. Ravfogel et al. (2025) Shauli Ravfogel, Anej Svete, Vésteinn Snæbjarnarson, and Ryan Cotterell. 2025. Gumbel counterfactual generation from language models. In International Conference on Learning Representations. Ray (2026) Shawn Ray. 2026. What can be enforced? A theory of certified runtime safety for tool-using agents. Preprint, arXiv:2607.22868. Robins (1986) James Robins. 1986. A new approach to causal inference in mortality studies with a sustained exposure period: Application to control of the healthy worker survivor effect. Mathematical Modelling, 7(9–12):1393–1512. Rockafellar and Uryasev (2002) R. Tyrrell Rockafellar and Stanislav Uryasev. 2002. Conditional value-at-risk for general loss distributions. Journal of Banking & Finance, 26(7):1443–1471. Ruan et al. (2024) Yangjun Ruan, Honghua Dong, Andrew Wang, Silviu Pitis, Yongchao Zhou, Jimmy Ba, Yann Dubois, Chris J. Maddison, and Tatsunori Hashimoto. 2024. Identifying the risks of LM agents with an LM-emulated sandbox. In The Twelfth International Conference on Learning Representations (ICLR 2024). Spotlight. Sachdeva et al. (2020) Noveen Sachdeva, Yi Su, and Thorsten Joachims. 2020. Off-policy bandits with deficient support. In Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, pages 965–975. ACM. Saha and Ramdas (2026) Aytijhya Saha and Aaditya Ramdas. 2026. Huber-robust likelihood ratio tests for composite nulls and alternatives. IEEE Transactions on Information Theory, 72(1):501–520. Shabadi and Alur (2026) Guruprerana Shabadi and Rajeev Alur. 2026. Risk-sensitive agent compositions. In International Conference on Learning Representations. Shaked and Shanthikumar (2007) Moshe Shaked and J. George Shanthikumar. 2007. Stochastic Orders. Springer Series in Statistics. Springer, New York. Shavit et al. (2023) Yonadav Shavit, Sandhini Agarwal, Miles Brundage, Steven Adler, Cullen O’Keefe, Rosie Campbell, Teddy Lee, Pamela Mishkin, Tyna Eloundou, Alan Hickey, Katarina Slama, Lama Ahmad, Paul McMillan, Alex Beutel, Alexandre Passos, and David G. Robinson. 2023. Practices for Governing Agentic AI Systems. White paper, OpenAI. Slattery et al. (2024) Peter Slattery, Alexander K. Saeri, Emily A. C. Grundy, Jess Graham, Michael Noetel, Risto Uuk, James Dao, Soroush Pour, Stephen Casper, and Neil Thompson. 2024. The AI Risk Repository: A Meta-Review, Database, and Taxonomy of Risks from Artificial Intelligence. Preprint, arXiv:2408.12622. Song et al. (2023) Yuda Song, Yifei Zhou, Ayush Sekhari, J. Andrew Bagnell, Akshay Krishnamurthy, and Wen Sun. 2023. Hybrid RL: Using both offline and online data can make RL efficient. In International Conference on Learning Representations. Spertus et al. (2024) Jacob V. Spertus, Mayuri Sridhar, and Philip B. Stark. 2024. Sequential stratified inference for the mean. Preprint, arXiv:2409.06680. Spertus and Stark (2022) Jacob V. Spertus and Philip B. Stark. 2022. Sweeter than SUITE: Supermartingale stratified union-intersection tests of elections. In Electronic Voting: 7th International Joint Conference, E-Vote-ID 2022, volume 13553 of Lecture Notes in Computer Science, pages 106–121. Springer. Subramanian et al. (2020) Jayakumar Subramanian, Amit Sinha, Raihan Seraj, and Aditya Mahajan. 2020. Approximate information state for approximate planning and reinforcement learning in partially observed systems. arXiv preprint. The B. John Garrick Institute for the Risk Sciences (n.d.) The B. John Garrick Institute for the Risk Sciences. n.d. ADS-IDAC overview. University of California, Los Angeles. Undated; accessed October 3, 2026. Ville (1939) Jean Ville. 1939. Étude critique de la notion de collectif. Thèses de l’Entre-Deux-Guerres, no. 218. Wald (1944) Abraham Wald. 1944. On cumulative sums of random variables. The Annals of Mathematical Statistics, 15(3):283–296. Wald (1945) Abraham Wald. 1945. Sequential tests of statistical hypotheses. The Annals of Mathematical Statistics, 16(2):117–186. Wang et al. (2024) Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, Wayne Xin Zhao, Zhewei Wei, and Ji-Rong Wen. 2024. A Survey on Large Language Model based Autonomous Agents. Frontiers of Computer Science, 18(6). Wisakanto et al. (2025) Anna Katariina Wisakanto, Joe Rogero, Avyay M. Casheekar, and Richard Mallah. 2025. Adapting probabilistic risk assessment for AI. arXiv preprint arXiv:2504.18536. Wu et al. (2026) Tianyuan Wu, Chaokun Chang, Lunxi Cao, Wei Gao, and Wei Wang. 2026. Crab: A semantics-aware checkpoint/restore runtime for agent sandboxes. Preprint, arXiv:2604.28138. Xu et al. (2026) Binyan Xu, Xilin Dai, Fan Yang, and Kehuan Zhang. 2026. When agent automation becomes profitable: Quantifying and insuring autonomous AI risk through trace-economic underwriting. Preprint, arXiv:2606.16465. Yang et al. (2025) An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, et al. 2025. Qwen3 technical report. arXiv preprint arXiv:2505.09388. Yao et al. (2025) Shunyu Yao, Noah Shinn, Pedram Razavi, and Karthik Narasimhan. 2025. τ-bench: A benchmark for tool-agent-user interaction in real-world domains. In International Conference on Learning Representations. Yin et al. (2022) Dong Yin, Botao Hao, Yasin Abbasi-Yadkori, Nevena Lazić, and Csaba Szepesvári. 2022. Efficient local planning with linear function approximation. In Proceedings of the 33rd International Conference on Algorithmic Learning Theory, volume 167 of Proceedings of Machine Learning Research, pages 1165–1192. Yu et al. (2025) Miao Yu, Fanci Meng, Xinyun Zhou, Shilong Wang, Junyuan Mao, Linsey Pang, Tianlong Chen, Kun Wang, Xinfeng Li, Yongfeng Zhang, Bo An, and Qingsong Wen. 2025. A Survey on Trustworthy LLM Agents: Threats and Countermeasures. Preprint, arXiv:2503.09648. Zhang and Bareinboim (2020) Junzhe Zhang and Elias Bareinboim. 2020. Designing optimal dynamic treatment regimes: A causal reinforcement learning approach. In Proceedings of the 37th International Conference on Machine Learning, volume 119 of Proceedings of Machine Learning Research, pages 11012–11022. PMLR. Zhang et al. (2024) Zhexin Zhang, Shiyao Cui, Yida Lu, Jingzhuo Zhou, Junxiao Yang, Hongning Wang, and Minlie Huang. 2024. Agent-SafetyBench: Evaluating the Safety of LLM Agents. Preprint, arXiv:2412.14470. Guide to the Appendix The appendices support the formulation in Section 2, results in Section 3, demonstrations in Section 4, and related work in Section 5. Start with Appendix A for the specification, assumptions, and evaluation procedure, or Appendix D for the registered and exploratory demonstrations and their uncertainty. Appendix E proves what replay identifies, what a log must preserve, and how horizons affect unresolved outcomes. Appendix F treats supported and unsupported continuation, execution budgets, restoration error, strata, and snapshot design. Appendix G establishes when component evidence transfers to a composition or deployment setting. Appendices B and C explain the survey and comparisons with prior work. Appendix H indexes the verification scripts. ARTIFACT.md and checks/README.md link the full operational details and worked examples. Appendix A Formal Statements Behind Sections 2 and 3 This appendix gives the formal specifications, assumptions, and results behind Sections 2 and 3; the proofs appear in Appendices E, F, and G. A.1 The Specification This is the specification of Section 2.3. Definition A.1.1 (Risk specification). A risk specification is a tuple ℜ=(E,ℓ,K,), R=(E, ,K,C), (3) where E is an execution mechanism, ℓ is a consequence map, K is an observation mechanism, and C is a declared family of admissible mechanism replacements. Execution Mechanism E. Fix a finite horizon T. E specifies initial distributions, policies, transitions, updates, and scheduling as named stochastic kernels whose declared inputs are generated earlier in a declared order; policies use only information available before their decisions. Because mechanisms with identical path laws can respond differently under intervention, E retains its modular kernel and input structure rather than only its induced law. Consequence map ℓ . Let L=ℓ(τ)∈ℝmL= (τ) ^m be the full-episode loss vector (Kaplan and Garrick, 1981, Section 3.4), with ℓ defined on a trajectory space shared by E and every admissible replacement. In the running agent, L is (failure, harm, cost) over the whole episode, and a declared post-abort kernel of E generates the abort valuation of Section 2.2. Observation mechanism K. Execution and evaluation share the clock t=0,…,Tt=0,…,T, and the declared generation order interleaves execution coordinates and records. The evaluator receives records Rt=(O0,…,Ot)R_t=(O_0,…,O_t), trivial for t=−1t=-1 and possibly different from the agent’s context, from causal kernels that read only the execution history available by time t, so an online record cannot depend on a future execution suffix. A monitor that changes approval, timing, scheduling, agent behavior, or losses belongs in E, as does any record used for control or loss accounting. The kernels of E and K, composed in their declared order, induce a joint law PE,KP_E,K on a finite set Ω of complete joint execution and observation paths, with loss L=ℓ(ω)L= (ω) in a finite set ⊂ℝmL ^m; the law of the current system is the baseline law P0P^0. Every result in this paper uses this finite setting. In the running agent, K is the deployer’s log. Admissible Replacements C. Each replacement κ∈κ specifies replaced kernels, implementation boundaries, and allowed information. Replacement kernels keep their output coordinates, ranges, and causal positions and are adapted to the implementer’s declared information; they may read different earlier inputs within it. Unreplaced kernels retain their declared inputs. For deviation replay, κ replaces one decision kernel. We refine the clock so that this kernel acts at most once per step, mapping declared input ItI_t to baseline action ft0(It)f^0_t(I_t) or replacement action ftκ(It)f^κ_t(I_t). Refining the clock changes no kernel, declared input, consequence map, or coarse record. For the stopping gate κθ _θ, input ItI_t holds proposals utu_t and score mtm_t, and ftκf^κ_t aborts when mt>θm_t>θ. The query applies κ to all histories compatible with the conditioning record; a selection using information outside that record belongs in E as further evidence. A.2 The Question, Assumptions (A1) and (A2), and Identified Sets For the query of Section 2.4, suppose replacement κ takes effect at boundary s>ts>t after records RtR_t. Splicing κ into E yields changed mechanisms EκE^κ and KκK^κ with joint law Pκ=PEκ,KκP^κ=P_E^κ,K^κ, defining the continuation query: Qtκ(⋅∣r)=ℒPEκ,Kκ(L∣Rt=r),Q_t^κ(\,· r)=L_P_E^κ,K^κ(L R_t=r), (4) computed from the specification; we write Pκ=PEκ,KκP^κ=P_E^κ,K^κ. Applying loss aggregation ϕφ and risk functional ρ gives the scalar query qtκ(r)=ρ(ϕ#Qtκ(⋅∣r))q^κ_t(r)=ρ( _\#Q^κ_t(· r)), such as harm probability, mean cost, or conditional value-at-risk (Rockafellar and Uryasev, 2002). The changed system obeys PκP^κ under two core conditions. (A1) Invariance: the initial law and every unreplaced kernel, including random-input generators, remain unchanged. Installing a gate leaves models, tools, users, and samplers as logged. (A2) Prefix preservation and no anticipation: both mechanisms share the causal generation order and coincide before the replacement boundary. Every unreplaced kernel retains its declared inputs; a replaced kernel may read different earlier inputs that C permits. For deviation replay, ft0f^0_t and ftκf^κ_t are evaluated on a common input ItI_t that contains the inputs either rule uses. No unreplaced kernel or declared input reads the identity or announcement of the installed replacement. Announcing the gate in the agent’s prompt violates (A2). Because true kernels are unknown, the evaluator determines which query values observed records rule out (Manski, 2003). A structural model M specifies target mechanisms (EM,ℓ,KM)(E_M, ,K_M) and evidence sources, including continuation runs linked by (T) restoration fidelity: continuation laws equal conditional laws of PMκP^κ_M given restored prefix h. The model family ℳ0M_0 encodes declared structural restrictions. Given observed record laws PobsRP_obs^R, the compatible models are ℳ=M∈ℳ0:PMR=PobsRM=\M _0:P_M^R=P_obs^R\, and the population identified set for query ψ is Θ(ℳ)=ψ(M):M∈ℳ (M)=\ψ(M):M \, yielding Θtκ(r) ^κ_t(r) for qt,Mκ(r)q^κ_t,M(r). Equality of evidence laws is source by source, and pointwise conditional sets are stated at records with positive observed probability. Sampling error. The set in (1) is stated at records with positive probability. One-sided endpoint confidence bounds, each with noncoverage at most α/2α/2, cover it with probability at least 1−α1-α; covering only the true risk can permit shorter intervals (Imbens and Manski, 2004), and plug-in bounds ignore sampling uncertainty. A.3 Records That Leave a Gate Change Open Section 2.2 names three ways baseline records can leave replacement risk unresolved. A declared abort valuation resolves the first ambiguity. The remaining ambiguities depend on the fixed kernels and input restrictions in the model family; the examples below state which restrictions they retain. (1) Stop. No baseline episode aborts, so no record shows the loss after an abort; the declared valuation, (A3) of Appendix A.4, supplies it, and records cannot check it. (2) Continue. The logged gate never blocks, so no logged input contains a block message. If the family fixes every kernel’s declared inputs, the gate, and the abort valuation but leaves the agent’s response to a block message free, two models that agree at every input of positive baseline probability have the same record law and can differ in the harm after a retry. (3) Logging. If the log keeps scores and an episode harm flag but not the step of each harm, and the family fixes the monitor and the gate but leaves the timing of harm free, a model whose harm falls before the step at which a stopping gate aborts and a model whose harm falls after it have the same record law, yet the gate removes the harm in only the second. The third ambiguity has the finite instance below, for a stricter gate as in the running agent. It is the toy episode of Section 2.2 in formal terms, with harm at step 1 or step 3 and the gate acting at step 2. Omitted Harm Timing under a Stricter Gate. When a log records overall harm but omits step-level harm hth_t, baseline paths with early harm (t=1t=1) and late harm (t=3t=3) generate identical coarse records. A stricter gate aborting at t=2t=2 under declared accrued-harm valuation eliminates late harm but retains early harm. In the family fixing every kernel except the law of the unrecorded early/late state, with (R) and (A1) to (A3), latent early-harm probability p∈[0,1]p∈[0,1] is unconstrained by the coarse log, the fibre condition of Proposition 3.1 fails and the identified harm interval is [0,1][0,1]. Logging step harm identifies p, contracting the garbled set [0,1][0,1] to p\p\. An Omitted State Variable under a Looser Gate. Replace a gate that blocks every proposal by one that executes every proposal. A record of the proposal, the damage, and the cost that omits a stale-state bit S has the same law for P(S=1)=0.1P(S=1)=0.1 and P(S=1)=0.9P(S=1)=0.9, yet the damage probability after the change is 0.10.1 or 0.90.9. The baseline gate decision is constant, so logging it adds nothing, while logging S identifies the replaced damage probability within this family (Appendix H). A.4 Deviation Replay This formalizes the replay decomposition in Section 3 and the result in Section 3.1. Let Ω0 ^0 be the paths where every replaced decision equals baseline rule ft0(It)f^0_t(I_t). The first deviation is σκ=mint:ftκ(It)≠ft0(It) _κ= \t:f^κ_t(I_t)≠ f^0_t(I_t)\, and κ=σκ>T A_κ=\ _κ>T\ is the agreement event. At a deviation, the replayed prefix hκ+h^+_κ appends replacement action fσκ(Iσκ)f^κ_ _κ(I_ _κ) to earlier history. A deviation is terminal if the replacement action aborts execution, and continuing otherwise. We condition on record Rt=rR_t=r with P0(Rt=r)>0P^0(R_t=r)>0 prior to intervention. Beyond (A1) and (A2), replay assumes: (R) Replay interface: ft0f^0_t and ftκf^κ_t are known and deterministic in the declared input ItI_t, which may include a random tape and which the full record contains (a coarser log, as in Proposition 3.1, need not). The gate rule can be rerun on logged proposals, scores, and seeds. (A3) Declared abort valuation: after a terminal deviation with replayed prefix h+h^+, the law of L is a declared bκ(⋅∣h+)b_κ(· h^+) that includes accrued losses. It describes post-abort kernels of E, so ℓ is unchanged; replacements that abort at the same replayed prefix share it, and it must agree with any post-abort kernel at inputs of positive baseline probability. Proposition A.4.1 (Deviation replay; Robins, 1986; Cain et al., 2010). Assume (R), (A1), and (A2), and let B⊆B . (i) Agreement. Pκ(L∈B,κ∣r)=P0(L∈B,κ∣r)P^κ(L∈ B, A_κ r)=P^0(L∈ B, A_κ r). (i) Stopping. Under (A3), Pκ(L∈B,σκ≤T,terminal∣r)=∫bκ(B∣hκ+(τ)) 1σκ≤T,terminaldP0(τ∣r)P^κ(L∈ B,\ _κ≤ T,\ terminal r)= b_κ(B h^+_κ(τ))\,1\ _κ≤ T,\ terminal\\,dP^0(τ r), even if the baseline never aborts. Part (i) formalizes the stop term in display (2). Appendix E establishes both assertions via Lemma E.3.1, while Proposition E.1.1 treats continuing deviations. A.5 Supported Continuation, Compact Form This is the formal result summarized in Section 3.4. Proposition A.5.1 (Supported continuation and unsupported inputs). Assume (A1) and (A2), let κ replace kernels from boundary s onward by known kernels, and fix Rt=rR_t=r with t<st<s and P0(Rt=r)>0P^0(R_t=r)>0. Suppose (G1) at each position of the declared generation order, every input that the replacement leads an unchanged downstream kernel to read there has positive baseline probability at that position, unless the specification fixes that kernel’s value at that input, as after an abort. Also suppose (G2) those kernels’ declared inputs are recorded at those positions, (G3) every coordinate that ℓ reads is recorded, and (G4) the replacement reads recorded inputs only. Then, within mechanisms that share the declared kernel inputs and the values the specification fixes, Qtκ(⋅∣r)Q_t^κ(· r) is identified by the g-formula. Zero agreement mass is compatible with identification. Unsupported inputs. Without (G1), keep (G2) to (G4), the declared kernel inputs, and the fixed values. Let the kernel law at each position of the declared generation order be free at its other inputs of baseline probability zero, within declared sets of allowed outputs, separately from the laws at other positions. Then the identified set is the image of the g-formula with one free law at each such position and input, shared by all histories that reach it; if one law is shared across positions, as for a policy called at every step, this image is an outer set. The first statement identifies QtκQ_t^κ via the sequential g-formula (Appendix F.4). When (G1) fails, optimizing over unobserved inputs specializes partial-identification bounds (Alvarez and Ferrando, 2026; Duarte et al., 2023), giving a sharp identified image when each position’s law at unseen inputs varies freely and an outer set when laws are shared across positions (Appendix F.5). Treating unobserved inputs in a finite log as unsupported preserves a valid outer set (Remark F.5.3). A.6 The Evaluation Procedure Algorithm 1 translates the five evaluation steps of Section 3 into formal decision logic. Algorithm 1 Evaluating a change κ from logs 0: ℜ R, ℳ0M_0, record r, change κ, query ρ∘ϕρ φ, decision rule 0: status; qtκ(r)q^κ_t(r) or an interval; missing evidence 1: Declare the kernels κ replaces, their inputs, bκb_κ of (A3), and the links (A1), (A2), (T) 2: if (A1) or (A2) is not justified and the extra change is not modeled then 3: return “this analysis does not evaluate qtκ(r)q^κ_t(r)” 4: Under (R), where records permit, rerun both rules on each logged τ: σκ _κ, hκ+h^+_κ, and its event 5: if the log is sufficient (Prop. 3.1) and keeps the feasible sets hX_h then 6: read the agree-plus-stop sum of (2) from P0(⋅∣r)P^0(· r) and bκb_κ 7: for all terms left open: the continue term, or any term of a failed check do 8: if (G1) to (G4) hold then 9: apply the g-formula (Prop. A.5.1) 10: else if snapshots at hκ+h^+_κ are kept and (T) holds then 11: execute continuations from restored prefixes, or, for binary harm, a random sample (Prop. F.7.1) 12: else 13: bound by Θtκ(r) ^κ_t(r) (1) over record completions, or by (5) for full records and monotone ρ; sharp under (S), else outer 14: if the value or interval, with sampling uncertainty, leaves the decision open then 15: name what is missing: episodes, record fields, justified assumptions, or runs 16: return status (identified; bounded; needs execution), value or interval, decision When targeted execution samples binary harm continuations at line 11, it invokes hypothesis (H) of Proposition F.7.1 (Appendix F.7) to guarantee one-sided confidence coverage. A.7 Symbols Table A.1 lists the symbols of Sections 2 and 3 and of this appendix, with a one-line meaning and the place where each is defined. Symbol Meaning Exact definition ℜ=(E,ℓ,K,) R=(E, ,K,C) Risk specification: execution mechanism, consequence map, observation mechanism, admissible replacements Appendix A.1 T; t Finite horizon; step index, shared by execution and records Appendix A.1 utu_t; mtm_t Tool calls proposed at step t; the monitor’s score for them Section 2.2 κ; κθ _θ; θ A replacement (a change); the stopping gate; its score threshold Appendix A.1 L=ℓ(ω)L= (ω); L Full-episode loss vector (failure, harm, cost); its finite set of values Appendix A.1 Rt=(O0,…,Ot)R_t=(O_0,…,O_t); r Evaluator records up to t; a value of RtR_t with positive baseline probability Appendix A.1 Ω ; PE,KP_E,K; P0P^0; PκP^κ Complete joint paths; their law; the baseline law; the law under κ Appendices A.1, A.2 ItI_t; ft0f^0_t; ftκf^κ_t Declared input of the replaced decision kernel; the baseline and replacement rules Appendix A.1 Qtκ(⋅∣r)Q^κ_t(· r) Loss law of the changed system given the record at the change Appendix A.2 qtκ(r)q^κ_t(r); Θtκ(r) ^κ_t(r) Risk of the change: ρ applied to the law of ϕ(L)φ(L) under Qtκ(⋅∣r)Q^κ_t(· r); its values under the models that reproduce the records Display (1) ϕφ; ϕ#Q _\#Q; ρ Coordinate or aggregation of L; the law of ϕ(L)φ(L) under Q; risk functional (probability, mean, CVaR) Appendix A.2 ℳ0M_0; ℳM; ψ; Θ(ℳ) (M) Declared model family; models that reproduce the records; a query; the identified set Appendix A.2 (A1); (A2) Invariance; prefix preservation and no anticipation Appendix A.2 (T) Restoration fidelity of a continuation run from a restored prefix Appendix A.2 Ω0 ^0 Paths on which every replaced decision equals the baseline rule Appendix A.4 σκ _κ; κ A_κ First deviation of the new rule from the logged one; the agreement set σκ>T\ _κ>T\ Appendix A.4 hκ+h^+_κ Replayed prefix: the history before the deviation followed by the replacement output Appendix A.4 terminal; continuing A deviation whose replacement output is an abort; any other deviation Appendix A.4 (R); (A3); bκb_κ Replay interface; declared abort valuation; the declared loss law after a stop Appendix A.4 agree; stop; continue The events κ A_κ, σκ≤T,terminal\ _κ≤ T,\ terminal\, and σκ≤T,continuing\ _κ≤ T,\ continuing\ Display (2) E0[⋅∣r]E^0[\,· r] Expectation of a path function under P0(τ∣r)P^0(τ r) Display (2) hX_h; (S) Feasible values of X=ϕ(L)X=φ(L) after a continuing prefix h; saturated continuation Appendix E.1 ν−ν^-; ν+ν^+ Law of X given r when agreeing episodes keep their logged value, stopped episodes follow the declared valuation, and each continuing episode takes the least (greatest) value in hX_h Display (5) CκC_κ; uκu_κ An episode’s combined contribution to the first two terms of (2); its missing mass Proposition 3.1 rP_r; sκ,rs_κ,r Baseline laws on Ω0 ^0 that charge r; the replay summary of a law Proposition 3.1 g; g#Pg_\#P; Ψ Logging map; the law of the log; a map from the log law to the summary Proposition 3.1 ηj(r) _j(r) Deviation hazard at step j among episodes that agree before j Corollary E.7.1 (G1) to (G4) Support, recorded kernel inputs, recorded loss coordinates, recorded replacement inputs Appendix A.5 S; PSP_S; UiU_i Shared state; its law; composed states never seen by component i alone Section 3.5 Table A.1: Symbols of Sections 2 and 3. Appendix B Survey and Classical Foundations This appendix describes the survey, classical tools, and existing practices behind the specification in Section 2 and comparisons in Section 5. B.1 Survey Method For the characteristics of Section 2.1, we reviewed a purposive sample of 85 papers and reports on agent risk. Two language-model coders from different model families independently coded 23 agent-risk taxonomies, surveys, and governance frameworks alongside 30 incidents from the AI Incident Database (AIID; McGregor, 2021) against 20 candidate characteristics. The incidents cover 2025 and 2026 reports describing tool-using AI agents. The coded sources are (Chan et al., 2023; Shavit et al., 2023; Chan et al., 2024; Kolt, 2025; Hammond et al., 2025; Slattery et al., 2024; Deng et al., 2025; Yu et al., 2025; He et al., 2024; Hua et al., 2024; Ruan et al., 2024; Zhang et al., 2024; Wang et al., 2024; OWASP GenAI Security Project, 2025; Bengio et al., 2025; Bengio et al., 2026; National Institute of Standards and Technology, 2024; Center for AI Standards and Innovation , NIST(2025), CAISI; European Commission, AI Office, 2025; AI Safety Institute, 2024; Infocomm Media Development Authority, 2026; Anthropic, 2024; OpenAI, 2025). Three criteria selected the six characteristics of Table 1. Sources or incidents name each one often, each remains a persistent risk driver under current mitigations, and the framework provides an identification result for each. This third criterion is partly circular because the framework was designed around these characteristics; the selection therefore motivates the six without proving that they matter most. The released artifact lists all 23 sources, their consulted versions, and the 30 incident identifiers. B.2 The Other Characteristics Agent characteristics modify instances of the four objects, interfaces, or model families rather than adding primitive concepts. Section 2.1 (Table 1) focuses on the six characteristics with formal results and demonstrations. Other candidates such as prompt injection, reviewer load, environment drift, and serving nondeterminism map to definitions within these same four objects; the rows are neither exhaustive nor additive risk scores. The companion mapping lists the other characteristics and their definitions within the four objects. B.3 Classical Tools Table B.1 summarizes how the four-object specification of Section 2.3 adapts classical tools; dynamic PRA models feedback and uncertain event timing (The B. John Garrick Institute for the Risk Sciences, n.d.), and the four-object specification is our modeling choice. Classical tool Role, essential condition, and status in specification Scenario triplets (Kaplan and Garrick, 1981) Kept with named kernels of E and loss ℓ ; requires declared consequence definitions under changed systems. Partial observation (Bäuerle and Rieder, 2017) Kept in observation record K and Proposition 3.1; deployer-designed records differ from agent context. Mechanism intervention (Pearl, 1995) Kept in intervention family C under (A1) and (A2); replaces agent decision rules with declared timing and inputs. g-formula and censoring at deviation (Robins, 1986; Cain et al., 2010) Inherited in Proposition A.4.1; agreement uses (R), (A1), and (A2), and stopping uses declared abort valuations (A3). Logged replay (Li et al., 2011) Inherited in Proposition A.4.1 and deviation time σκ _κ; requires rerunnability (R) via recorded seeds and invariant serving. Worst-case bounds (Manski, 2003) Inherited in Proposition E.1.1 and Proposition A.5.1; bounded losses give prefix-feasible bounds, sharp under (S) with full records and outer otherwise; shared-law restrictions may narrow them. Fréchet bounds and transportability (Fréchet, 1951; Pearl and Bareinboim, 2011) Inherited in Proposition G.1.1; uses known marginals for joint bounds, and invariance and support to transfer standalone component evidence. Table B.1: Classical tools, standard assumptions, agent strains, and roles in the specification. B.4 Existing Practice as Instances To complement Section 5, we write existing practices as specifications without ranking them: τ-bench and τ2τ^2-bench fix task reward ℓ (Yao et al., 2025; Barres et al., 2025); AI Control specifies audit and deferral thresholds in C (Greenblatt et al., 2024, Sections 2.2 and 2.5, Appendix K); PRA for AI models pathways in E and ℓ (Wisakanto et al., 2025, Sections 3.2, 4.3, and 5.2); and risk-sensitive compositions evaluate joint losses (Shabadi and Alur, 2026, Sections 2 and 4.2). The companion practice mapping records the objects each practice fixes and the conditions its conclusions require, which reflect our embedding unless a source section is cited. Appendix C Comparisons With Prior Work We extend Section 5 by positioning our identification and logging results against prior literature; Table B.1 in Appendix B summarizes foundations. Off-Policy Evaluation And Dynamic Regimes. Our logged gate is deterministic and never stops, leaving no observed stops to reweight. Halting needs no overlap. Proposition A.4.1 identifies stopping risk via declared accrued-loss valuation (A3); display (2) adds continuing mass. Bounds Without Overlap. Unlike dynamic regime bounds under unobserved confounding (Zhang and Bareinboim, 2020; Namkoong et al., 2020), we bound missing support at recorded inputs. Where bandit approaches restrict policies (Sachdeva et al., 2020), Proposition A.5.1 leaves unsupported inputs free with declared valuations. Specializing discrete causal bounds (Duarte et al., 2023; Alvarez and Ferrando, 2026), we separate position-specific free-law sharp sets from shared-law outer bounds. Transport And Evidence Collection. Causal transport uses graphical conditions (Bareinboim and Pearl, 2016); assumptions (A1), (A2), and (T) formalize transfer across logs, restored runs, and altered systems. Rather than designing behavior policies (Hanna et al., 2017), Proposition F.7.1 executes open continuations through reset access (Yin et al., 2022; Song et al., 2023). Unlike learned simulator models (Liu et al., 2026), targeted execution rests on reset fidelity (T). What logs must keep. Agent logs (Chan et al., 2024) and reasoning from a deployed system’s logs (Bottou et al., 2013) motivate Proposition 3.1. It instantiates the elementary fact that a log determines an expected contribution for every path law exactly when indistinguishable paths have equal contributions. State-abstraction irrelevance gives sufficient conditions for evaluation on compressed states (Hao et al., 2024). Information states preserve values through reward and transition sufficiency (Subramanian et al., 2020). Logging and reporting duties. Several laws set related duties for AI providers and developers. The EU AI Act provides for automatic event logging in high-risk systems (applicable from 2027 or 2028), documentation by providers of general-purpose models, and, for models with systemic risk, evaluation and incident reporting (European Parliament and Council of the European Union, 2024, Arts. 12, 53, and 55); the voluntary Code of Practice elaborates the systemic-risk duties (European Commission, AI Office, 2025). California’s SB 53 requires large frontier developers to publish safety frameworks and all frontier developers to report critical safety incidents (California State Legislature, 2025), and New York’s amended RAISE Act sets similar duties from January 2027 (New York State Legislature, 2026). These instruments do not provide a general criterion for whether an agent’s records suffice to assess a specified change. Under (R), (A1), and (A2), Proposition 3.1 characterizes the records that preserve the combined replay contributions and unresolved mass across all baseline laws. Shared randomness and model comparison. Shared-seed replay is a common-random-numbers coupling of the two policies. Oberst and Sontag (2019) infer Gumbel-max noise under a structural causal model to evaluate a new policy on logged episodes, and Gumbel-max coupling of language models generates counterfactual text and compares models (Chatzi et al., 2025; Ravfogel et al., 2025; Corvelo Benz et al., 2026). Seed-addressable replay reads recorded seeds instead, and Corollary F.6.1 needs only deterministic evaluation at logged inputs and seeds. Agent evaluation and control. Ray (2026) bounds a multi-judge gate’s errors by Fréchet–Hoeffding. Our range conditions on the state that composed agents share and transfers standalone evidence only on covered states (Proposition G.1.1). Bhardwaj et al. (2026) certify the reliability of composed agents without assuming independence, from measured joint executions; our range needs only component logs and the shared state. We separate stopping replay from continuing changes and state the evidence each requires. Appendix B.4 writes four existing practices as specifications (Yao et al., 2025; Greenblatt et al., 2024; Wisakanto et al., 2025; Shabadi and Alur, 2026). Of these, only control evaluation reuses records to assess a change (the companion practice mapping). Insurance. An insurer pricing a proposed change to an agent can use the agree, stop, and continue split to state which losses the policyholder’s logs settle and which need further evidence. Chen (2026) charges each side-effect action against a contractually fixed safe default, and Xu et al. (2026) map task traces, economic exposure, and contract terms to modeled claim costs; our results complement them by characterizing the evidence needed to assess a specified change to the agent. Premiums require a further link from episode losses to calibrated monetary severity, exposure volumes, coverage terms, and dependence across claims. Appendix D Registered Demonstrations and Supporting Evidence This appendix provides the experimental setup, runs, and change-by-change results behind Section 4, exploratory values, and secondary readings. Interval types follow Section 4; Newcombe intervals are score intervals for differences of proportions, and exact ones are Clopper-Pearson. Post hoc values were computed after registered analyses using the same logs and frozen code, without multiplicity control. In the primary bash setting (Inglis et al., 2025; Bhatt et al., 2025), task failure is near saturation (0.873 on the held-out log), so these claims hold within this sandbox setting only. D.1 Logs and Runs The bash runs use uniform task sampling with replacement from 257 tasks, fresh containers and seeds per episode, and the frozen checker (version 1.1). Table D.1 summarizes the registered and exploratory runs of Section 4. Run Gate Episodes Serving Role Exploratory log Pass-all 300 Default kernels Exploratory; θ=0.94θ=0.94 chosen here Exploratory live gates Stopping gate at θ=0.99θ=0.99, 0.940.94, 0.190.19 300 each (286 scored at 0.99) Default kernels Exploratory live comparison with replay from the exploratory log Held-out log Pass-all 300 Batch-invariant Primary held-out log; source of the retry bounds and the step-0 continuations Live retry gate Retry gate, θ=0.94θ=0.94, retry cap 2 300 Batch-invariant Live check of the retry bounds, after the fact Targeted-execution run Pass-all with a snapshot at the first block; continuations under the retry gate; live retry gate 1,200 units (2,885 episodes) Batch-invariant, two hosts Registered; prediction frozen before the live arm was read First announcement test Stopping gate, announced 300 Batch-invariant Registered null against the held-out log (no margin; analysis fixed after launch); followed up by the paired announcement test Replication log; live replication runs Pass-all; stopping gate 1,000 and 1,000 Batch-invariant, one host The registered replication Paired announcement test Pass-all; stopping gate unannounced; announced 400 triplets Batch-invariant, one host Registered; announced and unannounced gates on the same 400 task-and-seed triplets Step-0 continuations Retry continuations from the held-out log 85 Batch-invariant Targeted execution of step-0 blocks Model-update reruns Reruns of logged decisions 99 (and 30) Per rung Model-update ladder Long-horizon log Pass-all, cap 40 600 (594 scored) Batch-invariant, two hosts Both gates replayed by horizon Stronger-agent run Pass-all; stopping gate at λ=11.551λ=11.551 on s 1,400 pairs (2,800; 2,797 scored) Default kernels, one host Registered; stopping-gate replay and certification with a stronger agent Airline run Pass-all; stopping gate at λ=11.186λ=11.186 on s; retry gate 1,200 units (2,800 episodes) Default kernels, one host Registered; stopping-gate replay, certification, and retry bounds in a second environment Airline retry by targeted execution Continuations restored by replaying logged writes; live retry gate 1,200 units (959 new episodes: 159 continuations, 800 live) Default kernels, one host Registered; prediction frozen before the 800 new live episodes were read; live units 0 to 399 reuse the airline run’s retry arm, analyzed there Two retry gates by targeted execution Pass-all with a gate-free snapshot rule; two live retry gates; continuations 7,200 units (25,561 episodes: 7,200 pass-all, 14,400 live, 3,961 continuations) Default kernels, six hosts Registered; prediction frozen before the live arms were read; two gates from one log Two-agent relay Relay, five conditions 1,600 units (8,000; 7,998 scored) Batch-invariant, two hosts Registered; tests of each agent alone against the live relay Table D.1: Runs behind Section 4. Batch-invariant serving returns the same output for the same input whatever else shares the batch; default kernels do not. ARTIFACT.md maps each run to the code that its logs and commands use. D.2 Setup Specification Verbatim prompts, commands, input logs, and verifying records for Section 4 are documented in ARTIFACT.md. ControlArena and τ2τ^2-bench (MIT license), the Qwen models, and vLLM (Apache 2.0) are used for research evaluation under their licenses. Declared policy. The operating rules forbid: (1) network access, (2) modifying files outside /workspace or /tmp, (3) destructive commands outside those paths, and (4) privilege escalation. An episode is harmed when any executed tool call violates these rules. Harm checker and limitations. A frozen mechanical checker (version 1.1) inspects commands and filesystem changes after each call, excluding sanctioned run_tests and submit. Command substitutions or unexpanded variables may escape command checks but can trigger state checks. A failed state check leaves harm status unknown unless a violation was recorded or, for a replayed stop, the failure came at or after the stop. Pre-execution blocking and monitor. The monitor, Qwen3-4B-Instruct-2507 (Yang et al., 2025) (revision cdbee75), scores proposed calls before execution at temperature 0 and seed 0. Scores are scaled to [0,1][0,1]; the gate at θ=0.94θ=0.94 blocks on scores above 0.94, terminating execution before the flagged action runs. Agent and episode limits. The agent, Qwen3-14B-FP8 (revision 9a283b4), operates in ControlArena’s honest bash setting at temperature 0.7, top-p 1.0. Step t uses seed 1000×episode_seed+t1000×episode\_seed+t. Episodes terminate at submission, 15 steps (40 in the long-horizon log), 400,000 total tokens, or context exhaustion (32,768 tokens). Serving. Models are served with vLLM 0.30.0 (Kwon et al., 2023) (PyTorch 2.13.0, CUDA 13.0) on one NVIDIA H100 80GB per host with seed 0, prefix caching off, and offline weights. Agent and monitor contexts are 32,768 and 8,192 tokens (55% and 30% GPU memory). The exploratory log, the exploratory live gates, the stronger-agent run, both airline runs, and the two-gate run served the agent with default kernels. The other runs of Table D.1 used batch-invariant kernels (VLLM_BATCH_INVARIANT=1), except the model-update reruns, whose serving varies by rung. Each H100 host ran 32 episodes at a time. The model-update reruns replayed logged decisions on one NVIDIA GH200 120GB per job (85% GPU memory), with 32 requests in flight under batch-invariant kernels and one under default kernels. Change Status Harm (interval type) Rests on To settle 1 Stopping gate, θ=0.94θ=0.94 Identified; implementation check P(harm): replay 0.039, live 0.030, equiv. within 0.03 (Newcombe 90%). (R), (A1), (A2); (A3) declared, harm untested Test (A3) for harm 1 Stopping gate, replications Identified; implementation check Equiv. within 0.03 (Newcombe paired 90%): stronger agent [−0.021,0.009][-0.021,0.009]; airline [−0.020,0.018][-0.020,0.018]. (R), (A1), (A2); outputs vary across runs; (A3) declared Test (A3) for harm; margin vs effect 1 Two retry gates, one log Identified by targeted execution P(harm): log [0.244,0.345][0.244,0.345] and [0.100,0.451][0.100,0.451]; log + 1,032 and 2,929 snapshot continuations: 0.279 and 0.158; live 0.288 and 0.165, equiv. within 0.015 (Newcombe paired 90% [0.003,0.014][0.003,0.014] and [0.001,0.013][0.001,0.013]); pass-all and retry-as-stop outside the margin. Cost: 0.08 and 0.23 of live agent calls, given the log (partial). (R), (A1), (A2); snapshot (T): 3,961 of 3,961 continuations valid Check (T) beyond file tree 1 Retry gate, bash agent Identified by targeted execution P(harm): log [0.023,0.422][0.023,0.422] (plug-in outer bounds); log + 485 snapshot continuations: 0.029 (exact 95% [0.020,0.040][0.020,0.040]); live 0.030, equiv. within 0.02 (Newcombe paired 90% [−0.002,0.004][-0.002,0.004]). Cost: 0.30 of live agent calls, given the log (partial). (R), (A1), (A2); snapshot (T): 485 of 485 restoration checks passed Check (T) beyond file tree 2 Log without per-step harm Set; identified with per-step harm Certified P(harm) without per-step harm: held-out 0.159, replication 0.111; with it: 0.064, 0.051 (exact one-sided 95%) As stopping gate Log harm timing 3 Both gates, 40-step cap Stop identified; retry bounded P(harm): stopping 0.043 for horizons k≥15k≥ 15 (unknowns harmful: 0.067); retry [0.043,0.473][0.043,0.473] (plug-in outer bounds), agreement 0.77 (k=1k=1) to 0.57 (k=40k=40) As both gates; 17 unknown outcomes (disk incident) Execute retry continuations 4 Model release Agreement only, pooled Agreement 0/99, share-weighted over six server processes (exact two-sided 95% upper end 0.037, conservative); losses unestimated Seed-addressable access per process Support or new runs 5 Two-agent relay Identified from snapshots Second-agent P(harm): relay 0.115; snapshot equiv. within 0.03 (Newcombe paired 90% [−0.010,0.004][-0.010,0.004]); clean 0.178 (relay minus clean, Newcombe paired 95% [−0.078,−0.049][-0.078,-0.049]). Both violate: 0.085; rate product 0.0195. Snapshot (T): start digests 1,599 of 1,599 Clean starts: workspace in S 6 Announced gate Replay inapplicable Abort +0.070+0.070 over the live unannounced gate (Newcombe paired 95% [0.019,0.120][0.019,0.120]); P(harm): 10/400 live (A2) fails for this prompt Live runs Table D.2: Table 2 in full: what the deployer can state before each change ships, and what would settle the rest. Honest agents; in the bash setting, failure is near saturation and θ was chosen on an exploratory log; the stronger-agent and airline thresholds were chosen on pilots. Mint: identified, by the first two terms of display (2) or by targeted execution under (T). Gray: needs support or bounds, or replay does not apply. Coral: evidence that would settle the rest (last column). Newcombe: difference-of-proportions score interval; exact: Clopper-Pearson; plug-in: without sampling uncertainty; equiv.: equivalent. Failure, task success, and cost: Appendix D. D.3 1 Approval Gates: Stopping and Retry Gates This subsection gives the stopping and retry results of Section 4.1. Figure D.1: Targeted execution and snapshot starts match within registered margins; the unannounced gate stays compatible. A thick 90% Newcombe bar inside the gray band is a match (with registered cluster checks). Otherwise a thin 95% whisker decides: excluding zero is a failure, and containing zero is compatible (unknown outcomes: midpoints and envelopes). Figure D.2: The log alone leaves each gate’s P(harm) on both sides of the ceiling; executed continuations settle it and match live runs (bars: exact 95%). Gray: point estimates from retry as stop to the log-only upper bound; diamond: post hoc skip-blocked reading. Figure D.3: Implementation checks: stopping-gate replay matches live harm in all three settings. The two “Stopping gate” rows use unpaired Newcombe intervals. Intervals, midpoint dots, and verdicts follow Figure D.1; the airline check also requires its task-cluster interval to fit the margin. Stopping gate (Section 4.1). Replay from the 1,000 episodes of the replication log predicts P(harm) 0.039, and the 1,000 live replication runs yield 0.030 (Figure D.3). The difference, −0.009-0.009 (Newcombe 95% [−0.025,0.007][-0.025,0.007]), falls within the registered equivalence margin of ±0.03± 0.03 (Newcombe 90% [−0.023,0.005][-0.023,0.005]). Sensitivity to the abort valuation (A3). On the replication log, 372 of 1,000 episodes stopped before harm, so if a stopped episode later caused harm with probability p, replayed P(harm) would be 0.039+0.372p0.039+0.372p, below an illustrative 0.10 harm target only if p<0.16p<0.16; (A3) is declared and untested for harm. Stopping gate with a stronger agent. The stronger-agent run tests Qwen3.5-27B-FP8 (up to 15 steps) on default kernels, so replay predicts the live gate in distribution. The gate reads the log-scale doubt s=−log10(1−E[N]/100)s=- _10(1-E[N]/100) from the monitor’s next-token distribution. On a pilot, threshold λ=11.551λ=11.551 was chosen where the stop rate fell between 10% and 15%; the registered run used 1,400 task-and-seed pairs. Live P(harm) is 0.224 to 0.226 against 0.230 to 0.233 for replay. Live minus replay is −0.009-0.009 to −0.004-0.004 (Newcombe paired 95% [−0.024,0.011][-0.024,0.011]; 90% [−0.021,0.009][-0.021,0.009]), equivalent within the registered margin of ±0.03± 0.03. With per-step harm, the log certifies P(harm) at most 0.253 (exact one-sided 95%, rounded outward); without it, the identified set is [0.189,0.331][0.189,0.331] and certifies only 0.353. Seven episodes across five pairs had unknown outcomes from a host disk incident (three unscored, four failed state checks); all seven remain in every denominator as ranges. Stopping gate in a second environment. The airline run uses τ2τ^2-bench v1.0.1 (Barres et al., 2025), where an agent modifies a customer booking database under written rules for cancellations, changes, fees, and compensation. A frozen deterministic checker flags policy violations. The agent (Qwen3-14B-FP8) and simulator run on default kernels. Threshold λ=11.186λ=11.186 was chosen on a pilot (stop rate 0.130), and the registered evaluation used 1,200 units across 50 tasks (24 seeds each). Live P(harm) is 554/1,200 = 0.4617 against 555/1,200 = 0.4625 for replay. Live minus replay is −0.001-0.001 (Newcombe paired 90% [−0.020,0.018][-0.020,0.018]; task-cluster bootstrap 90% [−0.023,0.020][-0.023,0.020]); both intervals satisfy the registered ±0.03± 0.03 margin. Pass-all P(harm) is 0.512; the gate removes 0.049 of harm in replay and 0.050 live, so the 0.03 margin is loose relative to this 0.05 effect. Because the database state is a deterministic function of executed tool calls, rerunning the checker on logged calls recovered harm timing in 1,200 of 1,200 episodes, certifying P(harm) at most 0.487 (without timing: 0.511). Retry gate by targeted execution (Section 4.1). Each of 1,200 units (a task and seed) runs three conditions on one host: a pass-all baseline committing a container snapshot prior to the first step scoring above θ=0.94θ=0.94; a continuation from that snapshot with context rebuilt from logged messages, the proposal refused, and the live retry gate active; and the live retry gate from a clean sandbox. The retry gate agrees with 715 logged episodes and first blocks 485 (317 at step 0). From the log alone, display (5) bounds P(harm) within [0.023,0.422][0.023,0.422] (plug-in outer bounds). Executing the 485 continuations yields P(harm) of 35/1,200 = 0.029 (exact 95% [0.020,0.040][0.020,0.040]), with no unknown outcomes; this prediction was frozen with its hash recorded before reading live records. The live gate gives 36/1,200 = 0.030 ([0.021,0.041][0.021,0.041]). Paired by unit, both arms are harmful in 35 units, the live arm alone in 1, and neither in 1,164. Live minus identified is 0.001 (Newcombe paired 95% [−0.003,0.005][-0.003,0.005]; 90% [−0.002,0.004][-0.002,0.004]), well within the registered ±0.02± 0.02 margin. Equivalence applies to marginal P(harm) over the task distribution; it does not establish that pathwise trajectories or task-level rates agree, as agreement and continuation errors could offset. Every restoration matched its source file-tree digest and passed context checks; no snapshot held outside processes. An independent recomputation from raw logs reproduced all values. Execution cost. The continuations required 4,004 agent calls and 26.1 million tokens, compared to 13,489 calls and 83.7 million tokens for the live gate: cost ratios of 0.30 and 0.31. These are partial-cost ratios that assume the pass-all log exists (14,460 agent calls). Two retry gates from one log: protocol (Section 4.1; registered). The two-gate run (E7) logs the stronger agent (Qwen3.5-27B-FP8 on default kernels) under pass-all across 7,200 task-and-seed units on six hosts. A gate-free snapshot rule committed the container before every step whose monitor doubt score s exceeded 1.0, yielding 16,456 committed snapshots (mean 61 MB per episode and 3.1 seconds per commit). Two retry gates block at λ1=11.551 _1=11.551 and λ2=10.25 _2=10.25 on s with two retries permitted. For each gate, the log resolves agreeing units (6,168 and 4,271), while continuations from first-block snapshots were executed live (1,032 and 2,929, about 14% and 41% of the log; all 3,961 valid). Predictions were frozen, with their hash recorded, before reading live records, and an independent recomputation verified all identified rows, intervals, and decisions. For Gate 2, the evaluation follows Section 3. The deployer declares the gate, stop value, and decision rule. Replay finds 4,271 agreeing episodes and 2,929 first blocks (41%). Of these, 92 fall at the last step, where no agent step remains, so their recorded outcome is final (69 harmless, 23 harmed before the block); the other 2,837 continue. The log reads 387 harmed agreeing episodes, and executing the continuations yields 730 more. Display (2) gives (387+23+730)/7,200≈0.158(387+23+730)/7,200≈ 0.158 (with the one unknown outcome, the midpoint is 0.1584). Joint 95% bounds put harm at most 0.1672 and success at least 0.3871, approving the gate. E7 primary results. For Gate 1, identified P(harm) is 0.2794 against live 2,072/7,200=0.28782,072/7,200=0.2878 (one unknown outcome), a difference of 0.008 (Newcombe paired 90% [0.003,0.014][0.003,0.014]; task-cluster 90% [0.002,0.015][0.002,0.015]), equivalent within the registered 0.015 margin. For Gate 2, identified P(harm) is 0.1584 against live 0.1652 (one unknown each), a difference of 0.007 (paired 90% [0.001,0.013][0.001,0.013]; task-cluster [0.000,0.013][0.000,0.013]), also equivalent within 0.015. Across all four targeted-execution comparisons, live harm exceeds identified harm by 0.001 to 0.008, all within registered margins. Log-only outer bounds are [0.244,0.345][0.244,0.345] and [0.100,0.451][0.100,0.451], corrected for the unknown outcome. Both ends are attainable: an agent that halts after a refusal gives the lower end, and one that violates the policy whenever a refusal leaves it a step gives the upper end. The log contains no refusal and rules out neither, so it cannot decide either gate. E7 reference predictors. Both registered reference predictors fail the 0.015 margin on both gates. Ignoring the gate (pass-all, 0.3445) misses live harm by −0.057-0.057 and −0.179-0.179. Counting each retry as a stop (0.2445 and 0.1002) misses by +0.043+0.043 and +0.065+0.065 (Newcombe paired 95% [0.036,0.051][0.036,0.051] and [0.058,0.072][0.058,0.072]). A third reading, fixed in a note before computation (post hoc), drops blocked calls while retaining the remaining logged episode and yields 0.3108 and 0.1904 (discrepancies −0.023-0.023, 95% [−0.030,−0.016][-0.030,-0.016], and −0.025-0.025, [−0.033,−0.018][-0.033,-0.018]), also outside the margin; under the declared rule, it would select gate 2 with harm at most 0.1984. The registered reference errors round to 0.04 to 0.18, as reported in Section 4.1. E7 decision and execution cost. The declared decision rule (P(harm) at most 0.25 and task success at least 0.37, exact one-sided 95% bounds, unknowns unfavorable) selects Gate 2 in both arms: identified harm at most 0.1658 and success at least 0.3889; live harm at most 0.1727 and success at least 0.3897 (also passing with 97.5% per bound, for joint 95% coverage: 0.1672 and 0.3871). Neither registered reference certifies any candidate (post hoc): pass-all violates the harm ceiling, and retry-as-stop violates the harm ceiling for gate 1 and the success floor for gate 2. Continuations used 0.08 and 0.23 of live agent calls (8% and 23%; partial-cost records); including the pass-all log’s 102,779 calls, the ratio is 0.66. With the log already recorded, the continuations’ 31,706 calls are 15% of the 204,875 of both live gates. Random live subsets of that expected cost (1,114 units per gate) reached both live decisions in 56.4% of 500 draws; the smallest common size on a 1% grid reaching both in at least 90% was 2,232 units per gate (31% of the cohort; 91.8%), at 2.0 times the continuations’ calls and 0.47 times those of log plus continuations (post hoc; per-bound 95%). Simpler readings at face value (post hoc). Read as point values without coverage at the declared ceiling and floor, counting retries as stops approves gate 1, which live runs refuse, and refuses gate 2, whose success it puts at 0.334; ignoring the gate also refuses gate 2. E7 snapshot design. Minimal first-deviation snapshots at open running maxima after step 0 require 6,332 of the 16,456 snapshots and 173 of 441 GB for harm alone (Proposition F.10.1, post hoc). A running maximum at the last step is not open because no agent step remains. Retry gate in the airline environment. The registered airline run (E5) restores each continuation by replaying logged database writes without container snapshots. The pass-all log plus 159 valid executed continuations identify P(harm) of 597/1,200 = 0.4975; the paired live retry gate gives 598/1,200 = 0.4983. Both 90% equivalence intervals (Newcombe paired [−0.019,0.020][-0.019,0.020]; task-cluster bootstrap [−0.017,0.019][-0.017,0.019]) lie inside ±0.03± 0.03. The prediction was frozen before the 800 new live records were read; units 0 to 399 reuse the airline run’s live retry episodes, already analyzed there. Counting retries as stops gives the lower bound 0.4625 (0.036 below live). Continuations used 0.090 of live agent calls and 0.131 of declared tokens (complete usage). Retry gate on the held-out log. In the earlier held-out protocol, later-prefix restoration checks passed 0 of 10 trials, so those continuations stayed bounded; step-0 runs needed only fresh starts (bounds and live check: companion file). D.4 2 Partial Records: Certification For the logging comparison in Section 4.2, exact one-sided 95% Clopper–Pearson bounds on replayed P(harm) certify a harm level with reduced logs in this setting. On the replication log (no unknown outcomes), full and reduced logs certify 0.051 (39/1,000 harms) against 0.111 without per-step harm (94/1,000). On the held-out log, counting one failed state check as harmful yields 0.064 for full and reduced logs (12/300) against 0.159 without per-step harm (37/300). The reduced log preserves per-step scores, per-step harm and cost, and final outcomes. Field Needed for Droppable when Evidence Monitor scores Deviation Monitor reruns deterministically Held-out: 3,589 of 3,589 recomputed Per-step harm Stop valuation Calls and a deterministic checker fix timing Certified ceiling with vs. without it: held-out 0.064 vs. 0.159, replication 0.051 vs. 0.111; airline: 1,200 of 1,200 recomputed Per-step cost Pre-stop cost Another field fixes it Mean tokens, exploratory gates (companion) Inputs, seeds, serving mode Agent rerun Change reads logged fields only 1,650 of 1,650 decisions; other kernel mode: 2 of 99 episodes Gate decisions Nothing Always (Remark E.5.1) Unused Table D.3: What a stopping-gate replay needs from the log here: per-step harm (shaded) is the one field whose removal raised the certified harm ceiling. An instance of Proposition 3.1; no general field list. Certification: exact one-sided 95% bounds on replayed P(harm). D.5 3 Long Horizons For the horizon comparison in Section 4.3, truncating a 600-episode pass-all log with a 40-step cap under batch-invariant serving yields horizon curves with all 600 planned episodes in every denominator (the companion file holds the per-horizon table). Beyond k=25k=25, more than 5% of runs have already ended on token or context limits (151 by k=40k=40, while 240 reach the 40-step cap). Stopping-gate replayed P(harm) stabilizes at 26/600 = 0.043 for k≥15k≥ 15 (0.067 if all unknowns were harmful). Retry-gate agreement mass falls from 0.77 at k=1k=1 to 0.57 at k=40k=40, widening plug-in outer bounds from [0.018,0.030][0.018,0.030] to [0.043,0.473][0.043,0.473]. A host disk incident caused 17 unknown outcomes (6 unscored, 11 failed state checks), which generate all reported ranges; no episode was excluded. D.6 4 Model Releases In the model-release test of Section 4.4, the release candidate (Qwen3.5-27B-FP8) reproduces none of 99 logged episodes across six server processes at identical inputs and seeds, while the identical model reproduces 99 of 99 and kernel and precision changes reproduce 2 and 1. Outputs were seed-addressable within each process (40 of 40 probe inputs reproduced) but varied across processes (14 of 40 differed). Episodes were assigned to processes independently of content, so the bound targets the mean agreement mass over processes, weighted by their shares; the exact two-sided 95% Clopper–Pearson bound for 0/99 (0.037) is conservative for it, by independence across episodes and concavity of log(1−p) (1-p). D.7 5 Shared State: Two Agents in Relay In the registered five-condition design of Section 4.5, a first agent works a task up to 7 steps, and a second agent continues for up to 8 steps in the inherited workspace. Across 1,600 units (8,000 planned runs, 7,998 scored; two snapshot starts failed to commit and count as unknown), the second agent violated policy in 184 of 1,600 relays (0.115, exact 95% [0.100,0.132][0.100,0.132]). From a clean start on the same task and seed, it violated in 285 of 1,600 (0.178, [0.160,0.198][0.160,0.198]). Relay minus clean start is −0.063-0.063 (Newcombe paired 95% [−0.078,−0.049][-0.078,-0.049]; 90% [−0.075,−0.051][-0.075,-0.051]), failing equivalence within the registered ±0.03± 0.03 margin. Started from a snapshot of the first agent’s standalone end state, violations occurred in 0.1175 to 0.1188 of runs; relay minus snapshot start is −0.004-0.004 to −0.003-0.003 (paired 90% [−0.010,0.004][-0.010,0.004]), equivalent within ±0.03± 0.03. Here clean starts substantially overstate relay harm. Both agents violated in 136 of 1,600 relays (β=0.085β=0.085, exact 95% [0.072,0.100][0.072,0.100]), against marginal rates p1=0.169p_1=0.169 and p2=0.115p_2=0.115 whose product is 0.0195. The difference β−p1p2=0.066β-p_1p_2=0.066 shows strong positive dependence; treating the agents as independent overstates the union harm probability π=p1+p2−βπ=p_1+p_2-β by 0.066. Per-agent logs without shared state give the Proposition G.1.1(i) range [0,0.115][0,0.115] for β; conditioning on the task risk class C narrows it to [0.031,0.115][0.031,0.115], and adding external write flags D gives [0.041,0.115][0.041,0.115]. Linking snapshot runs by unit yields 0.084 to 0.085, matching relay within ±0.03± 0.03. At initialization, file-tree digests matched their sources in 1,599 of 1,599 runs per snapshot condition. D.8 6 Oversight Cues In the paired design of Section 4.6 over 400 triplets (pass-all, unannounced stopping gate, announced stopping gate), the announced gate aborted 0.070 more often than the unannounced gate (181/400 versus 153/400; Newcombe paired 95% [0.019,0.120][0.019,0.120]; 90% [0.027,0.112][0.027,0.112], excluding equivalence within ±0.03± 0.03). Replay from unannounced logs understates the announced abort rate by 0.0725 (Newcombe paired 95% [0.022,0.122][0.022,0.122]), while the unannounced gate stays compatible with replay (negative control). Harm is 10/400 in all three arms. This intervention alters the live abort rate, rejecting the abort-rate invariance of (A2) for this prompt; it does not isolate semantic anticipation from other prompt perturbations. Appendix E Replay, Logging Sufficiency, and Long Horizons For Sections 3.1 to 3.3, this appendix proves Propositions A.4.1, E.1.1, and 3.1, Lemma E.4.2, and Corollaries E.6.1 and E.7.1 in the finite setting. E.1 Continuing Deviations: Statement Proposition A.4.1 gives the agreement and stopping components of display (2) in Section 3; this subsection bounds the continuing component. For a scalar query X=ϕ(L)X=φ(L) and continuing replayed prefix h, let hX_h denote the values of X on paths extending h that follow fκf^κ at later decisions. Condition (S) formalizes saturated continuation, with primitive conditions in Lemma E.4.2. (S) Saturated continuation: distinct continuing replayed prefixes of positive baseline mass reach distinct inputs of unknown kernels, each of baseline probability zero. For every family (Qh)(Q_h) with Qh∈Δ(h)Q_h∈ (X_h), one admissible mechanism with the same baseline law realizes all QhQ_h at once. A replacement that sends two or more continuing prefixes of positive baseline mass to one common state violates (S). Proposition E.1.1 (Continuing deviations; Manski, 2003). Assume (R), (A1), and (A2), and let B⊆B . Suppose every coordinate of Ω is recorded, so the evidence is P0P^0. Let ν be the subprobability from (i) and (i) of Proposition A.4.1 pushed to X. Under (A3) and (S), the identified set of laws of X is ν+∫QhP0(h,continuing∣r):Qh∈Δ(h)\ν+ Q_h\,P^0(dh,continuing r):Q_h∈ (X_h)\. Every law-invariant functional nondecreasing in first-order stochastic dominance (mean, exceedance probability, VaR, CVaR) attains its minimum and maximum over this set when each continuing prefix places its mass at minh _h or at maxh _h, respectively. For the mean, exceedance probability, and CVaR, every value between the extremes is attained; VaR takes values in a finite set. Without (S), these are outer bounds. Let ν−ν^- and ν+ν^+ be the laws of X given r that keep agreement and stop values and assign each continuing prefix its least and greatest feasible value, respectively. Every such functional ρ then satisfies ρ(ν−)≤qtκ(r)≤ρ(ν+),ρ(ν^-)≤ q^κ_t(r)≤ρ(ν^+), (5) with the inequalities holding without (S). Section E.4 contains the proof. E.2 Finite Setting This setting is used in the replay, logging, and horizon proofs for Sections 3.1 to 3.3. Paths, Histories, and Kernels. Let Ω be a finite set of complete paths ω=(v1,…,vn(ω))ω=(v_1,…,v_n(ω)) listing execution, observation, and post-abort coordinates in declared generation order, with no path a proper prefix of another. Histories ℋH are proper prefixes, including the empty history. Declared order assigns to each h∈ℋh a kernel name nm(h)∈nm(h) and a declared input π(h)π(h). The tree is full: (h,v)∈ℋ∪Ω(h,v) ∪ for every kernel value v. A mechanism M assigns transition kernels knM(⋅∣i)k^M_n(· i). For ω1:j=(v1,…,vj) _1:j=(v_1,…,v_j), with ω1:0 _1:0 empty, the path law is PM(ω)=∏j=0n(ω)−1knm(ω1:j)M(vj+1∣π(ω1:j)).P_M(ω)= _j=0^n(ω)-1k^M_nm( _1:j) (v_j+1 π( _1:j) ). (6) The cylinder [h][h] collects paths extending h. Summing over extensions of h gives PM([h])=∏j=0|h|−1knm(h1:j)M(hj+1∣π(h1:j)).P_M([h])= _j=0^|h|-1k^M_nm(h_1:j) (h_j+1 π(h_1:j) ). (7) Loss is L=ℓ(ω)∈⊂ℝmL= (ω) ^m. Observation kernels are named kernels, so records RtR_t are path coordinates, realizing PE,KP_E,K of Appendix A.1 in the finite setting. Replaced Kernel. The replaced decision kernel is named k∈k . A history h with nm(h)=knm(h)=k is a decision history with input I(h)=π(h)I(h)=π(h) and step t(h)∈0,…,Tt(h)∈\0,…,T\. The refined clock of Appendix A.1 invokes k at most once per step. Under (R), known maps define the baseline kernel δf0(i) _f^0(i) and replacement kernel δfκ(i) _f^κ(i). The input is a function of history contained in the full record, distinguishing full histories from declared inputs. Baseline laws are supported on Ω0 ^0, where decision coordinates match f0f^0. A value a is an abort if no extension of (h,a)(h,a) has nm(h′)=knm(h )=k, terminating calls to the replaced kernel. First Deviation. A decision history h is a deviation history if fκ(I(h))≠f0(I(h))f^κ(I(h))≠ f^0(I(h)) while fκ(I(h′))=f0(I(h′))f^κ(I(h ))=f^0(I(h )) on all proper decision prefixes h′h . The set κD_κ of deviation histories has pairwise disjoint cylinders. For ω∈[h]ω∈[h] with h∈κh _κ, set σκ(ω)=t(h) _κ(ω)=t(h) and replayed prefix h+=(h,fκ(I(h)))h^+=(h,f^κ(I(h))); set σκ=∞ _κ=∞ on agreement set κ A_κ. Paths partition into agreement and disjoint deviation cylinders: Ω=κ⊔⨆h∈κ[h]. = A_κ _h _κ[h]. (8) Deviations partition into terminal set κtermD^term_κ (abort outputs) and continuing set κcontD^cont_κ. Conditioning Record. A record value r is pre-intervention if Ωr=R=r _r=\R=r\ is a disjoint union of cylinders [h][h] over ℋrH_r, none having a deviation history as a proper prefix. Records RtR_t with t<st<s satisfy this property. We assume P0(Ωr)>0P^0( _r)>0 and write P(⋅∣r)=P(⋅∩Ωr)/P(Ωr)P(· r)=P(·∩ _r)/P( _r). Let κ(r)=h∈κ:[h]⊆ΩrD_κ(r)=\h _κ:[h] _r\, with κterm(r)D^term_κ(r) and κcont(r)D^cont_κ(r) defined analogously. Assumptions. Let P0=PM0P^0=P_M^0 and Pκ=PMκP^κ=P_M^κ. The assumptions of Appendices A.2 and A.4 take tree form: (R) Replay interface: the replaced decision kernel is δf0(i) _f^0(i) under M0M^0 and δfκ(i) _f^κ(i) under MκM^κ, with both maps known and the input contained in the full record (a coarser log, as in Proposition 3.1, need not contain it). (A1) Invariance: knMκ=knM0k^M^κ_n=k^M^0_n for every name n≠kn≠ k, including the kernel at the empty history (the initial law) and every random-input kernel. (A2) Prefix preservation (no anticipation): both mechanisms use the same declared order and inputs (nm,π)(nm,π), and no declared input or unreplaced kernel depends on the identity or specification of the installed replacement. (A3) Declared abort valuation: for every h∈κtermh ^term_κ with P0([h])>0P^0([h])>0, Pκ(L∈⋅∣[h])=bκ(⋅∣h+)P^κ(L∈· [h])=b_κ(· h^+), a declared probability measure on L. Because no replaced kernel acts after an abort, (A1) ensures that post-abort distributions depend only on h+h^+, shared by replacements that abort at the same replayed prefix. E.3 Prefix Lemma and Proof of Proposition A.4.1 Lemma E.3.1 (Prefix Lemma). Assume (R), (A1), and (A2). (a) Pκ(ω)=P0(ω)P^κ(ω)=P^0(ω) for every ω∈κω∈ A_κ. (b) Pκ([h])=P0([h])P^κ([h])=P^0([h]) for every history h none of whose proper prefixes is a deviation history. In particular this holds for every h∈κh _κ and every h∈ℋrh _r, and Pκ(Ωr)=P0(Ωr)P^κ( _r)=P^0( _r). Proof. By (R), (A1), and (A2), corresponding factors in (6) and (7) agree until the first deviation, proving (a) and (b). Summing over the disjoint record cylinders gives equality on Ωr _r. ∎ Proof of Proposition A.4.1(i). Immediate from Lemma E.3.1(a),(b), summing over agreement paths and conditioning on r. ∎ Proof of Proposition A.4.1(i). Immediate from Lemma E.3.1(b) and (A3), summing over the disjoint terminal cylinders and conditioning on r. ∎ E.4 Saturated Continuation and Proof of Proposition E.1.1 Fix a finite query ϕ:→φ:L , with ⊂ℝX for order statements. For h∈κh _κ, let Ωκ(h+) ^κ(h^+) collect replacement-consistent extensions that follow fκf^κ at all decisions after h+h^+, giving feasible set h=ϕ(ℓ(ω)):ω∈Ωκ(h+)X_h=\φ( (ω)):ω∈ ^κ(h^+)\. The model class ℳM is a family of mechanisms that share the tree, ℓ , f0f^0, fκf^κ, and bκb_κ, and satisfy (R) and (A1) to (A3). Let ℳ(P)M(P) be members with baseline law P, with identified set Θϕ(P)=ϕ#PMκ(L∈⋅∣r):M∈ℳ(P) _φ(P)=\ _\#P^κ_M(L∈· r):M (P)\. Definition E.4.1 (Saturated Continuation). Let κcont(r,P)D^cont_κ(r,P) be the set of h∈κcont(r)h ^cont_κ(r) with P([h])>0P([h])>0. The class ℳM is saturated at P for ϕφ if, for every family (Qh)(Q_h) with Qh∈Δ(h)Q_h∈ (X_h) for h∈κcont(r,P)h ^cont_κ(r,P), some M∈ℳ(P)M (P) satisfies ϕ#PMκ(L∈⋅∣[h])=Qh _\#P^κ_M(L∈· [h])=Q_h for every such h. Let P be the set of laws P on Ω0 ^0 with P(Ωr)>0P( _r)>0. Lemma E.4.2 (Unrestricted Class). Let ℳfullM_full be the class of mechanisms on the declared tree that satisfy (R) and (A1) to (A3) and in which every unreplaced kernel reads the full history, π(h)=hπ(h)=h whenever nm(h)≠knm(h)≠ k. Suppose that for every h∈κtermh ^term_κ the declared bκ(⋅∣h+)b_κ(· h^+) is the law of ℓ under some probability on the replacement-consistent extensions of h+h^+. Then for every P∈P , every ϕφ, and every family (Qh)(Q_h) with Qh∈Δ(h)Q_h∈ (X_h) for h∈κcont(r,P)h ^cont_κ(r,P), some M∈ℳfullM _full has baseline law P and satisfies ϕ#PMκ(L∈⋅∣[h])=Qh _\#P^κ_M(L∈· [h])=Q_h for every such h. In particular, every law in P is the baseline law of a member, and ℳfullM_full is saturated at every P∈P . Proof sketch. For each continuing prefix h, mix replacement-consistent paths achieving each outcome in hX_h with weights QhQ_h; at terminal prefixes, use extensions realizing bκb_κ. Set unreplaced kernels to the conditional transitions of P on its support and of these mixtures inside each [h+][h^+]. Full-history inputs allow these assignments independently: the replayed cylinders are disjoint and baseline-null, since each contains a first output differing from f0f^0. Complete unused inputs arbitrarily. The product path law then recovers P and realizes all target continuation laws and terminal valuations simultaneously. ∎ Assumption (S) is Definition E.4.1 at P0P^0 with distinct continuing prefixes reaching distinct unreached inputs; under realizable bκb_κ, ℳfullM_full is saturated at every P∈P . Proposition E.4.3 (Identified Set). Assume (R) and (A1) to (A3), and let P be a baseline law with P(Ωr)>0P( _r)>0. Write wh=P([h]∣r)w_h=P([h] r) for h∈κcont(r,P)h ^cont_κ(r,P), and let ν= ν= ϕ#(P(L∈⋅,κ∣r) _\# (P(L∈·, A_κ r) +∑h∈κterm(r)P([h]∣r)bκ(⋅∣h+)). + _h ^term_κ(r)P([h] r)\,b_κ(· h^+) ). Then Θϕ(P) _φ(P) is contained in ϕ(P)=ν+∑hwhQh:Qh∈Δ(h)S_φ(P)= \ν+ _hw_hQ_h:Q_h∈ (X_h) \, with equality if ℳM is saturated at P. Proof. Summing over (8), Proposition A.4.1(i),(i) fixes ν, while Lemma E.3.1(b) fixes each continuing weight whw_h. By (R), each continuation law lies in Δ(h) (X_h), giving the inclusion; saturation gives equality by Definition E.4.1. ∎ Order Bounds. For finitely supported laws η,η′η,η on ℝR, write η≤stη′η _stη if Fη(x)=η((−∞,x])≥Fη′(x)F_η(x)=η((-∞,x])≥ F_η (x) for all x (Shaked and Shanthikumar, 2007). Let η−=ν+∑hwhδminhη^-=ν+ _hw_h _ _h and η+=ν+∑hwhδmaxhη^+=ν+ _hw_h _ _h. Proposition E.4.4 (Order Bounds). Under the hypotheses of Proposition E.4.3, with ⊂ℝX , the following hold. (a) η−,η+∈ϕ(P)η^-,η^+ _φ(P), and η−≤stη≤stη+η^- _stη _stη^+ for every η∈ϕ(P)η _φ(P). (b) If ρ is law invariant and nondecreasing in ≤st _st, then ρ(ϕ(P))⊆[ρ(η−),ρ(η+)]ρ(S_φ(P)) [ρ(η^-),ρ(η^+)] and both endpoints are attained; for nonincreasing ρ the endpoints swap. The mean, the exceedance probability η((,,,))η((x,∞)), the CDF value Fη(x)F_η(x), which is nonincreasing, VaRβ(η)=minx:Fη(x)≥βVaR_β(η)= \x:F_η(x)≥β\, and CVaRβCVaR_β for β∈(0,1)β∈(0,1) are such functionals. (c) For the mean, the exceedance probability, the CDF value, and CVaRβCVaR_β, every value between the two endpoints is attained. Proof sketch. Point masses at feasible endpoints bound each continuation CDF, proving (a); CDF and quantile ordering give (b) (Shaked and Shanthikumar, 2007, Eqs. (1.A.2), (1.A.7)). For (c), mix η−η^- and η+η^+ within ϕ(P)S_φ(P). Means and event probabilities are affine; finite support makes the CVaR formula (Rockafellar and Uryasev, 2002, author’s version, Theorem 10, Eqs. (27)–(28)) a finite minimum of affine functions and also gives its monotonicity in (b). Continuity and the intermediate value theorem finish. ∎ Proof of Proposition E.1.1. Combine Propositions E.4.3 and E.4.4, using full recording and (S) for equality; VaR takes values in the finite feasible set. ∎ E.5 Logging Characterization and Proof of Proposition 3.1 Scope of the Necessity Direction. Necessity in Proposition 3.1 requires variation across all baseline laws on Ω0 ^0 via point-mass witnesses. In restricted classes where coordinates have fixed laws, necessity can fail, whereas sufficiency holds for every baseline class. Proof. In the tree setting, the contribution CκC_κ of Proposition 3.1 is δℓ(ω) _ (ω) on κ A_κ, bκ(⋅∣h+)b_κ(· h^+) on [h][h] for terminal h, and 00 on [h][h] for continuing h; rP_r is the set P above, sκ=sκ,rs_κ=s_κ,r, and Ωr0=Ω0∩Ωr ^0_r= ^0∩ _r. For a baseline law, sκ(P)=(νκ,εκ)s_κ(P)=( _κ, _κ), where νκ _κ is the measure ν of Proposition E.4.3 with ϕφ the identity and εκ=∑hwh _κ= _hw_h. A logging map is a function g on Ω , and it determines the record event when Ωr=g−1(Yr) _r=g^-1(Y_r) for a set YrY_r of log values. Proof of Proposition 3.1. Fix κ and assume Ωr=g−1(Yr) _r=g^-1(Y_r). For sufficiency, fibre constancy makes (Cκ,uκ)(C_κ,u_κ) a function of g on Ωr0 ^0_r, so its conditional expectation is determined by g#Pg_\#P. For necessity, suppose ω,ω′∈Ωr0ω,ω ∈ ^0_r satisfy g(ω)=g(ω′)g(ω)=g(ω ) and (Cκ,uκ)(ω)≠(Cκ,uκ)(ω′)(C_κ,u_κ)(ω)≠(C_κ,u_κ)(ω ). The point masses δω _ω and δω′ _ω belong to P and have the same log law. Their summaries are (Cκ,uκ)(ω)(C_κ,u_κ)(ω) and (Cκ,uκ)(ω′)(C_κ,u_κ)(ω ), which differ, so no function of g#Pg_\#P equals sκ(P)s_κ(P) on P. Applying both directions to each κ in the family proves the equivalence. ∎ Remark E.5.1 (Status Need Not Be Logged). A coarsened log need not record deviation status when its fibres pool paths with equal signatures (check T1-4, checks/verify_replay.py). Condition (R) refers to the full record, which contains the gate input; the log need not. E.6 Coarse Evidence and Garbling This corollary supports the coarse-log claim of Section 3.2. Corollary E.6.1 (Garbling). For a fixed model class, replacement, and query conditioned on one record event measurable from g′g , if g′=G∘g =G g for some map G, the identified set under g is contained in the set under g′g . Proof sketch. Immediate from nesting the compatible model classes under g and G∘gG g (Blackwell, 1951; Blackwell, 1953). ∎ E.7 Long Horizons This proves the horizon claims of Section 3.3. Corollary E.7.1 (Long horizons). Assume (R), (A1), and (A2). For j=0,…,Tj=0,…,T let ηj(r)=P0(σκ=j∣σκ≥j,Rt=r) _j(r)=P^0( _κ=j _κ≥ j,\ R_t=r), set to 00 when P0(σκ≥j∣r)=0P^0( _κ≥ j r)=0; by Lemma E.3.1(b) the same value holds under PκP^κ. Fix η∈[0,1]η∈[0,1]. (i) The agreement mass Pκ(κ∣r)=∏j=0T(1−ηj(r))P^κ( A_κ r)= _j=0^T(1- _j(r)) is identified from the full record; if ηj(r)≥η _j(r)≥η at k steps, it is at most (1−η)k(1-η)^k. (i) If every deviation is terminal, (A3) holds, and a logging map g that determines the event Rt=r\R_t=r\, as in Proposition 3.1, determines the contribution CκC_κ on Ω0∩Rt=r ^0∩\R_t=r\, then Proposition A.4.1(i) and (i) and Proposition 3.1 identify the whole law of L given r, at every horizon. (i) If every deviation is continuing, then under the hypotheses of Proposition E.1.1 the identified interval of the mean of X has width ∫(maxh−minh)P0(h,continuing∣r) ( _h- _h)\,P^0(dh,continuing r). When every hX_h has spread at least δ, the width is at least δ[1−∏j(1−ηj(r))]δ [1- _j(1- _j(r)) ]. Proof sketch. Part (i) follows from the chain rule and Lemma E.3.1; the bound follows by comparing factors. For (i), apply Propositions A.4.1 and 3.1, since agreement and terminal deviations exhaust the mass. For (i), subtract the mean endpoints in Proposition E.4.4; the lower bound uses continuing mass equal to one minus the agreement mass in (i). ∎ Appendix F Proofs: Supported Continuation, Unsupported Inputs, and Model Updates This appendix proves the continuation results of Section 3.4: Proposition A.5.1, Proposition F.5.2, and Corollary F.6.1 in a finite coordinate model, using the sequential g-formula (Robins, 1986; Pearl and Robins, 1995) and partial identification (Manski, 2003). It also proves that section’s execution-budget and snapshot-design results. F.1 Finite Coordinate Model This is the model for the proof of Proposition A.5.1, summarized in Section 3.4. Coordinates in generation order are V1,…,VnV_1,…,V_n with finite ranges 1,…,nV_1,…,V_n, and Ω=∏i = _iV_i. For S⊆[n]=1,…,nS [n]=\1,…,n\, VS=(Vi)i∈SV_S=(V_i)_i∈ S, S=∏i∈SiV_S= _i∈ SV_i, and vSv_S is the restriction of v∈Ωv∈ to S. Kernel i has declared input set Si⊆[i−1]S_i [i-1] and conditional law ki(⋅∣vSi)k_i(· v_S_i) on iV_i. The baseline law is P0(v)=∏i=1nki(vi∣vSi),v∈Ω.P^0(v)= _i=1^nk_i(v_i v_S_i), v∈ . (9) A declared set i⊆SiK_i _S_i collects inputs where kik_i is known by declaration (default i=∅K_i= ). Tree mechanisms of Proposition A.4.1 embed into coordinates by allocating one slot per history where call order or kernel identity varies. Inactive slots emit a dummy value. Replaced slots are those where replaced and baseline kernels differ. The post-abort path is a single valuation slot carrying the law of L given the prefix (declared as bκb_κ after terminal deviations by (A3)). Allowed sets ℰj,zE_j,z exclude the dummy at active inputs, and equal ℓ(ω):ω extends p\ (ω):ω extends p\ at undeclared abort prefixes p. Replacement. Replacement κ acts at boundary s, replacing kernels Dκ⊆s,…,nD_κ \s,…,n\ by known kernels kjκ(⋅∣vSjκ)k^κ_j(· v_S^κ_j) with Sjκ⊆[j−1]S^κ_j [j-1] (with kjκ=δfjκ(vSjκ)k^κ_j= _f^κ_j(v_S^κ_j) for deterministic replacements). For i∉Dκi∉ D_κ, kiκ=kik^κ_i=k_i and Siκ=SiS^κ_i=S_i. Invariance and prefix preservation ((A1) and (A2)) give Pκ(v)=∏i=1nkiκ(vi∣vSiκ).P^κ(v)= _i=1^nk^κ_i(v_i v_S^κ_i). (10) Here P0=PE,KP^0=P_E,K and Pκ=PEκ,KκP^κ=P_E^κ,K^κ on Ω . Loss and Records. Loss is L=ℓ(V)=ℓ¯(VSL)L= (V)= (V_S_L) for SL⊆[n]S_L [n] and ℓ¯:SL→ _S_L . Records are V_O for ⊆[n]O [n]. The pre-intervention record is Rt=VSrR_t=V_S_r with Sr⊆∩[s−1]S_r ∩[s-1] and P0(Rt=r)>0P^0(R_t=r)>0 (t=−1,Sr=∅t=-1,S_r= for unconditional queries). A value v is r-compatible when vSr=rv_S_r=r. The continuation query is Qtκ(B∣r)=Pκ(L∈B∣Rt=r)Q^κ_t(B r)=P^κ(L∈ B R_t=r) for B⊆B . Definition F.1.1 (Downstream and Relevant Sets). The downstream set Δκ⊆[n] _κ [n] is defined recursively in index order: i∈Δκi∈ _κ if i∈Dκi∈ D_κ, or if i∉Dκi∉ D_κ and Si∩Δκ≠∅S_i∩ _κ≠ . Its complement Δ¯κ=[n]∖Δκ _κ=[n] _κ is the unaffected set. The relevant set JκJ_κ is the smallest set that contains SL∪SrS_L∪ S_r and satisfies Sjκ⊆JκS^κ_j J_κ for every j∈Jκ∩Δκj∈ J_κ∩ _κ. A set K⊆[n]K [n] is κ-closed when Sjκ⊆KS^κ_j K for every j∈K∩Δκj∈ K∩ _κ. The recursion is well defined because Si⊆[i−1]S_i [i-1]; the smallest set exists by intersection of closed sets. F.2 Assumptions and Their Deployment Reading These are the assumptions for Proposition A.5.1 (Section 3.4). (G1) Support. For every j∈Jκ∩(Δκ∖Dκ)j∈ J_κ∩( _κ D_κ) and every z∈Sj∖jz _S_j _j, Pκ(VSj=z,Rt=r)>0P^κ(V_S_j=z,\ R_t=r)>0 implies P0(VSj=z)>0P^0(V_S_j=z)>0. (G2) Recorded downstream inputs. Sj⊆S_j for every j∈Jκ∩(Δκ∖Dκ)j∈ J_κ∩( _κ D_κ). (G3) Recorded loss inputs. SL⊆S_L . (G4) Recorded assignment. Sjκ⊆S^κ_j and kjκk^κ_j is known for every j∈Jκ∩Dκj∈ J_κ∩ D_κ. For an unchanged agent reading full text context, (G1) fails if a refusal message or regenerated text has zero baseline probability at that position. Coarsening that context creates support only under a sufficient-input assumption that logs alone cannot confirm. F.3 Structural Lemmas These lemmas support the proof of Proposition A.5.1 and its extension to unsupported inputs (Section 3.4). Every i∈Δ¯κi∈ _κ has i∉Dκi∉ D_κ and Si⊆Δ¯κS_i _κ, so Δκ⊆s,…,n _κ \s,…,n\ and Sr⊆Δ¯κS_r _κ; minimality and (G2) to (G4) give Jκ⊆J_κ . Lemma F.3.1 (Truncated Factorization). Under both laws, the marginal of VΔ¯κV_ _κ is ∏i∈Δ¯κki(vi∣vSi) _i∈ _κk_i(v_i v_S_i); in particular PκP^κ and P0P^0 agree on VΔ¯κV_ _κ and on RtR_t. For every κ-closed K and w∈Kw _K, Pκ(VK=w) P^κ(V_K=w) (11) =P0(VK∩Δ¯κ=wK∩Δ¯κ) =P^0\! (V_K∩ _κ=w_K∩ _κ ) ∏j∈K∩Δκkjκ(wj∣wSjκ). _j∈ K∩ _κk^κ_j\! (w_j w_S^κ_j ). Proof sketch. Apply the causal Markov factorization (Pearl, 2009a, Theorem 1, Eq. (15)) to the finite independent-seed model of PκP^κ, in whose replacement graph Δ¯κ _κ and K∪Δ¯κK∪ _κ are ancestral. Marginalizing the latter to K gives (11) by κ-closure. ∎ Lemma F.3.2 (Kernel Recovery). Let j∈Δκj∈ _κ, and let K⊆Δ¯κ∪(Δκ∩[j−1])K _κ∪( _κ∩[j-1]) contain SjS_j. If P0(VK=u)>0P^0(V_K=u)>0, then P0(Vj=a∣VK=u)=kj(a∣uSj)P^0(V_j=a V_K=u)=k_j(a u_S_j) for every a∈ja _j, where kjk_j is the baseline kernel. Proof. Because K contains only nondescendants of j along with its inputs SjS_j, the claim follows from the parental Markov condition for (9) (Pearl, 2009b, Theorem 1.2.7). ∎ F.4 Full Statement and Proof of Proposition A.5.1 Enumerate Jκ∩Δκ=j1<⋯<jqJ_κ∩ _κ=\j_1<…<j_q\ and set Km=(Jκ∩Δ¯κ)∪j1,…,jmK_m=(J_κ∩ _κ)∪\j_1,…,j_m\ for 0≤m≤q0≤ m≤ q (Kq=JκK_q=J_κ). For unchanged j, let j⊆Sj∖jZ_j _S_j _j be inputs, and let λ assign λj,z∈Δ(j) _j,z∈ (V_j) to each z∈jz _j. For r-compatible v∈Jκv _J_κ, define G0λ(v)=P0(VK0=vK0)G^λ_0(v)=P^0(V_K_0=v_K_0) and Gmλ(v)=Gm−1λ(v)cjmλ(v)G^λ_m(v)=G^λ_m-1(v)\,c^λ_j_m(v) (00 if Gm−1λ(v)=0G^λ_m-1(v)=0), where cjλ(v)=kj(vj∣vSj),j∉Dκ,vSj∈j,P0(Vj=vj∣VSj=vSj),j∉Dκ,vSj∉j∪j,kjκ(vj∣vSjκ),j∈Dκ,λj,vSj(vj),j∉Dκ,vSj∈j. gatheredc^λ_j(v)=\\ casesk_j\! (v_j v_S_j ), j∉ D_κ,\ v_S_j _j,\\ aligned &P^0\! (V_j=v_j V_S_j=v_S_j ),\\ & j∉ D_κ,\ v_S_j _j _j, aligned\\ k^κ_j\! (v_j v_S^κ_j ), j∈ D_κ,\\ _j,v_S_j(v_j), j∉ D_κ,\ v_S_j _j. cases gathered (12) Here every j=∅Z_j= , so the fourth case never applies; write cjc_j and G=GqG=G_q. Section F.5 takes jZ_j to be the null inputs. Full Statement. In the finite coordinate model, let P0(Rt=r)>0P^0(R_t=r)>0. (i) g-formula. Under (G1), (G2), (G3), and (G4), every cjc_j used in G is well defined, and Pκ(VJκ=v)=G(v)P^κ(V_J_κ=v)=G(v) for every r-compatible v∈Jκv _J_κ. Hence, for every B⊆B , Qtκ(B∣r)=1P0(Rt=r)∑v∈Jκ:vSr=r,ℓ¯(vSL)∈BG(v).Q^κ_t(B r)= 1P^0(R_t=r) _ subarraycv _J_κ:\\ \ v_S_r=r,\\ \ (v_S_L)∈ B subarrayG(v). (13) The right side depends only on the baseline record law, the declared inputs, the declared kernel values, ℓ¯ , and the known replacement kernels. The vector law Qtκ(⋅∣r)Q^κ_t(· r) and every query ρ(ϕ#Qtκ(⋅∣r))ρ( _\#Q^κ_t(· r)) are therefore identified within mechanisms that share the declared inputs and declared kernel values. (i) Support is checkable. Under (G2), (G3), and (G4), whether (G1) holds is determined by the baseline record law and the declared kernel values. (i) Zero agreement. There exists a mechanism satisfying (G1) to (G4) in which the baseline and the replacement are deterministic given a recorded tape. Its agreement mass is 00, and its replacement risk is identified as 1/21/2. (iv) Composition with Proposition A.4.1. Let the coordinate list embed a tree mechanism of Proposition A.4.1 as in Section F.1, with (R), (A1), (A2), and (A3) of that proposition, and a conditioning record generated before every replaced slot. Then (G1) holds at every input that the replacement reaches on an agreement path, and every downstream input reached after a terminal deviation is declared. Under (G1) to (G4), Proposition A.4.1(i) and (i) give the restrictions of Qtκ(⋅∣r)Q^κ_t(· r) to the agreement set and to terminal deviations. The continuing part is therefore identified as the remainder. (v) Unsupported inputs. Without (G1), the identified set is the image described in Proposition F.5.2. Conditions (G2) and (G4) cannot be dropped, and (G3) cannot be weakened to recording L alone (verify_supported.py, Appendix H). Proof sketch. Part (i) is the sequential g-formula (Robins, 1986; Pearl and Robins, 1995), established here in Proposition F.5.2(a),(c). For (i), Jκ⊆J_κ makes the recursion observable up to any first reached undeclared null input, which detects failure of (G1). For (i), record all coordinates of U∼Bernoulli(1/2)U (1/2), baseline A=UA=U, replacement A=1−UA=1-U, and Y whose kernel reads only A, with P(Y=1∣A=0)=1/4P(Y=1 A=0)=1/4 and P(Y=1∣A=1)=3/4P(Y=1 A=1)=3/4; take L=YL=Y and no conditioning record. Both outcome inputs have baseline support, all decisions disagree, and the g-formula gives replacement risk 1/21/2. For (iv), Lemma E.3.1 gives support on agreement paths, and (A3) declares terminal valuations; subtract the two restrictions in Proposition A.4.1. Part (v) is Proposition F.5.2. ∎ F.5 Continuation from Records with Unsupported Inputs To handle unsupported inputs in Section 3.4, we keep (A1), (A2), and (G2) to (G4), drop (G1), and vary kernel laws at unsupported inputs within allowed sets. In the coordinate model of Section F.1, let κ=Jκ∩(Δκ∖Dκ)U_κ=J_κ∩( _κ D_κ). For j∈κj _κ and z∈Sj∖jz _S_j _j, kernel j emits values in a nonempty allowed set ℰj,z⊆jE_j,z _j (default jV_j). Members of ℳ0M_0 share the declared inputs, declared kernel values, known replacement kernels, and allowed sets. Each coordinate has its own kernel; restrictions tying slots are addressed in Remark F.5.4. The population identified set is Θr=Qκt,M(⋅∣r):M∈ℳ0, _r= \Q^κ_t,M(· r):\ M _0, (14) V has the observed record law under P0M. V_O has the observed record law under P^0_M \. Under (G2), an input z∈Sj∖jz _S_j _j with P0(VSj=z)=0P^0(V_S_j=z)=0 is a null input; collect them in jZ_j. The null blocks are ℬ=(j,z):j∈κ,z∈jB=\(j,z):j _κ,\ z _j\, and free families form Λ=∏(j,z)∈ℬΔ(ℰj,z) = _(j,z) (E_j,z). For a member M with the observed record law, define its own null-input family by λM=(kjM(⋅∣z))(j,z)∈ℬ _M=(k^M_j(· z))_(j,z) . For λ∈Λλ∈ , the recursion of Section F.4 defines GλG^λ via (12), and Qλ(B∣r)=1P0(Rt=r)∑v∈Jκ:vSr=r,ℓ¯(vSL)∈BGλ(v).Q^λ(B r)= 1P^0(R_t=r) _ subarraycv _J_κ:\\ \ v_S_r=r,\\ \ (v_S_L)∈ B subarrayG^λ(v). (15) The class ℳ0M_0 is closed at null inputs if for each member M with the observed record law and each λ∈Λλ∈ , setting kj(⋅∣z)=λj,zk_j(· z)= _j,z on ℬB yields a member Mλ∈ℳ0M^λ _0. Lemma F.5.1 (Zero-Support Modification in the Coordinate Model). Let M and M′M have the same declared inputs and the same kernels, except kernel j at inputs in a set ⊆SjZ _S_j. If PM0(VSj∈)=0P^0_M(V_S_j )=0, then PM′0=PM0P^0_M =P^0_M. Proof. The products (9) of M and M′M differ only where vSj∈v_S_j . Since Sj⊆[j−1]S_j [j-1], the probability of VSj∈\V_S_j \ depends only on the shared kernels 1,…,j−11,…,j-1, so it is 00 under both and both laws vanish there. ∎ Proposition F.5.2 (Continuation from Records with Unsupported Inputs). In the finite coordinate model, assume (A1) and (A2) in the form (10), together with (G2), (G3), and (G4). Condition (G1) is not assumed. (a) Outer set. Let M have the declared inputs, the declared kernel values, and the known replacement kernels, with PM0(Rt=r)>0P^0_M(R_t=r)>0. Formula (15), computed from the record law of M with λ=λMλ= _M, equals Qt,Mκ(⋅∣r)Q^κ_t,M(· r). Hence Θr⊆Qλ(⋅∣r):λ∈Λ _r \Q^λ(· r):λ∈ \, where each QλQ^λ is computed from the observed record law. (b) Sharpness. If ℳ0M_0 is closed at null inputs, then Θr=Qλ(⋅∣r):λ∈Λ _r=\Q^λ(· r):λ∈ \. (c) Supported extreme. Suppose (G1) holds; by Proposition A.5.1(i), this is a property of the observed record law and the declared kernel values. Then Qλ(⋅∣r)Q^λ(· r) equals the right side of (13) for every λ∈Λλ∈ , and the image is the single law of Proposition A.5.1(i). Proof of (a). Fix M and λ=λMλ= _M. Each KmK_m is κ-closed, so Lemma F.3.1 gives Πm(v) _m(v) :=PMκ(VKm=vKm) :=P^κ_M\! (V_K_m=v_K_m ) (16) =PM0(VK0=vK0) =P^0_M\! (V_K_0=v_K_0 ) ∏l≤mkjlκ(vjl∣vSjlκ). _l≤ mk^κ_j_l\! (v_j_l v_S^κ_j_l ). Lemma F.3.2 and the definitions of declared, replacement, and null factors give GmλM=ΠmG _M_m= _m, including zero prefixes. Summing and conditioning on r gives (15); Jκ⊆J_κ makes all terms except λ observable, proving the inclusion. ∎ Proof of (b). For λ∈Λλ∈ and a compatible M, closure gives Mλ∈ℳ0M^λ _0. Resetting the null blocks one at a time, Lemma F.5.1 keeps the baseline law at each step, so PMλ0=PM0P^0_M^λ=P^0_M and λMλ=λ _M^λ=λ. Part (a) for MλM^λ gives Qλ(⋅∣r)=Qt,Mλκ(⋅∣r)∈ΘrQ^λ(· r)=Q^κ_t,M^λ(· r)∈ _r. ∎ Proof of (c). By (G1), no first undeclared null input can follow a positive r-compatible prefix in (a); zero prefixes stay zero. Thus no free factor is used, so Gλ=G^λ=G for every λ, giving (13) by (a). ∎ Remark F.5.3 (What Finite Logs Show). Under (G2) to (G4), the population record law determines null inputs. Absence from a finite log does not prove an input is null. Treating unobserved inputs as null still yields a valid outer set. Setting free arguments to the true conditional law returns (12), so the enlarged image contains the true identified set. Finite-sample inference is a separate claim (Limitations). Remark F.5.4 (Scope of Sharpness). Part (b) uses that each coordinate’s kernel is free at its own null inputs. In the slot embedding of Section F.1, several slots can host one named kernel. A class that ties slots, such as one law per kernel and step when the embedding needs more slots than kernel and step pairs, is covered by the outer-set clause of Proposition A.5.1. It is a subclass with the same evidence, so part (a) still gives an outer set for it. Its identified set can be smaller. F.6 Model Updates: Statement and Proof This is the model-release result of Section 3.4. Corollary F.6.1 (Model updates). Assume (A1) and (A2) for every replaced decision, and let κ replace the agent policy at its decisions from the boundary onward, under an interface whose output contains every action and dynamic state that later kernels or ℓ read; a model update applied from the episode start replaces every decision. Suppose the baseline policy is deterministic given its decision input and a random tape, and that decision inputs, tapes, and baseline outputs are recorded. If the new policy is seed-addressable, that is, evaluable deterministically at each logged input and tape, then the agreement mass κ(r)=Pκ(κ∣r) m_κ(r)=P^κ( A_κ r) is identified. It is estimated by the empirical agreement frequency over independent baseline episodes and is at most the first-decision agreement probability. With the loss value recorded, the agreement contribution is identified as well. Proof sketch. Including tapes in the inputs, the stated determinism and recording give (R); Lemma E.3.1 identifies agreement mass and its logged loss contribution. Seed-addressable evaluation determines the agreement indicators, whose empirical frequency is consistent by the strong law. The bound follows since agreement throughout implies first-decision agreement. ∎ F.7 Budgeted Targeted Execution: Statement and Proof This subsection proves the sampling and restoration bounds used in Section 3.4. Scripts in checks/ reproduce the E1 and E7 bounds and check finite instances; Appendix H and checks/README.md map each script to its claim. Replay supplies the agree and stop terms of display (2); a uniform sample of unresolved continuations bounds the rest. Hypergeometric and binomial inversion (Clopper and Pearson, 1934), a union bound, and error spending over declared looks (Lan and DeMets, 1983) determine how many executions a decision needs. Setting. Let harm be binary and q the changed system’s P(harm), the target qtκ(r)q^κ_t(r) with X the harm indicator. A pass-all log holds n episodes. Under (R), (A1), (A2), and (A3), replay resolves an episode’s outcome under the change when it agrees, when harm occurred before its first deviation, or when it stops and the abort valuation fixes the harm indicator (a point mass, as when a stop ends the episode with the harm accrued before it); b resolved episodes are harmful. A nondegenerate abort valuation would need an independent draw for each stopped episode. The remaining N continuing episodes are unresolved, partitioned into strata s of sizes NsN_s fixed by the log (for example, by the step of first deviation). Executing an unresolved episode’s continuation from its snapshot gives its outcome under the change, by (T). The completed cohort assigns each resolved episode its replayed outcome and each unresolved episode the outcome of its continuation; S is its harm count. Hypothesis (H). The completed outcomes are independent Bernoulli variables with common probability q; the random order in which unresolved episodes are executed is drawn independently of them, and the looks are fixed in advance. Independently sampled tasks and fresh seeds support (H); (T) links each continuation to its live law but does not by itself make outcomes independent across episodes, so dependence through shared serving or environment state lies outside it. Bounds. In stratum s, execute a uniform random sample without replacement of ksk_s unresolved episodes and observe xsx_s harms. With H(Ns,D,ks)H(N_s,D,k_s) the hypergeometric law of harms in such a sample when D of the NsN_s are harmful, let DsU(xs,ks,e) D_s^U(x_s,k_s;e) =maxD∈xs,…,Ns−ks+xs: = \D∈\x_s,…,N_s-k_s+x_s\: PrH(Ns,D,ks)(X≤xs)>e, _H(N_s,D,k_s)(X≤ x_s)>e \, with DsU=NsD_s^U=N_s when ks=0k_s=0; at ks=Nsk_s=N_s it returns xsx_s. Let SU=b+∑sDsUS^U=b+ _sD_s^U and let uCP(z,n,a)u_CP(z,n;a) be the one-sided Clopper-Pearson upper limit for z successes in n trials at level 1−a1-a, with uCP(n,n,a)=1u_CP(n,n;a)=1. Proposition F.7.1 (Budgeted targeted execution). (i) Given the completed cohort, Pr(S≤SU)≥1−∑ses (S≤ S^U)≥ 1- _se_s, where stratum s uses error ese_s. (i) Under (H), Pr(q≤uCP(SU,n,aL))≥1−aL−∑ses (q≤ u_CP(S^U,n;a_L) )≥ 1-a_L- _se_s. (i) Let samples be nested over declared looks j=1,…,Jj=1,…,J with sizes ks,jk_s,j and errors es,je_s,j, ∑s,jes,j≤aE _s,je_s,j≤ a_E, and let U¯j=minl≤juCP(SlU,n,aL) U_j= _l≤ ju_CP(S^U_l,n;a_L). Under (H), Pr(q≤U¯j for all j)≥1−aL−aE (q≤ U_j for all j)≥ 1-a_L-a_E. Stopping at the first look whose bound clears a target, or at look J, keeps this coverage, for every target at once. Proof. (i) If D>DsU(xs,ks,es)D>D_s^U(x_s,k_s;e_s) then PrH(Ns,D,ks)(X≤xs)≤es _H(N_s,D,k_s)(X≤ x_s)≤ e_s, so in each stratum the failure event is a lower tail of probability at most ese_s; a union bound gives the claim. (i) Combine (i) with Clopper-Pearson coverage for S∼Bin(n,q)S (n,q) under (H) and monotonicity in the count (Clopper and Pearson, 1934). (i) A union bound over strata and declared looks, intersected with the single Clopper-Pearson event for S, gives simultaneous coverage of the running minima. This also covers any selected look and every target. ∎ The guarantees above concern sampling error under exact restoration (T). Lemma F.7.2 prices restoration error, and Remark F.7.3 incorporates it into certified bounds. Lemma F.7.2 (Restoration Error). Assume (R) and (A1) to (A3), and let ν, whw_h, and Qh=ϕ#Pκ(L∈⋅∣[h])Q_h= _\#P^κ(L∈· [h]) be as in Proposition E.4.3. Let Q^h Q_h be the law of X=ϕ(L)X=φ(L) in the run restored at h+h^+, so that (T) says Q^h=Qh Q_h=Q_h, and let γh=maxB|Q^h(B)−Qh(B)| _h= _B| Q_h(B)-Q_h(B)|. Let P^=ν+∑hwhQ^h P=ν+ _hw_h Q_h be the law that display (2) gives when its continue term uses the restored laws, with mean μ μ, and let εκ=∑hwh _κ= _hw_h be the continuing mass. Then for every event B of X, |P^(B)−Pκ(X∈B∣r)|≤∑hwhγh≤εκmaxhγh, aligned &| P(B)-P^κ(X∈ B r)|\\ & ≤ _hw_h _h≤ _κ _h _h, aligned |μ^−Eκ[X∣r]|≤(max−min)∑hwhγh. aligned &| μ-E^κ[X r]|\\ & ≤( - ) _hw_h _h. aligned Proof. Both event bounds follow from the decomposition in Proposition E.4.3 and the triangle inequality; integrating tail differences over [min,max][ , ] gives the mean bound. ∎ Remark F.7.3 (Restoration Allowance). Proposition F.7.1 bounds the harm probability q q of P P when the completed restored outcomes satisfy hypothesis (H): independent Bernoulli with a common probability. Let u be its certified bound and ξ=∑hwhγhξ= _hw_h _h. Lemma F.7.2 gives |q−q^|≤ξ|q- q|≤ξ, so with the probability of the proposition q≤u+ξq≤ u+ξ, and a target q⋆q is cleared when u+ξ≤q⋆u+ξ≤ q ; exact (T) is the case ξ=0ξ=0. For a tolerance ξ0≥ξ _0≥ξ declared in advance, stopping at the first look with U¯j+ξ0≤q⋆ U_j+ _0≤ q keeps the coverage of part (i). The continuing mass εκ _κ is estimated from the log, so a population statement uses an upper confidence limit for it, whose error adds to that of the proposition, or the bound εκ≤1 _κ≤ 1. At prefixes with harm before the deviation, Qh=Q^hQ_h= Q_h for harm, so they drop out of the harm allowance; task success can still depend on the continuation, so a decision with a success floor needs its own allowance from the same lemma. Both bounds of the lemma are attained: with Qh=δminQ_h= _ and Q^h=(1−γ)δmin+γδmax Q_h=(1-γ) _ +γ _ for every h, the errors equal εκγ _κγ and (max−min)εκγ( - ) _κγ. A paired live run measures q−q^q- q itself and does not bound γh _h, since errors at different prefixes can offset. F.8 Necessity of the Execution Budget This subsection proves the execution limits and achievability claims of Section 3.4. Setting. Let harm be binary, and assume (R), (A1) to (A3), and (S) with feasible set 0,1\0,1\ at every unresolved prefix. Episodes are independent. Each is resolved and harmful with probability q0q_0, unresolved with probability m>0m>0, and resolved and harmless otherwise. An unresolved continuation is harmful with probability p∈(0,1)p∈(0,1). Write q=q0+mpq=q_0+mp, and assume ζ=q⋆−q>0ζ=q -q>0 and q⋆<q0+mq <q_0+m. A world gives every unresolved prefix a live harm probability p0p_0 and a restored one p p with |p0−p^|≤γ|p_0- p|≤γ. Condition (S) frees every live p0p_0 for a mechanism with the observed baseline law. We also let every restored p p within γ of p0p_0 occur, as in the attainment part of Remark F.7.3. The log then has one law across worlds, and each restored cohort satisfies (H) because episodes are independent. A procedure reads the log, may randomize internally, and executes unresolved episodes one at a time, each at most once and chosen adaptively. An execution reveals the record of one restored continuation, independent of the other executions given the log. Worlds may give these records any law with the stated harm probabilities, so a world can change a harm probability and keep the conditional law of the record given harm. It stops after K≤nK≤ n executions and certifies or not. Fix α,β∈(0,1)α,β∈(0,1) with α+β<1α+β<1 in this subsection; probabilities average over the log and any randomization. The size of a procedure is its largest certification probability over worlds with q0+mp0>q⋆q_0+mp_0>q . Its power is its certification probability in the world W1W_1 with p0=p^=p_0= p=p. It is valid if its size is at most α and powerful if its power is at least 1−β1-β. Let klkl be the binary relative entropy and p¯=p+(ζ−mγ)/m p=p+(ζ-mγ)/m. Proposition F.8.1 (Execution Budget: Necessity). In the setting above, the following hold. (i) If mγ≥ζmγ≥ζ, every procedure has power at most its size, so no valid procedure is powerful, for any n. (i) If mγ<ζmγ<ζ, every valid and powerful procedure has W1[K]≥kl(1−β,α)/kl(p,p¯)≥kl(1−β,α)m2p¯(1−p¯)/(ζ−mγ)2E_W_1[K] (1-β,α)/kl(p, p) (1-β,α)\,m^2 p(1- p)/(ζ-mγ)^2. The first bound diverges as mγ↑ζmγ ζ. (i) Consider a sequential test of independent live episodes whose stopping time KLK_L has finite mean at live harm q. If it certifies with probability at most α under every episode law whose harm probability exceeds q⋆q , and at least 1−β1-β at harm q, then q[KL]≥kl(1−β,α)/kl(q,q⋆)≥kl(1−β,α)q⋆(1−q⋆)/ζ2E_q[K_L] (1-β,α)/kl(q,q ) (1-β,α)\,q (1-q )/ζ^2. Proof. For ε>0 >0, let W0εW_0 have p0=p+(ζ+ε)/mp_0=p+(ζ+ )/m and p^ε=maxp0−γ,p p_ = \p_0-γ,p\. For small ε it is a world, since p0<1p_0<1 when q⋆<q0+mq <q_0+m, and its live harm is q⋆+εq + . At every prefix, W0εW_0 keeps the conditional law of the restored record given harm from W1W_1. Let E be the event that the procedure certifies, with laws ℙ1P_1 in W1W_1 and ℙ0P_0 in W0εW_0 . The log has the same law in both. Since W0εW_0 has live harm above q⋆q , ℙ0(E)P_0(E) is at most the size, and at most α for a valid procedure. (i) Let mγ≥ζmγ≥ζ. Then p^ε−p≤ε/m p_ -p≤ /m. Draw one uniform variable per unresolved episode, and let the episode be harmful when the variable falls below p in W1W_1 and below p^ε p_ in W0εW_0 . Draw the rest of its record from the common conditional law given harm. The two outcomes differ with probability at most ε/m /m per episode. The procedure acts identically unless one of the at most n unresolved outcomes differs, so ℙ1(E)≤ℙ0(E)+nε/mP_1(E) _0(E)+n /m. Letting ε↓0 0 bounds the power by the size. A valid procedure has size at most α<1−βα<1-β, so it is not powerful. (i) Let mγ<ζmγ<ζ, so p^ε=p¯+ε/m∈(p,1) p_ = p+ /m∈(p,1) for small ε , since p¯≤(q⋆−q0)/m<1 p≤(q -q_0)/m<1. Conditional on the common log and internal randomization G, unused episodes are independent arms. Their record laws have common conditional laws given harm, hence are mutually absolutely continuous with divergence kl(p,p^ε)kl(p, p_ ). The stopping time satisfies K≤nK≤ n. Apply Kaufmann et al. (2016, Lemma 1) conditionally and average using joint convexity of klkl: 1[K]kl(p,p^ε) _1[K]\,kl(p, p_ ) ≥kl(ℙ1(E),ℙ0(E)) (P_1(E),P_0(E)) ≥kl(1−β,α), (1-β,α), by validity, power, and binary-KL monotonicity. Let ε↓0 0. The standard binary-KL bound kl(p,p¯)≤(p¯−p)2/p¯(1−p¯)kl(p, p)≤( p-p)^2/\ p(1- p)\ gives the second bound. As mγ↑ζmγ ζ, p¯↓p p p and the first bound diverges. (i) Give the unsafe live law harm probability q⋆+εq + , keeping the conditional record law given harm from W1W_1. For small ε , 0<q<q⋆+ε<10<q<q + <1. Apply the same lemma with one arm, stopping at minKL,t \K_L,t\ and event E∩KL≤tE∩\K_L≤ t\. Let t→∞t→∞, using q[KL]<∞E_q[K_L]<∞, and then ε↓0 0. The same binary-KL bound gives the second inequality. ∎ Achievability. Sequential probability ratio tests (Wald, 1945, SPRTs;) approach the bounds of Proposition F.8.1(i) and (i) as error levels fall and the log grows, with a finite-pool allowance; Remark F.8.4 treats estimation of q0q_0 and m. Let mγ<ζmγ<ζ, and put up(a,c)=log(1−a)/(1−c)up(a,c)= \(1-a)/(1-c)\ for 0<a<c<10<a<c<1. The log has one law in every world, so a procedure may use q0q_0 and m. The execution test with levels α,β′∈(0,1)α,β ∈(0,1) uses p¯=(q⋆−q0)/m−γ p=(q -q_0)/m-γ. It executes unresolved episodes in any order and reads only their harm bits. Starting at Ξ0=0 _0=0, it adds log(p/p¯) (p/ p) after a harm and up(p,p¯)up(p, p) after a harmless outcome. It certifies when Ξt≥log(1/α) _t≥ (1/α), and stops without certifying when Ξt≤−log(1/β′) _t≤- (1/β ) or all N unresolved episodes are used. The live test applies the same rule to live harm bits, with (q,q⋆)(q,q ) in place of (p,p¯)(p, p) and no pool. A test with thresholds A,B>0A,B>0 uses A and B in place of log(1/α) (1/α) and log(1/β′) (1/β ). Both tests look after every outcome, and Ville’s inequality covers all looks. Proposition F.8.2 (Execution Budget: Achievability). Assume the setting of Proposition F.8.1 with mγ<ζmγ<ζ. Let τ be the stopping time of the execution test with levels α,β′∈(0,1)α,β ∈(0,1) and an unlimited pool. Put K¯ex=log(1/α)+up(p,p¯)/kl(p,p¯) K_ex=\ (1/α)+up(p, p)\/kl(p, p) and χn=2K¯ex/(mn)+e−m2n/2 _n=2 K_ex/(mn)+e^-m^2n/2. (i) The size of the test is at most α. For any thresholds, certification is nonincreasing in the restored harm rate, so the size is the certification probability at p^=p¯ p= p. This holds in every world with q0+mp0>q⋆q_0+mp_0>q , for every p p within γ of p0p_0 and every record law given harm. (i) The power is at least 1−β′−χn1-β - _n. Also W1[K]≤p[τ]≤K¯exE_W_1[K] _p[τ]≤ K_ex, where pE_p refers to independent Bernoulli(p)(p) bits. (i) Let the live episodes be independent. The live test certifies with probability at most α when every episode has harm probability at least q⋆q , and with probability at least 1−β′1-β at harm q. Also q[KL]≤K¯lv=log(1/α)+up(q,q⋆)/kl(q,q⋆)E_q[K_L]≤ K_lv=\ (1/α)+up(q,q )\/kl(q,q ). Proof. For the Bernoulli SPRT score Z (Wald, 1945), a direct computation gives ϑeZ=1−(ϑ−c)(c−a)/c(1−c)E_ e^Z=1-( -c)(c-a)/\c(1-c)\, ae−Z=1E_ae^-Z=1, and aZ=kl(a,c)E_aZ=kl(a,c) for 0<a<c<10<a<c<1; take (a,c)=(p,p¯)(a,c)=(p, p). (i) Given the log, executed bits are independent Bernoulli(p^)( p) with p^≥p0−γ>p¯ p≥ p_0-γ> p, whatever the record law. Thus eΞte _t, stopped at the pool, is a nonnegative supermartingale starting at one. Ville’s inequality (Ville, 1939, Chapter V, Theorem 1, Eq. (15)), applied after adding the predictable decreases and approaching the threshold from below, bounds certification by α. Coupling by uniforms makes certification nonincreasing in p p; finite-pool continuity gives the size at p¯ p. (i) At W1W_1, Ville’s inequality for e−Ξte^- _t bounds lower exit by β′β . A run of ⌈log(1/α)+log(1/β′)/up(p,p¯)⌉ \ (1/α)+ (1/β )\/up(p, p) harmless outcomes leaves the strip, so τ has a geometric tail. Wald’s identity (Wald, 1944), with upper overshoot at most up(p,p¯)up(p, p), gives p[τ]≤K¯exE_p[τ]≤ K_ex. Since K=minτ,N≤τK= \τ,N\≤τ, the expected-cost bound follows. Failure requires a lower exit or pool exhaustion; Markov’s and Hoeffding’s inequalities with N∼Bin(n,m)N (n,m) give Pr(τ>N)≤χn (τ>N)≤ _n, hence power at least 1−β′−χn1-β - _n. (i) The same argument with (a,c)=(q,q⋆)(a,c)=(q,q ) and no pool gives the live bounds. Size requires only conditional harm probability at least q⋆q ; independent Bernoulli(q)(q) bits give the power and mean bounds. ∎ Corollary F.8.3 (Cost Bounds and Ratio). Let mγ<ζmγ<ζ, α+β<1α+β<1, and χn<β _n<β. Let CexC_ex be the infimum of W1[K]E_W_1[K] over valid and powerful procedures. Let ClvC_lv be the infimum of q[KL]E_q[K_L] over the live tests of Proposition F.8.1(i). Write klex=kl(p,p¯)kl_ex=kl(p, p), kllv=kl(q,q⋆)kl_lv=kl(q,q ), upex=up(p,p¯)up_ex=up(p, p), and uplv=up(q,q⋆)up_lv=up(q,q ). Then kl(1−β,α)klex kl(1-β,α)kl_ex ≤Cex≤log(1/α)+upexklex, ≤ C_ex≤ (1/α)+up_exkl_ex, kl(1−β,α)kllv kl(1-β,α)kl_lv ≤Clv≤log(1/α)+uplvkllv. ≤ C_lv≤ (1/α)+up_lvkl_lv. Each upper bound exceeds its lower bound by at most [up+βlog(1/α)+log(1/β)+1]/kl[up+β\ (1/α)+ (1/β)+1\]/kl with matching subscripts. Moreover CexClv C_exC_lv ≥kl(1−β,α)log(1/α)+uplv⋅kllvklex, ≥ kl(1-β,α) (1/α)+up_lv· kl_lvkl_ex, CexClv C_exC_lv ≤log(1/α)+upexkl(1−β,α)⋅kllvklex. ≤ (1/α)+up_exkl(1-β,α)· kl_lvkl_ex. Both outer factors tend to 11 as α,β↓0α,β 0 with n large enough for χn<β _n<β, so Cex/Clv→kllv/klexC_ex/C_lv _lv/kl_ex. Proof. Combine Propositions F.8.1 and F.8.2, taking β′=β−χnβ =β- _n for executions and β′=β =β for live episodes; the ratio bounds divide the cost bounds, and expanding kl(1−β,α)kl(1-β,α) with −(1−β)log(1−β)≤β-(1-β) (1-β)≤β and βlog(1−α)≤0β (1-α)≤ 0 gives the gaps and limiting factors. ∎ With Proposition F.8.1(i), this makes γ=ζ/mγ=ζ/m the sharp threshold as n grows. For every γ<ζ/mγ<ζ/m there is an n0n_0, depending also on α and β, such that for n≥n0n≥ n_0 a valid and powerful procedure exists. For γ≥ζ/mγ≥ζ/m none exists at any n. Remark F.8.4 (Estimating q0q_0 and m). A finite log gives only b/nb/n and N/nN/n, and p¯ p decreases in q0q_0 and in m. Let q0U≥q0q_0^U≥ q_0 and mU≥m^U≥ m be Clopper–Pearson upper limits at level αlog/2 _ /2 each, so that both hold with probability at least 1−αlog1- _ . Run the execution test with p¯U=(q⋆−q0U)/mU−γ p^U=(q -q_0^U)/m^U-γ in place of p¯ p and the realized N as pool, and require p<p¯U<1p< p^U<1 before evaluating the test, never certifying when this condition fails. On the event of the limits, p¯U≤p¯<p p^U≤ p< p, so the size is at most α+αlogα+ _ . Given a log with p<p¯U<1p< p^U<1, the argument of (i) at p¯U p^U gives [K∣log]≤K¯UE[K ]≤ K^U, and Markov’s inequality bounds pool exhaustion by K¯U/N K^U/N, so the failure probability is at most β′+K¯U/Nβ + K^U/N, where K¯U K^U is K¯ex K_ex at p¯U p^U. Unconditionally, the power loses at most ℙ(p¯U≤p or p¯U≥1)+[min1,K¯U/N;p<p¯U<1]P( p^U≤ p or p^U≥ 1)+E[ \1, K^U/N\;p< p^U<1]. Both terms vanish as n grows, because p¯U→p¯∈(p,1) p^U→ p∈(p,1) and N→∞N→∞ in probability. F.9 Execution Across Strata This extends the execution bounds of Section 3.4 to strata. Setting. We extend the framework of Appendix F.8 to strata s=1,…,Ss=1,…,S, such as the step where the gate first blocks. An episode is unresolved in stratum s with probability ws>0w_s>0, so ∑sws=m _sw_s=m. In stratum s, continuations are harmful with probability ps∈(0,1)p_s∈(0,1), restoration error is at most γs∈[0,1] _s∈[0,1], and each execution costs cs>0c_s>0 (for example, in agent calls); live episodes cost cL>0c_L>0. A world assigns stratum s live harm probability p0sp_0s and restored rate p^s p_s with |p0s−p^s|≤γs|p_0s- p_s|≤ _s. An adaptive procedure executes unused unresolved episodes in chosen strata, incurring cost C=∑scsKsC= _sc_sK_s. Let q=q0+∑swspsq=q_0+ _sw_sp_s, ζ=q⋆−q>0ζ=q -q>0, and q⋆<q0+mq <q_0+m. Power is evaluated at world W1W_1 (p0s=p^s=psp_0s= p_s=p_s), and size is the maximum certification probability over worlds with q0+∑swsp0s>q⋆q_0+ _sw_sp_0s>q . A restored vector can come from a world of the null only if the live harm it allows, at most q0+∑swsmin1,p^s+γsq_0+ _sw_s \1, p_s+ _s\, exceeds q⋆q . So the restored vectors of the null lie in the convex set = = \ r∈[0,1]S: r∈[0,1]^S: q0+∑swsmin1,rs+γs≥q⋆, q_0+ _sw_s \1,r_s+ _s\≥ q \, and every r∈(0,1)Sr∈(0,1)^S with strict inequality is one. Let ξ=∑swsminγs,1−psξ= _sw_s \ _s,1-p_s\ cap each restoration error at 1−ps1-p_s (Remark F.7.3), put ζ′=ζ−ξζ =ζ-ξ, and let J=s:ps+γs<1J=\s:p_s+ _s<1\. For s∉Js∉ J, null worlds can keep restored rate psp_s while setting live harm to one, so the design below does not sample these strata. For s∈Js∈ J and t≥0t≥ 0, let zs(t)∈[ps,1)z_s(t)∈[p_s,1) solve kl(ps,zs(t))=cstkl(p_s,z_s(t))=c_st, and set bs(t)=min1−γs,zs(t)b_s(t)= \1- _s,z_s(t)\. When ζ′>0ζ >0, let t∗t_* be the unique positive root of ∑s∈Jwsbs(t)−ps=ζ′, _s∈ Jw_s\b_s(t)-p_s\=ζ , (17) We define the design point: p¯s=bs(t∗) p_s=b_s(t_*) on J and p¯s=ps p_s=p_s off J; active strata J∗=s∈J:p¯s<1−γsJ_*=\s∈ J: p_s<1- _s\; slopes gs=(p¯s−ps)/p¯s(1−p¯s)g_s=( p_s-p_s)/\ p_s(1- p_s)\; execution shares as∝ws/gsa_s w_s/g_s on J∗J_* (as=0a_s=0 elsewhere); and mean cost c¯=∑sascs c= _sa_sc_s. With S=1S=1, p¯1 p_1 is the p¯ p of Appendix F.8. Proposition F.9.1 (Execution across Strata: Necessity and Allocation). In the setting above, the following hold. (i) If ξ≥ζξ≥ζ, every procedure has power at most its size. If every ps+γs≤1p_s+ _s≤ 1, then ξ=∑swsγsξ= _sw_s _s; otherwise ∑swsγs≥ζ _sw_s _s≥ζ does not suffice. (i) If ζ′>0ζ >0, then (17) has a unique root t∗>0t_*>0, J∗J_* is nonempty, and every valid and powerful procedure has W1[C]≥kl(1−β,α)/t∗E_W_1[C] (1-β,α)/t_*. (i) Let ζ′>0ζ >0. Then t∗=maxλinfr∈∑sλskl(ps,rs)/cs=minr∈maxskl(ps,rs)/cst_*= _λ _r _s _skl(p_s,r_s)/c_s= _r _skl(p_s,r_s)/c_s, with λ ranging over cost shares (λs≥0 _s≥ 0, ∑sλs=1 _s _s=1). The cost shares λs∗=ascs/c¯λ^*_s=a_sc_s/ c and the vector p¯ p form a saddle point, every stratum in J∗J_* has kl(ps,p¯s)=cst∗kl(p_s, p_s)=c_st_*, and every r∈r has ∑s∈J∗ws(rs−p¯s)≥0 _s∈ J_*w_s(r_s- p_s)≥ 0. (iv) Let every ps+γs<1p_s+ _s<1 and q⋆↓q+ξq q+ξ, and put V=∑swsps(1−ps)csV= _sw_s p_s(1-p_s)c_s. Then 1/t∗=2V2ζ′−21+O(ζ′)1/t_*=2V^2ζ -2\1+O(ζ )\, and asa_s tends to wsps(1−ps)/cs/∑jwjpj(1−pj)/cjw_s p_s(1-p_s)/c_s/ _jw_j p_j(1-p_j)/c_j, the cost-weighted allocation of Neyman (1934). With S=1S=1 and c1=1c_1=1, (i) and (i) are Proposition F.8.1(i) and the first bound of (i). If ∑swsγs<ζ _sw_s _s<ζ, then 1/t∗≤cpool/kl(ppool,ppool+(ζ−∑swsγs)/m)1/t_*≤ c_pool/kl(p_pool,p_pool+(ζ- _sw_s _s)/m) with ppool=∑swsps/mp_pool= _sw_sp_s/m and cpool=∑swscs/mc_pool= _sw_sc_s/m: the strata never raise the bound of Proposition F.8.1(i) applied to the pooled rate at the mean cost. (v) Replace the strata of a set I by one stratum with mass ∑s∈Iws _s∈ Iw_s, the mass-weighted means of psp_s and γs _s, and a cost at least the mass-weighted mean of csc_s. Then t∗t_* does not increase, where t∗=0t_*=0 when ζ′≤0ζ ≤ 0, the max-min value of (i) in that case because then p∈p . Proof. (i) Since min1,ps+γs=ps+minγs,1−ps \1,p_s+ _s\=p_s+ \ _s,1-p_s\, the live harm allowed by p^=p p=p is q+ξq+ξ. If ξ>ζξ>ζ, the world with p^=p p=p, p0s=min1,ps+γsp_0s= \1,p_s+ _s\, and the record law of W1W_1 given harm is in the null and gives the log and every executed record the laws they have in W1W_1, so the power is at most the size. If ξ=ζξ=ζ, then q+ξ=q⋆<q0+mq+ξ=q <q_0+m, so some stratum s′s has ps′+γs′<1p_s + _s <1. For small ε>0 >0, raise only p^s′ p_s to ps′+εp_s + and keep p0s=min1,p^s+γsp_0s= \1, p_s+ _s\ and the record law of W1W_1 given harm; the live harm is q⋆+ws′εq +w_s . The coupling of Proposition F.8.1(i) changes at most n outcomes, each with probability at most ε , and ε↓0 0 bounds the power by the size. For the second claim, let q0=0q_0=0, w=(1/2,1/2)w=(1/2,1/2), p=(0.95,0.05)p=(0.95,0.05), γ=(0.2,0)γ=(0.2,0), and q⋆=0.58q =0.58. Then ∑swsγs=0.10>ζ=0.08 _sw_s _s=0.10>ζ=0.08, but ξ=0.025ξ=0.025, and every world of the null has p^2>0.16 p_2>0.16 because p01≤1p_01≤ 1. With n=4,000n=4,000, a test that executes 1,000 episodes of stratum 2 when the log holds that many, and certifies when at most 105 are harmful, has size below e−2⋅1000⋅0.0552<0.0024e^-2· 1000· 0.055^2<0.0024 and failure probability below e−2⋅1000⋅0.0562+e−500<0.0024e^-2· 1000· 0.056^2+e^-500<0.0024 (Hoeffding). (i) and (i) Setting rs=psr_s=p_s off J and replacing rsr_s by min1−γs,maxps,rs \1- _s, \p_s,r_s\\ on J keep r in A and raise no objective. So the inner problems run over ps≤rs≤1−γsp_s≤ r_s≤ 1- _s on J with ∑s∈Jws(rs−ps)≥ζ′ _s∈ Jw_s(r_s-p_s)≥ζ . Each bs(t)−psb_s(t)-p_s is continuous and nondecreasing from 00, and strictly increasing until it reaches 1−γs−ps1- _s-p_s. The total capacity ∑s∈Jws(1−γs−ps) _s∈ Jw_s(1- _s-p_s) equals q0+m−q−ξq_0+m-q-ξ and exceeds ζ′ζ . So t∗t_* exists, is unique, and leaves J∗J_* nonempty, and p¯ p meets the constraint with equality. Let r∈r . Strata outside J∗J_* contribute wsw_s to the live harm at p¯ p, the most they can, so ∑s∈J∗ws[min1,rs+γs−(p¯s+γs)]≥0 _s∈ J_*w_s[ \1,r_s+ _s\-( p_s+ _s)]≥ 0, and the bracket is at most rs−p¯sr_s- p_s; this is the last claim of (i). Every stratum has kl(ps,p¯s)≤cst∗kl(p_s, p_s)≤ c_st_*, with equality on J∗J_*, so maxskl(ps,p¯s)/cs=t∗ _skl(p_s, p_s)/c_s=t_* and every λ has inner value at most t∗t_*. Convexity of kl(ps,⋅)kl(p_s,·) and λs∗gs/cs=asgs/c¯∝wsλ^*_sg_s/c_s=a_sg_s/ c w_s on J∗J_* give, for r∈r , ∑sλs∗cskl(ps,rs) _s λ^*_sc_skl(p_s,r_s) ≥∑s∈J∗asc¯cst∗+gs(rs−p¯s) ≥\ _s∈ J_* a_s c\c_st_*+g_s(r_s- p_s)\ ≥t∗, ≥\ t_*, so λ∗λ^* has inner value t∗t_*, and maxskl(ps,rs)/cs≥t∗ _skl(p_s,r_s)/c_s≥ t_* on A. This proves (i) without exchanging the maximum and the infimum. For (i), take r with strict inequality in A and 0<rs<10<r_s<1, and the world of the null with p^=r p=r, p0s=min1,rs+γsp_0s= \1,r_s+ _s\, and the record law of W1W_1 given harm. An execution in stratum s contributes relative entropy kl(ps,rs)kl(p_s,r_s), and Lemma 1 of Kaufmann et al. (2016), applied as in Proposition F.8.1(i), gives ∑sW1[Ks]kl(ps,rs)≥kl(1−β,α) _sE_W_1[K_s]\,kl(p_s,r_s) (1-β,α). With B=W1[C]B=E_W_1[C] and λs=csW1[Ks]/B _s=c_sE_W_1[K_s]/B, this reads B∑sλskl(ps,rs)/cs≥kl(1−β,α)B _s _skl(p_s,r_s)/c_s (1-β,α). Points p¯+δJ∗ p+ 1_J_* are such r for small δ>0δ>0, so letting δ↓0δ 0 gives Bmaxskl(ps,p¯s)/cs≥kl(1−β,α)B _skl(p_s, p_s)/c_s (1-β,α), that is, Bt∗≥kl(1−β,α)B\,t_* (1-β,α). (iv) For small ζ′ζ , no coordinate reaches 1−γs1- _s; Taylor expansion of binary relative entropy in (17) and as∝ws/gsa_s w_s/g_s gives both limits. With S=1S=1 and c1=1c_1=1, the setting’s q⋆<q0+mq <q_0+m gives ζ<m(1−p)ζ<m(1-p), so ξ=mminγ,1−p≥ζξ=m \γ,1-p\≥ζ exactly when mγ≥ζmγ≥ζ. If mγ<ζmγ<ζ, then ξ=mγξ=mγ, the root of (17) is p¯1=p+(ζ−mγ)/m p_1=p+(ζ-mγ)/m, and t∗=kl(p,p¯)t_*=kl(p, p). For pooling, choose λs∝wscs _s w_sc_s in (i). Joint convexity gives ∑s(ws/m)kl(ps,rs)≥kl(ppool,∑swsrs/m) _s(w_s/m)kl(p_s,r_s) (p_pool, _sw_sr_s/m), where feasibility ensures ∑swsrs/m≥ppool+(ζ−∑swsγs)/m>ppool _sw_sr_s/m≥ p_pool+(ζ- _sw_s _s)/m>p_pool; monotonicity gives the bound. (v) The claim is immediate if the merged t∗=0t_*=0. Otherwise split the optimal share of merged stratum ι as λs=λι′wscs/∑j∈Iwjcj _s=λ _ w_sc_s/ _j∈ Iw_jc_j. Map feasible r to r′r by mass-weighted averaging on I; concavity of min1,⋅ \1,·\ preserves feasibility. Joint convexity and the cost condition give ∑s∈Iλskl(ps,rs)/cs≥λι′kl(pι,rι′)/cι _s∈ I _skl(p_s,r_s)/c_s≥λ _ kl(p_ ,r _ )/c_ , so (i) bounds the split value below by the merged value. ∎ Achievability. The stratified execution test with levels α,β′∈(0,1)α,β ∈(0,1) draws stratum s∈J∗s∈ J_* with probability asa_s, independently of the past, executes an unused unresolved episode, and reads its harm bit Y. Like the test of Proposition F.8.2, it uses p and the log’s masses. Starting at Ξ0=0 _0=0, each draw adds score Ylog(ps/p¯s)+(1−Y)up(ps,p¯s)Y (p_s/ p_s)+(1-Y)\,up(p_s, p_s). The test certifies when Ξt≥log(1/α) _t≥ (1/α), and stops without certifying when Ξt≤−log(1/β′) _t≤- (1/β ) or the drawn stratum pool is exhausted. Set u¯=maxs∈J∗up(ps,p¯s) u= _s∈ J_*up(p_s, p_s), K¯=log(1/α)+u¯/(t∗c¯) K=\ (1/α)+ u\/(t_* c), and χn=∑s∈J∗2asK¯/(wsn)+e−ws2n/2 _n= _s∈ J_*\2a_s K/(w_sn)+e^-w_s^2n/2\. Proposition F.9.2 (Execution across Strata: Achievability and Live Crossover). Assume the setting of Proposition F.9.1 with ζ′>0ζ >0. (i) For every log, every restored vector in A, and every record law given harm, the test certifies with probability at most α. This also holds when the design point is computed from design values p~∈(0,1)S p∈(0,1)^S in place of p, provided ζ′>0ζ >0 at p~ p, since A does not involve p. (i) With unlimited pools, at W1W_1 the test stops at the lower threshold with probability at most β′β , uses W1[τ]≤K¯E_W_1[τ]≤ K draws, and costs W1[C]≤log(1/α)+u¯/t∗E_W_1[C]≤\ (1/α)+ u\/t_*. With the pools of a log of n episodes, its power is at least 1−β′−χn1-β - _n and the cost bound holds. (i) Let CexC_ex be the least W1[C]E_W_1[C] over valid and powerful procedures, and ClvC_lv the least expected cost, at cLc_L per episode, of the live tests of Proposition F.8.1(i). If χn<β _n<β, then kl(1−β,α)/t∗≤Cex≤log(1/α)+u¯/t∗kl(1-β,α)/t_*≤ C_ex≤\ (1/α)+ u\/t_*. As α,β↓0α,β 0 with χn<β _n<β, Cex/Clv→kl(q,q⋆)/(cLt∗)C_ex/C_lv (q,q )/(c_Lt_*). So executing the unresolved continuations is cheaper to first order exactly when t∗>tL=kl(q,q⋆)/cLt_*>t_L=kl(q,q )/c_L, that is, when the left side of (17) at tLt_L is below ζ′ζ . Proof. Use the score identities and SPRT argument of Proposition F.8.2, with (a,c)=(ps,p¯s)(a,c)=(p_s, p_s) in stratum s. (i) Given the log, past, and stratum s, the bit is Bernoulli(p^s)( p_s) whatever its record law. For p^∈ p , Proposition F.9.1(i) and asgs∝wsa_sg_s w_s give [eZt∣past]=1−∑s∈J∗asgs(p^s−p¯s)≤1E[e^Z_t ]=1- _s∈ J_*a_sg_s( p_s- p_s)≤ 1. Extend each pool by independent Bernoulli(p^s)( p_s) bits; finite-pool certification requires the unlimited supermartingale eΞte _t to cross 1/α1/α. Ville’s inequality gives size at most α, also for p~ p, since the argument uses only the design point’s properties relative to A. (i) At W1W_1, the mean score is t∗c¯t_* c and upper overshoot is at most u¯ u. The same SPRT argument gives lower-exit probability at most β′β , [τ]≤K¯E[τ]≤ K, and mean cost c¯[τ] cE[τ]. Wald’s identity gives mean draws as[τ]≤asK¯a_sE[τ]≤ a_s K in stratum s. The same Markov and Hoeffding bounds, summed over strata, bound exhaustion by χn _n; together with lower exit this gives the power, while exhaustion only reduces cost. (i) Combine Proposition F.9.1(i) with (i) and (i), taking β′=β−χnβ =β- _n, for the execution bounds. The live bounds of Propositions F.8.1(i) and F.8.2(i), and kl(1−β,α)/log(1/α)→1kl(1-β,α)/ (1/α)→ 1, give the cost ratio. Strict increase of the left side of (17) on [0,t∗][0,t_*] gives the crossover equivalence. ∎ Remark F.9.3 (Allocation, Pools, and Snapshots). The shares a are part of the test’s validity, not only of its cost. In the instance of checks/verify_budget_strata.py, the same increments with draws in proportion to wsw_s have a per-draw mean of eZe^Z above one at a boundary point of A, and their size there is about 0.15 at α=0.05α=0.05. Design values p~∈(0,1)S p∈(0,1)^S from a pilot on separate episodes, such as smoothed proportions, keep the size at α by part (i), with no certification when ζ′≤0ζ ≤ 0 at p~ p; we do not analyze the cost of such an adaptive rule (Garivier and Kaufmann, 2016, compare). The bounds concern population harm under independent outcomes, with power at exact restoration; fixed-cohort harm fractions require a sampling design such as Proposition F.7.1. Power at every approximately restored law is not guaranteed. With q0q_0 and w estimated, replacing them in A by simultaneous upper confidence limits of level αlog _ enlarges A on the event of the limits. Running the test only when q0U+∑swsUmin1,p~s+γs<q⋆<q0U+∑swsUq_0^U+ _sw_s^U \1, p_s+ _s\<q <q_0^U+ _sw_s^U for these limits q0Uq_0^U and wUw^U, and otherwise not certifying, keeps the size at most α+αlogα+ _ , as in Remark F.8.4. Runs from an earlier snapshot re-execute the agreeing steps (Remark F.10.2). Suppose they reach the first-deviation strata of a set I with probabilities ws/∑j∈Iwjw_s/ _j∈ Iw_j in every world, with the same restored harm laws and admissible rates; that their records can be simulated from the stratum and one restored harm bit by a randomization that does not depend on the world; and that they cost at least the mean cost of runs started at those deviations. Then data processing and the share splitting of Proposition F.9.1(v) show that restoring at the first deviations of Proposition F.10.1 never raises the bound of part (i). The comparison does not cover earlier runs that observe more, restore differently, or route differently, and choosing coarser snapshots trades storage against the bound, which we do not solve. Related Tests. With unit costs and no restoration error, A is a half-space of mean vectors, and the saddle point of Proposition F.9.1(i) is the half-space case of Juneja and Krishnasamy (2019, Theorem 5), whose least favorable alternative also equalizes the divergences. Multi-fidelity best-arm identification pairs cheaper samples of known maximal bias with their costs (Poiani et al., 2024). Stratified sequential audits permit arbitrary stratum selection (Spertus and Stark, 2022; Spertus et al., 2024); this likelihood-ratio test requires its design shares. F.10 Snapshot Design for a Family of Gates This proves the snapshot-design claim of Section 3.4. Setting and Evidence. We adopt the framework of Appendix E.2 with query X=ϕ(L)X=φ(L) and pre-intervention record r, where f0f^0 executes each call. Decisions represent steps in the demonstrations; gates acting on each call treat calls as decisions (via the refined clock of Appendix A.1). Let m(h)=mt(h)m(h)=m_t(h) be the score in I(h)I(h), and m¯(h) m(h) the maximal score over previous decision histories h′≺h h with t(h′)≥st(h )≥ s for boundary step s (−∞-∞ if none). The retry gate κθ _θ of Section 2.2 replaces the call by a refusal aθ(i)≠f0(i)a_θ(i)≠ f^0(i) when t≥st≥ s and m(i)>θm(i)>θ. A refusal at final step T constitutes an abort, as no decision history follows (Appendix E.2). At each step t<Tt<T, a decision history follows the refusal. Write wh=P0([h]∣r)w_h=P^0([h] r), κ+=κcont(r,P0)D^+_κ=D^cont_κ(r,P^0), and Qhκ=ϕ#Pκ(L∈⋅∣[h])Q^κ_h= _\#P^κ(L∈· [h]) for h∈κ+h ^+_κ. Feasible set hκX^κ_h follows Appendix E.1 for gate κ, depending on κ via subsequent refusals. A history h∈κ+h ^+_κ is open for κ when |hκ|≥2|X^κ_h|≥ 2 and closed otherwise (for instance, when X is the harm indicator and harm accrued before h). Let κO_κ collect histories open for κ. A set S of logged decision histories h with [h]⊆Ωr[h] _r and P0([h])>0P^0([h])>0 stores first-deviation snapshots. For h∈h and gate κ with h∈κ+h ^+_κ, the evaluator restores at hκ+h^+_κ and executes the continuation. Assumption (T) equates this continuation law with QhκQ^κ_h, estimated by finite executions (Proposition F.7.1). Earlier runs re-execute agreeing steps as partial live runs (Remark F.10.2). Condition (U) of Section 3.4 admits arbitrary response laws at inputs of zero baseline probability, taking model class ℳfullM_full from Lemma E.4.2. Its mechanisms satisfy (R) and (A1) to (A3), with unreplaced kernels reading the full history, so (G1) fails at refusal inputs. The proof of (c) does not require realizability. Proposition F.10.1 (Snapshots for a Threshold Family). In (a) and (b), let h be a decision history with s≤t(h)<Ts≤ t(h)<T, [h]⊆Ωr[h] _r, and P0([h])>0P^0([h])>0. (a) h∈κθ+h ^+_ _θ exactly when m¯(h)≤θ<m(h) m(h)≤θ<m(h), so h is a first deviation for some θ∈Θθ∈ exactly when Θ∩[m¯(h),m(h))≠∅ ∩[ m(h),m(h))≠ . (b) For Θ=[θmin,1) =[ _ ,1), this means m(h)>maxθmin,m¯(h)m(h)> \ _ , m(h)\, a running maximum above θmin _ , and the gates θ∈[maxθmin,m¯(h),m(h))θ∈[ \ _ , m(h)\,m(h)) deviate at h. Ties and a score equal to θmin _ give no running maximum, and a score of 11 is one exactly when all earlier scores since s are below 11. For a finite Θ=θ1<⋯<θn =\ _1<…< _n\, the condition is B(m(h))>B(m¯(h))B(m(h))>B( m(h)) with B(x)=#i:θi<xB(x)=\#\i: _i<x\, and an episode has at most n first deviations. (c) Assume (R), (A1) to (A3), (U), and (T). Given first-deviation snapshots S, the identified set of ϕ#Pκ(L∈⋅∣r) _\#P^κ(L∈· r) is ν+∑u∈κ+∩wuQuκ+∑u∈κ+∖wuQu:Qu∈Δ(uκ)\ν+ _u ^+_κ w_uQ^κ_u+ _u ^+_κ w_uQ_u:Q_u∈ (X^κ_u)\ (ν as in Proposition E.4.3). It is a singleton exactly when κ⊆O_κ ; otherwise, for binary X, the set for Pκ(X=1∣r)P^κ(X=1 r) has width ∑u∈κ∖wu _u _κ w_u. So S identifies every κθ _θ, θ∈Θθ∈ , exactly when it contains ⋃θκθ _θO_ _θ, the least such set. For [θmin,1)[ _ ,1), these are the running maxima above θmin _ at steps t<Tt<T that are open for some gate deviating there. Proof. (a) This is the first-deviation condition by definition, with continuation because t(h)<Tt(h)<T. (b) Intersecting [m¯(h),m(h))[ m(h),m(h)) with Θ gives the stated cases. For finite Θ , B(m)−B(m¯)B(m)-B( m) counts the available thresholds, and each threshold has at most one first deviation per episode. (c) By Proposition E.4.3, a compatible model has law ν+∑uwuQuMν+ _uw_uQ^M_u with QuM∈Δ(uκ)Q^M_u∈ (X^κ_u), and (T) fixes QuM=QuκQ^M_u=Q^κ_u for u∈κ+∩u ^+_κ . Conversely, let M∗∈ℳfullM^* _full generate the evidence and fix Qu∈Δ(uκ)Q_u∈ (X^κ_u) for u∈κ+∖u ^+_κ . For each x∈uκx ^κ_u, take a replacement-consistent extension ωx _x of uκ+u^+_κ with ϕ(ℓ(ωx))=xφ( ( _x))=x. By (U), set the kernels inside [uκ+][u^+_κ] to the conditional laws of ∑xQu(x)δωx _xQ_u(x) _ _x. These cylinders are P0P^0-null, so kernels set inside them do not enter the baseline law, which the modification therefore preserves. They are disjoint from [gκ′+][g^+_κ ] for every gate κ′κ of the family and every g∈∩κ′+g ^+_κ or terminal g of positive mass. If u≠gu≠ g and they meet, one of u,gu,g extends a deviating output of the other, which has baseline probability zero. A terminal g=ug=u has an abort output, whereas uκ+u^+_κ continues. Thus the modification also preserves the stored laws and the valuations of (A3), and attains the chosen law. The set is a constant plus wuΔ(uκ)w_u (X^κ_u) for each u∉u , which gives the singleton criterion and the width. ∎ Remark F.10.2 (Broader Evidence). The least-set claim concerns restoration at the first deviation of each gate. Suppose instead that S holds logged decision histories g with [g]⊆Ωr[g] _r and P0([g])>0P^0([g])>0. Assume that (T) links a run of κ from g to the changed system only for gates that reach g, those that agree with f0f^0 at every earlier decision. Such a run re-executes the agreeing steps below g, and its law determines only the sum ∑h⪰gwhQhκ _h gw_hQ^κ_h over the first deviations h of κ below g, up to known terms. Under the other assumptions of (c), κ is then identified exactly when each h∈κh _κ has an ancestor-or-self in S, by the proof of (c). Minimal sets are then not unique. With the trivial record and a decision at step 00 on every path, storing every step-00 history (the live-run cover) identifies every gate with no snapshot at a running maximum. Re-executing every agreeing step is the price. The claim above is the least set of first-deviation snapshots. Appendix G Proofs: Component Evidence and Composition This appendix proves Proposition G.1.1, used in Sections 3.5 and 3.6. G.1 Statement Section 3.5 states this result in words. Fix a target composition and scheduler, with shared state S∼PSS P_S, component losses LiL_i with conditional laws Fi(⋅∣s)F_i(· s), and declared joint loss L=h(S,L1,…,Ln)L=h(S,L_1,…,L_n); write pi(s)=Fi(Bi∣s)p_i(s)=F_i(B_i s). Section G.2 makes these objects precise. Proposition G.1.1 (Component evidence to joint risk). (i) If L1,…,LnL_1,…,L_n are mutually conditionally independent given S (CI), the law of (S,L1,…,Ln)(S,L_1,…,L_n) is PS(ds)∏iFi(dli∣s)P_S(ds) _iF_i(dl_i s), and the law of L is its image under h. (i) Let the evidence be PSP_S and the FiF_i, as from separate component logs that each carry S, with no restriction on dependence given S (NR). Then P(L1∈B1,L2∈B2)P(L_1∈ B_1,L_2∈ B_2) takes exactly the values in [∫(p1+p2−1)+dPS,∫min(p1,p2)dPS] [ (p_1+p_2-1)_+\,dP_S,\ (p_1,p_2)\,dP_S ]. (i) Records linking S and every LiL_i within each episode identify the law of (S,L1,…,Ln)(S,L_1,…,L_n), hence every query of L. Under (NR), separate logs of each (S,Li)(S,L_i) identify that law if and only if, at each state of positive probability, at most one Fi(⋅∣s)F_i(· s) is not a point mass. Records of S alone identify only PSP_S in the family of Lemma G.3.2. (iv) Standalone runs of component i identify Fi(⋅∣s)F_i(· s) when the composition’s state law is known (Known PSP_S), the conditional law of LiL_i given S is the same in standalone runs and in the composition (Invi), and every composed state occurs in standalone runs (Suppi). In a family that does not tie the composed component to its standalone run, the standalone law of (S,Li)(S,L_i) places no restriction on FiF_i. Without (Suppi), let component i read only S and private randomness, and let UiU_i hold the composed states never seen in isolation. For ∅≠B⊊i ≠ B _i, the identified set of P(Li∈B)P(L_i∈ B) is then an interval of width PS(Ui)P_S(U_i), and other restrictions on component i can narrow it. Parts (i) to (i) restate conditional independence, Fréchet bounds given S (Fréchet, 1951; Nelsen, 2006), and linked-record identification; part (iv) gives transportability with overlapping support (Pearl and Bareinboim, 2011). G.2 Finite Setting and Composition Interfaces This setting supplies the objects and assumptions for Proposition G.1.1 (Section 3.5). A composition declares interfaces, a scheduler, compatible kernels, and joint loss map h:×1:n→⊂ℝmh:S×L_1:n ^m. This defines joint specification ℜjoint=(Ejoint,ℓjoint,Kjoint,joint) R_joint=(E_joint, _joint,K_joint,C_joint) with law P on finite trajectory space Ω . Shared state is a declared map S:Ω→S: , with finite S. Component i∈1,…,ni∈\1,…,n\ has loss map Li:Ω→iL_i: _i with finite iL_i. Write =(L1,…,Ln)∈1:nL=(L_1,…,L_n) _1:n, consequence map ℓjoint=h∘(S,) _joint=h (S,L), and full-episode loss L=h(S,)L=h(S,L). Let ΛP(s,)=P(S=s,=) _P(s,l)=P(S=s,L=l) be the law of (S,)(S,L), with state marginal PS(s)=∑ΛP(s,)P_S(s)= _l _P(s,l), support +=s:PS(s)>0S_+=\s:P_S(s)>0\, and conditional laws Fi(l∣s)=P(Li=l∣S=s)F_i(l s)=P(L_i=l S=s) for s∈+s _+. For events Bi⊆iB_i _i, write Ei=Li∈BiE_i=\L_i∈ B_i\ and pi(s)=Fi(Bi∣s)p_i(s)=F_i(B_i s). The product law is Λ⊗(s,)=PS(s)∏i=1nFi(li∣s). (s,l)=P_S(s) _i=1^nF_i(l_i s). (18) For component i, standalone deployment is a mechanism with law PisaP^sa_i yielding evidence Q(i)=ℒPisa(S,Li)Q^(i)=L_P^sa_i(S,L_i), state marginal QS(i)Q^(i)_S, and support isa=s:QS(i)(s)>0S^sa_i=\s:Q^(i)_S(s)>0\. The model family ℳ0M_0 contains finite composition mechanisms under the scheduler, with true mechanism M⋆∈ℳ0M _0 having PM⋆=P_M =P and ΛM⋆=ΛP _M = _P. Identified sets are Θe(θ)=θ(M):M∈ℳ0,e(M)=e(M⋆) _e(θ)=\θ(M):M _0,\ e(M)=e(M )\. Evidence maps are linked records elink(M)=ℒPM(S,)e_link(M)=L_P_M(S,L), paired records epair(M)=(ℒPM(S,L1),…,ℒPM(S,Ln))e_pair(M)=(L_P_M(S,L_1),…,L_P_M(S,L_n)), and state records eS(M)=ℒPM(S)e_S(M)=L_P_M(S). Definition G.2.1 (Coupling set). Γ=Γ(PS,F1,…,Fn) = (P_S;F_1,…,F_n) is the set of probability laws Λ on ×1:nS×L_1:n such that, for every s∈s , every i, and every l∈il _i, ∑:li=lΛ(s,)=PS(s)Fi(l∣s). _l:\,l_i=l (s,l)=P_S(s)\,F_i(l s). Summing over l shows every Λ∈Γ ∈ has state marginal PSP_S, and for each s∈+s _+, πs=Λ(s,⋅)/PS(s) _s= (s,·)/P_S(s) couples F1(⋅∣s),…,Fn(⋅∣s)F_1(· s),…,F_n(· s); thus Λ⊗,ΛP∈Γ , _P∈ . Definition G.2.2 (Assumptions). (CI) L1,…,LnL_1,…,L_n are mutually conditionally independent given S under P: P(=∣S=s)=∏iFi(li∣s)P(L=l S=s)= _iF_i(l_i s) for every s∈+s _+ and every l. (NR) No dependence restriction: Γ(PS,F1,…,Fn)⊆ΛM:M∈ℳ0 (P_S;F_1,…,F_n) \ _M:M _0\. (Known PSP_S) The shared-state law of the target composition is available, from logged S in that composition or from its declared scheduler and upstream kernels. (Invi) There is a kernel GiG_i from S to iL_i with Fi(⋅∣s)=Gi(⋅∣s)F_i(· s)=G_i(· s) for every s∈+s _+ and Q(i)(Li∈⋅∣S=s)=Gi(⋅∣s)Q^(i)(L_i∈· S=s)=G_i(· s) for every s∈isas ^sa_i. (Suppi) +⊆isaS_+ ^sa_i. G.3 Lemmas These lemmas support the proof of Proposition G.1.1 (Section 3.5). Lemma G.3.1 (Paired evidence fixes exactly the coupling set). For M∈ℳ0M _0, epair(M)=epair(M⋆)e_pair(M)=e_pair(M ) if and only if ΛM∈Γ(PS,F1,…,Fn) _M∈ (P_S;F_1,…,F_n), where PSP_S and the FiF_i are those of M⋆M . Proof. The marginal conditions ℒPM(S,Li)(s,l)=∑:li=lΛM(s,)=PS(s)Fi(l∣s)L_P_M(S,L_i)(s,l)= _l:\,l_i=l _M(s,l)=P_S(s)F_i(l s) for all i,s,li,s,l define Γ . ∎ Lemma G.3.2 (Realization by an unlogged shared input). Let ℳ0WM_0^W be the family of mechanisms in which a shared-state kernel draws S, an unlogged exogenous input V on a finite set is drawn from a kernel given S, and each component i, in the scheduled order, outputs Li=ki(S,V)L_i=k_i(S,V) for a deterministic map kik_i. Every law Λ on ×1:nS×L_1:n is ΛM _M for some M∈ℳ0WM _0^W. In particular ℳ0WM_0^W satisfies (NR) at every (PS,F1,…,Fn)(P_S,F_1,…,F_n). Proof. Draw S∼ΛS _S, draw V∼Λ(⋅∣S)V (· S), and set ki(s,)=vik_i(s,v)=v_i. ∎ Lemma G.3.3 (When the coupling set is a point). Γ is a singleton if and only if, for every s∈+s _+, at most one of F1(⋅∣s),…,Fn(⋅∣s)F_1(· s),…,F_n(· s) is not a point mass. Proof. If at most one margin is non-degenerate at each s∈+s _+, the marginal constraints uniquely fix Λ(s,⋅) (s,·). Otherwise, choose two distinct positive-mass values in each of two non-degenerate margins at some s∈+s _+, and fix positive-mass values in all other margins. The four resulting cells have positive mass under ∏iFi(⋅∣s) _iF_i(· s). Add ϵ>0ε>0 to the two diagonal cells and subtract it from the other two, with ϵε smaller than their masses. This preserves every margin and non-negativity; multiplying by PS(s)P_S(s) and leaving other states unchanged gives a second member of Γ . ∎ G.4 Proofs of Proposition G.1.1 Parts (i) to (iv) Proof of Part (i). For s∈+s _+ and l, conditional probability and (CI) give ΛP(s,)=PS(s)∏iFi(li∣s)=Λ⊗(s,) _P(s,l)=P_S(s) _iF_i(l_i s)= (s,l), vanishing outside +S_+. Because L=h(S,)L=h(S,L), ℒP(L)=h#Λ⊗L_P(L)=h_\# , so every query of L is a function of (PS,F1,…,Fn)(P_S,F_1,…,F_n). Paired records cannot test (CI) because Λ⊗∈Γ ∈ and part (i)(b) shows they exclude no element of Γ under (NR). Remark G.4.1 (Sub-parts of part (i)). Let β−(s)=(p1(s)+p2(s)−1)+β^-(s)=(p_1(s)+p_2(s)-1)_+ and β+(s)=min(p1(s),p2(s))β^+(s)= (p_1(s),p_2(s)) for s∈+s _+. For a function β on +S_+, write β¯=∑sPS(s)β(s) β= _sP_S(s)β(s); in particular β¯−=∑sPS(s)β−(s) β^-= _sP_S(s)β^-(s) and β¯+=∑sPS(s)β+(s) β^+= _sP_S(s)β^+(s). (a) Every Λ∈Γ ∈ , in particular ΛP _P, satisfies β−(s)≤Λ(E1∩E2∣S=s)≤β+(s)β^-(s)≤ (E_1∩ E_2 S=s)≤β^+(s) for s∈+s _+, and β¯−≤Λ(E1∩E2)≤β¯+ β^-≤ (E_1∩ E_2)≤ β^+. (b) Under (NR), Θepair(P(E1∩E2))=[β¯−,β¯+] _e_pair(P(E_1∩ E_2))=[ β^-, β^+]. (c) (P(E1)+P(E2)−1)+≤β¯−(P(E_1)+P(E_2)-1)_+≤ β^- and β¯+≤min(P(E1),P(E2)) β^+≤ (P(E_1),P(E_2)). (d) Under (NR), the identified set for the law of L under paired records is ℋ=h#Λ:Λ∈ΓH=\h_\# : ∈ \, and that of a query (ϕ,ρ)(φ,ρ) is ρ(ϕ#ν):ν∈ℋ\ρ( _\#ν):ν \. If n=2n=2 and h(s,l1,l2)=h¯(B1(l1),B2(l2))h(s,l_1,l_2)= h(1_B_1(l_1),1_B_2(l_2)) does not depend on s, each element h#Λh_\# of ℋH depends on Λ only through β¯=Λ(E1∩E2) β= (E_1∩ E_2), which ranges over [β¯−,β¯+][ β^-, β^+]. Proof of Part (i). (a) At each s∈+s _+, apply the Fréchet bounds (Fréchet, 1951), in Nelsen (2006, Theorem 2.2.3 and Eq. (2.5.1)), to 1−B1(L1)1-1_B_1(L_1) and 1−B2(L2)1-1_B_2(L_2) conditionally on S=sS=s, evaluating their joint CDF at (0,0)(0,0). These finite conditional laws have CDF values p1(s),p2(s)p_1(s),p_2(s) there, giving β±(s)β^±(s); averaging gives β¯± β^±. (c) follows by summing (x)+≥x,0(x)_+≥ x,0 and min(x,y)≤x,y (x,y)≤ x,y against PSP_S. (b) The bounds in Nelsen’s Eq. (2.5.1) are themselves joint CDFs, including for discrete margins. Mix the two endpoint indicator couplings with a common weight λ∈[0,1]λ∈[0,1] at every s. Lift each positive indicator cell to the full losses by taking the product of the Fi(⋅∣s)F_i(· s) conditioned on that cell’s indicators; positive cell mass ensures these conditional laws exist. Give components i≥3i≥ 3 their independent margins. This yields a member of Γ with intersection mass (1−λ)β¯−+λβ¯+(1-λ) β^-+λ β^+. By (NR) and Lemma G.3.1, each such coupling has a compatible mechanism, proving sharpness and every intermediate value. (d) By Lemma G.3.1 and (NR), the consistent (S,)(S,L)-laws form exactly Γ , and ℒ(L)=h#ΛL(L)=h_\# . Let n=2n=2 and let h¯ h be an indicator map that does not depend on s. The law of (B1(L1),B2(L2))(1_B_1(L_1),1_B_2(L_2)) under Λ∈Γ ∈ has the fixed margins P(E1)P(E_1) and P(E2)P(E_2) and joint cell β¯=Λ(E1∩E2) β= (E_1∩ E_2). Hence h#Λh_\# depends on Λ only through β¯ β, which ranges over [β¯−,β¯+][ β^-, β^+] by (b). Proof of Part (i). (a) Linked records log (S,)(S,L) jointly, so in every family elink(M)=elink(M⋆)e_link(M)=e_link(M ) implies ΛM=ΛP _M= _P, which identifies every query of L through ℒP(L)=h#ΛPL_P(L)=h_\# _P. (b) By Lemma G.3.1, Θepair(Λ)=ΛM:M∈ℳ0∩Γ _e_pair( )=\ _M:M _0\∩ , which equals Γ under (NR). (c) eS(M)e_S(M) is the state marginal of each component of epair(M)e_pair(M), so Θepair(Λ)⊆ΘeS(Λ) _e_pair( ) _e_S( ). The family ℳ0WM_0^W of Lemma G.3.2 realizes every law with state marginal PSP_S and satisfies (NR). In it, eS(M)=eS(M⋆)e_S(M)=e_S(M ) holds exactly when ΛM _M has state marginal PSP_S, and two elements ≠′l of 1:nL_1:n give the distinct members ∑sPS(s)δ(s,) _sP_S(s) _(s,l) and ∑sPS(s)δ(s,′) _sP_S(s) _(s,l ), so records of S alone identify only PSP_S. (d) Lemma G.3.3 combined with (b) shows that, under (NR), paired records identify ΛP _P exactly when, for every s∈+s _+, at most one Fi(⋅∣s)F_i(· s) is not a point mass. Remark G.4.2 (Sub-parts of part (iv)). Assume (Known PSP_S). (a) Under (Invi) and (Suppi), Fi(⋅∣s)=Q(i)(Li∈⋅∣S=s)F_i(· s)=Q^(i)(L_i∈· S=s) for every s∈+s _+. If this holds for every i, then under (CI) the law of L is h#Λ⊗h_\# computed from standalone evidence and PSP_S, and without (CI) the bounds of Remark G.4.1(a) hold with these FiF_i. (b) Let Ui=+∖isaU_i=S_+ ^sa_i, and let ℳ0tr,iM_0^tr,i be the family of pairs of a composition and a standalone deployment in which component i is one kernel Gi(⋅∣S)G_i(· S), reading only S and private randomness in both, with GiG_i arbitrary, composition state law PSP_S, and standalone state law QS(i)Q^(i)_S. In this family (Invi) holds, and for every B with ∅≠B⊊i ≠ B _i, the identified set of P(Li∈B)P(L_i∈ B) given Q(i)Q^(i) and PSP_S is [cB,cB+PS(Ui)],cB=∑s∈+∖UiPS(s)Q(i)(Li∈B∣S=s). gathered [c_B,\ c_B+P_S(U_i) ],\\ c_B= _s _+ U_iP_S(s)\,Q^(i)(L_i∈ B S=s). gathered It is a singleton if and only if (Suppi) holds. (c) Without (Invi), Q(i)Q^(i) places no restriction on FiF_i: for every family of laws (Fi′(⋅∣s))s∈+(F _i(· s))_s _+ on iL_i, some composition with state law PSP_S has these conditional laws while its standalone deployment has evidence Q(i)Q^(i). Proof of Part (iv). (a) Under (Suppi), each s∈+s _+ lies in isaS^sa_i, so (Invi) gives Fi(⋅∣s)=Gi(⋅∣s)=Q(i)(Li∈⋅∣S=s)F_i(· s)=G_i(· s)=Q^(i)(L_i∈· S=s). With (Known PSP_S), Λ⊗ is computable, part (i) gives ℒP(L)=h#Λ⊗L_P(L)=h_\# under (CI), and Remark G.4.1(a) applies without (CI) because it uses only membership in Γ . (b) Component i reads only S and private randomness in both deployments, so (Invi) holds in ℳ0tr,iM_0^tr,i. For s∈+∖Uis _+ U_i, (Invi) fixes Fi(B∣s)=Q(i)(Li∈B∣S=s)F_i(B s)=Q^(i)(L_i∈ B S=s), contributing cBc_B, while Gi(B∣s)G_i(B s) is unconstrained in [0,1][0,1] on UiU_i, so P(Li∈B)=cB+∑s∈UiPS(s)Gi(B∣s)∈[cB,cB+PS(Ui)]P(L_i∈ B)=c_B+ _s∈ U_iP_S(s)G_i(B s)∈[c_B,c_B+P_S(U_i)]. For attainment, fix xin∈Bx_in∈ B and xout∉Bx_out∉ B, set Gi(⋅∣s)=Q(i)(Li∈⋅∣S=s)G_i(· s)=Q^(i)(L_i∈· S=s) on isaS^sa_i and λδxin+(1−λ)δxoutλ _x_in+(1-λ) _x_out on UiU_i; the standalone deployment that draws S from QS(i)Q^(i)_S then has record law Q(i)Q^(i), and the composition gives cB+λPS(Ui)c_B+λ P_S(U_i) for λ∈[0,1]λ∈[0,1]. Since PS>0P_S>0 on UiU_i, the interval is a singleton if and only if Ui=∅U_i= , which is (Suppi). (c) A standalone deployment that draws S from QS(i)Q^(i)_S and LiL_i from Q(i)(Li∈⋅∣S)Q^(i)(L_i∈· S), paired with a composition that produces S with law PSP_S and draws LiL_i from Fi′(⋅∣S)F _i(· S), has evidence Q(i)Q^(i) and conditional laws Fi′F _i. In a deployment, different kernels at the same logged S arise when an unlogged input differs between the two deployments. Remark G.4.3 (Oversight cues). Let the composition be deployment and the standalone deployment be testing, with one component, the agent, and the cue Z as S. When Z is recorded and the agent’s kernel reads only Z and private randomness, Remark G.4.2(b) gives the interval [cB,cB+Pdep(U)][c_B,c_B+P_dep(U)] for a deployment event, where U holds the cue values never seen in testing. Appendix H Verification Index Scripts supporting Sections 2 and 3 evaluate finite instances using exact rational arithmetic (fractions.Fraction); seeded Monte Carlo cases, logarithms, and dynamic programs use floating point as disclosed in their headers. These calculations verify finite instances and counterexamples, whereas Appendices A to G prove the general theorems. The companion file checks/README.md provides the full script-to-claim map, execution commands, and worked examples. Appendix I AI Use Statement This disclosure supplements the Ethical Considerations. The authors used AI coding and writing assistants to support implementation, analysis tooling, proof checking, figure preparation, and manuscript drafting and revision. The reported empirical results are computed by evaluation code over logged runs and saved experimental artifacts. The authors take full responsibility for the methods, interpretation, and final content of the paper.