Paper deep dive
Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications
Ruggero Lanotte
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:Runtime monitoring traditionally evaluates a specification that is fixed before execution or externally modified when requirements change. In learning-enabled and data-intensive systems, however, the temporal relationships represented by a specification may themselves evolve. Allowing an AI component to directly replace a formal specification is unsafe: it may overfit transient behavior, weaken protected requirements, or activate statistically unsupported revisions. We introduce an intersymbolic architecture in which an untrusted AI proposer suggests temporal specification revisions and a symbolic governor controls their activation. Two results organize the framework. First, origin-version semantics makes the outcome of each obligation invariant to later revisions. Second, aggregate certification can conceal systematic failures on protected triggers; simultaneous aggregate and core-conditional post-selection certification controls both targets. A structural invariant preserves designer-protected components, and a proposer-independent lifetime error bound supports repeated activation decisions. The statistical bound concerns the predictable means of completed certification samples; interpreting it as future operational validity requires an additional stability assumption. Controlled synthetic experiments use a frozen supervised AI proposer to illustrate the masked-core failure at one decision and across repeated governed revisions. The proposer is a supervised regressor trained offline on synthetic tasks and frozen before use; it ranks candidates by predicted aggregate margin and never observes the protected-trigger success rate, so the masked-core failure arises from optimising the aggregate rather than from an adversary constructed by hand.
Tags
Links
- Source: https://arxiv.org/abs/2609.33461v1
- Canonical: https://arxiv.org/abs/2609.33461v1
Trouble viewing inline? Open PDF directly →
Full Text
123,438 characters extracted from source content.
Expand or collapse full text
Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications CCS: Software and its engineering Formal software verificationCCS: Theory of computation Logic and verification Ruggero Lanotte Affiliation: University of Insubria, Varese, Italy © none Abstract. Runtime monitoring traditionally evaluates a specification that is fixed before execution or externally modified when requirements change. In learning-enabled and data-intensive systems, however, the temporal relationships represented by a specification may themselves evolve. Allowing an AI component to directly replace a formal specification is unsafe: it may overfit transient behavior, weaken protected requirements, or activate statistically unsupported revisions. We introduce an intersymbolic architecture in which an untrusted AI proposer suggests temporal specification revisions and a symbolic governor controls their activation. Two results organize the framework. First, origin-version semantics makes the outcome of each obligation invariant to later revisions. Second, aggregate certification can conceal systematic failures on protected triggers; simultaneous aggregate and core-conditional post-selection certification controls both targets. A structural invariant preserves designer-protected components, and a proposer-independent lifetime error bound supports repeated activation decisions. The statistical bound concerns the predictable means of completed certification samples; interpreting it as future operational validity requires an additional stability assumption. Controlled synthetic experiments use a frozen supervised AI proposer to illustrate the masked-core failure at one decision and across repeated governed revisions. The proposer is a supervised regressor trained offline on synthetic tasks and frozen before use; it ranks candidates by predicted aggregate margin and never observes the protected-trigger success rate, so the masked-core failure arises from optimising the aggregate rather than from an adversary constructed by hand. Keywords: runtime verification, temporal specifications, specification evolution, confidence sequences, AI proposer 1. Introduction Modern data-intensive systems continuously generate timestamped observations. Runtime verification provides a principled mechanism for determining whether such executions satisfy temporal requirements (Bauer et al., 2011a; Maler and Nickovic, 2004). A typical property may require that an event A be followed by an event B within a bounded interval, (1) □(A→◇[a,b]B), (A→ _[a,b]B ), or, under uncertainty, that such a response occur with probability at least λ, as in probabilistic temporal formalisms such as PrSTL (Sadigh and Kapoor, 2016), (2) A⇒λ,[a,b]B.A _λ,[a,b]B. Such requirements are routinely deployed over streams whose generating process is not stationary. In a clinical-alarm monitor, for instance, a rule requiring that a desaturation alert be followed by a documented intervention within a bounded delay may have been specified for a given patient population, ward staffing level, and sensor configuration. A change in these conditions may alter the observed delay or the circumstances in which the rule applies. Persistent violations then require investigation: the monitor alone cannot distinguish a mismatch caused by the changed operating regime from a genuine safety degradation. Similar issues arise in service-level monitoring after a routing change and in industrial supervision after a retooling. In these settings, some components of a requirement are safety-relevant and must survive adaptation, while others describe relationships that may need to follow the process. The relationship encoded by a specification may evolve in a non-stationary environment, a setting closely related to concept-drift adaptation in streaming learning (Gama et al., 2014). For example, (3) A⇒0.90,[2,5]BA _0.90,[2,5]B may cease to describe the observed process, while (4) (A∧C)⇒0.92,[3,8]B(A C) _0.92,[3,8]B becomes supported by persistent evidence. A fixed monitor may then generate systematic violations after a regime change. Prior work has therefore considered adaptive monitoring and changing runtime requirements (Perotti et al., 2015; Carwehl et al., 2023). Conversely, a learner allowed to freely rewrite its own specification may eliminate violations by weakening the property. Our governor therefore preserves designer-protected trigger and response components and keeps every parameter tuple inside a fixed admissible envelope. Structural preservation alone is insufficient: a high aggregate success rate can conceal systematic failures on protected triggers. We therefore also require core-conditional statistical certification. Proposal, certification, and activation are distinct. At a selection index n⋆n , an untrusted proposer supplies candidate revisions using the observed prefix. The governor checks structural admissibility and collects completed obligations generated for the selected candidate after selection. Only if the statistical conditions hold at a later decision index m can the candidate become active for subsequent events: (≤n⋆,ψj)∋ψ⋆→post-selection certificationm+1(ψ⋆),m>n⋆. Propose(e_≤ n , _j) ψ \;post-selection certification\; Activate_m+1(ψ ), m>n . The proposer may be neural, statistical, rule-based, or LLM-based; its output is treated as untrusted. The problem studied in this paper is to decide whether an AI-proposed revision ψ can replace the active specification ψj _j while ensuring: (i) deterministic preservation of protected trigger and response structure; (i) admissibility of the rewrite; (i) post-selection statistical support for the candidate both overall and on protected triggers; (iv) non-retroactive semantics for obligations generated under earlier versions; and (v) a global bound on unsupported activations over the evolution history. The paper has two main results: (1) Origin-version non-retroactivity. An obligation retains the version under which it was generated, so later revisions cannot change its outcome. A retroactive active-version interpretation fails by counterexample. (2) Masked core failure and its certification remedy. An aggregate success rate may remain high while responses on protected triggers fail. Simultaneous aggregate and core-conditional post-selection bounds address this failure mode. The two-time semantics and protected-envelope invariant provide the formal setting for these results. A proposer-independent lifetime theorem supports the second result by bounding false certifications relative to the predictable means of the completed samples available at each decision. Finite-prefix evidence may initiate evolution but does not create a third activation guarantee. Claims about obligations generated after activation require a separate stability assumption. The technical novelty is therefore not the Hoeffding inequality or error spending in isolation. It is the certification target and proof structure forced by specification evolution: the candidate is chosen adaptively, evidence is indexed by completed post-selection obligations, activation may occur while earlier versions still own unresolved obligations, and the protected-trigger subsequence overlaps the aggregate sample. These features jointly determine what can be certified without assuming correctness of the AI proposer. All proofs are collected in Appendix A. 2. Related Work and Positioning The proposed framework lies at the intersection of runtime verification, temporal specification learning, concept-drift adaptation, and neural-symbolic or intersymbolic AI (Platzer, 2024); we use intersymbolic in that sense, with a symbolic and a subsymbolic component interlinked and the symbolic side retaining decision authority. Runtime verification and changing requirements. Runtime verification monitors execution prefixes against temporal properties (Bauer et al., 2011a; Maler and Nickovic, 2004). Adaptive monitoring is not new: Perotti, Garcez, and Boella combine neural-symbolic monitoring with learning-based adaptation of the initial specification (Perotti et al., 2015), while Carwehl et al. address runtime verification under changing requirements and preserve intermediate monitoring results when properties are adapted (Carwehl et al., 2023). Carwehl et al. address the complementary question of how monitor state is carried across a property change; the present paper fixes no monitor representation and is concerned instead with whether a revision may become active at all. Shared monitoring of multiple temporal properties has also been studied by Demir and Ulus (Demir and Ulus, 2026), while SENTIL supplies a probabilistic temporal-logic monitoring tool (Quansah and Bonnah, 2026). These two papers address monitoring computation or probabilistic checking; our activation rule additionally certifies a protected-trigger subpopulation under adaptive proposal. Our setting differs in that candidate structural revisions are generated by an explicitly untrusted proposer and become active only after a separate symbolic and statistical certification step. Learning temporal specifications. Temporal-logic learning and specification mining infer formulas or parameters from observed traces. Bombara and Belta introduced online learning of STL formulas from incrementally arriving labelled signals (Bombara and Belta, 2018) and later developed a decision-tree framework covering both offline and online STL learning (Bombara and Belta, 2021). Probabilistic Signal Temporal Logic (PrSTL) represents uncertain temporal properties whose probabilistic predicates can evolve as beliefs are updated from data (Sadigh and Kapoor, 2016). We therefore do not claim novelty for online formula learning, probabilistic temporal specifications, or parameter adaptation in isolation. Instead, the learned component in our architecture is only a proposer: activation is governed independently of the proposal mechanism. Concept drift and sequential certification. Concept-drift adaptation studies changes in data generating processes and online model adaptation (Gama et al., 2014). Our notion of semantic drift is narrower: it concerns a persistent change in the validity of an explicitly represented temporal relation. For repeated statistical decisions, ordinary fixed-time intervals are insufficient under optional stopping; confidence sequences provide time-uniform coverage over unbounded horizons (Howard et al., 2021), while betting-based constructions provide practical anytime-valid confidence sequences for bounded means (Waudby-Smith and Ramdas, 2024). We use this sequential-inference perspective to certify a sequence of specification revisions rather than a single model estimate. Classical post-selection inference instead adjusts inference for a data-dependent model-selection step (Berk et al., 2013). Our construction separates the selected prefix from fresh prospective outcomes and conditions on the selection-time information; it therefore addresses a different sequential object, but the same selection-versus-inference distinction is essential. Certified self-modification of AI systems. The Statistical Gödel Machine (SGM) admits recursive edits through statistical tests and a global risk budget (Wu et al., 2025). Self-Evolving Agents (SEA) uses anytime-valid certificates to gate changes to a steering adapter and a versioned harness around a frozen base model (Sengupta, 2026). These works establish that certification and cumulative error control are relevant to self-modifying AI. Our object of revision is a temporal specification rather than an agent implementation; origin-version obligations and the protected-trigger conditional target require separate semantics and evidence. Robust probabilistic shielding. Recent shielding methods combine learned uncertainty sets with formal probabilistic guarantees. Galesloot, Rhemrev, and Jansen construct shields for safe offline reinforcement learning from a fixed data set and obtain a high-confidence policy-safety guarantee (Galesloot et al., 2026). Hamel-De le Court et al. synthesize sound and optimal shields for robust MDPs, enforcing an LTL probability threshold against worst-case transition probabilities and combining the construction with PAC transition learning (le Court et al., 2026). These results already cover probabilistic automata, data-derived model sets, and uniform robust safety over the admissible dynamics. Our problem is different: the object being changed is the temporal specification itself, rather than the policy or its permitted actions. Consequently, the formal obligations are to keep pending obligations attached to their origin version, preserve a designer-fixed syntactic core, and certify both the aggregate and the protected-trigger conditional targets of an adaptively selected revision. The present lifetime bound ranges over specification activations; it is not a replacement for model-robust shielding. Monitoring deployed models and subpopulation guarantees. A related line monitors a deployed model sequentially and separates shifts that degrade performance from benign ones, either by sequential testing on a tracked risk (Podkopaev and Ramdas, 2022) or by weighted conformal test martingales that adapt to mild shifts while detecting and diagnosing harmful ones (Prinster et al., 2025). Our aggregate versus protected-group decomposition is related but not learned: the partition is the designer-fixed protected trigger, it is immutable under revision, and it is the same predicate that the deterministic invariant protects. Certifying a fixed subpopulation separately from the aggregate is likewise studied outside runtime verification (Cherian and Candès, 2024); what is specific to our setting is its interaction with adaptively selected candidates and with repeated activations under a single lifetime budget. Our distinguishing principle is AI proposal+symbolic admissibility+statistical certification+controlled activation. AI proposal+symbolic admissibility+statistical certification+controlled activation. The AI component proposes candidate revisions but is not part of the trusted computing base. The symbolic governor decides activation and maintains guarantees across an adaptively generated sequence of specification versions. We do not claim a new concentration inequality, a new temporal-logic learning algorithm, or a new shielding construction. The contribution is the certification object induced by adaptive specification revision: a candidate chosen from the observed prefix is monitored prospectively before activation, its completed outcomes are indexed by an outcome filtration, and pending operational obligations remain attached to their origin versions. Within that semantics, deterministic preservation of the designer-fixed core and simultaneous aggregate/core evidence compose into a lifetime guarantee over actual specification activations. 3. Model and Temporal Semantics 3.1. Timed streams Let AP be a finite set of atomic propositions. A timed observation is a pair en=(tn,νn),e_n=(t_n, _n), where n∈ℕn is the event index, tn∈ℝ≥0t_n _≥ 0 is a timestamp, and νn⊆ _n is the set of atomic propositions observed at time tnt_n. Definition 0 (Timed stream). A timed stream is a finite or infinite sequence =e0e1e2⋯e=e_0e_1e_2·s of timed observations with non-decreasing timestamps. For a finite stream =e0⋯eN−1e=e_0·s e_N-1, we require tn≤tn+1t_n≤ t_n+1 and n=0,…,N−2,n=0,…,N-2, whereas for an infinite stream the same condition holds for every n∈ℕn . In addition, every infinite timed stream is required to be non-Zeno: limn→∞tn=∞. _n→∞t_n=∞. Thus every finite temporal horizon is eventually exceeded at a finite event index. We write ℰωE^ω for the set of infinite timed streams and ℰ∗E for the set of finite timed streams. For an infinite stream ∈ℰωe ^ω, the finite prefix available at event index n is ≤n=e0e1⋯en∈ℰ∗.e_≤ n=e_0e_1·s e_n . We use n exclusively for event indices. 3.2. Temporal language Following the bounded-time monitoring tradition of metric temporal logics (Alur and Henzinger, 1993; Maler and Nickovic, 2004; Bauer et al., 2011b), we consider the bounded future-time fragment of MTL generated by φ::=p|⊤|⊥|¬φ∣φ∧φ∣φ∨φ∣□[a,b]φ∣◇[a,b]φ, ::=p _[a,b] _[a,b] , where p∈p and 0≤a≤b<∞0≤ a≤ b<∞. We denote by Φ the set of formulas generated by this grammar. The satisfaction relation is defined over infinite timed streams ∈ℰωe ^ω and event indices n∈ℕn . The constants satisfy ,n⊧⊤e,n and ,n⊧̸⊥e,n for every stream and event index. Moreover ,n⊧p ,n p ⇔p∈νn, p∈ _n, ,n⊧¬φ ,n ⇔,n⊧̸φ, ,n , ,n⊧φ1∧φ2 ,n _1 _2 ⇔,n⊧φ1 and ,n⊧φ2, ,n _1 and e,n _2, ,n⊧φ1∨φ2 ,n _1 _2 ⇔,n⊧φ1 or ,n⊧φ2, ,n _1 or e,n _2, ,n⊧□[a,b]φ ,n _[a,b] ⇔∀m≥n:(tm−tn∈[a,b]) implies ,m⊧φ, ∀ m≥ n: (t_m-t_n∈[a,b] ) implies e,m , ,n⊧◇[a,b]φ ,n _[a,b] ⇔∃m≥n:(tm−tn∈[a,b])∧,m⊧φ. ∃ m≥ n: (t_m-t_n∈[a,b] ) ,m . Finite streams ≤n∈ℰ∗e_≤ n represent the prefixes available to the online monitor and are not assigned the above two-valued satisfaction relation. Since all temporal intervals are bounded, every formula φ∈Φ ∈ has a finite structural horizon. Set hzn(⊤)=hzn(⊥)=0hzn( )=hzn( )=0. Define hzn(p) (p) =0, =0, hzn(¬φ) ( ) =hzn(φ), =hzn( ), hzn(φ1∘φ2) ( _1 _2) =maxhzn(φ1),hzn(φ2),∘∈∧,∨, = \hzn( _1),hzn( _2)\, ∈\ , \, hzn(□[a,b]φ) ( _[a,b] ) =b+hzn(φ), =b+hzn( ), hzn(◇[a,b]φ) ( _[a,b] ) =b+hzn(φ). =b+hzn( ). Hence, for every φ∈Φ ∈ , the truth value of ,n⊧φe,n is determined once the timed stream has progressed beyond tn+hzn(φ)t_n+hzn( ). 3.3. Probabilistic trigger–response semantics In addition to trace-level formulas defined above, we consider probabilistic trigger–response specifications. Admissible parameter envelope. The designer fixes a measurable admissible parameter envelope par⊆(λ,a,b)∈[0,1]×ℝ≥02| 0≤a≤b<∞.A_par \(λ,a,b)∈[0,1]×R_≥ 0^2\; |\;0≤ a≤ b<∞ \. The set parA_par specifies the parameter combinations permitted by the designer. Each admissible triple (λ,a,b)(λ,a,b) determines a minimum success threshold λ and a bounded response window [a,b][a,b]. Every specification version must use parameters belonging to parA_par, and parameter revisions may select only triples within this set. The envelope is fixed independently of the AI proposer and remains unchanged throughout specification evolution. No closure, convexity, or ordering assumption is imposed on parA_par. When desired, the designer may additionally impose a strict lower threshold λmin:=infλ:(λ,a,b)∈par>0. _ := \λ:(λ,a,b) _par\>0. Definition 0 (Probabilistic trigger–response specification). A probabilistic trigger–response specification is the tuple ψ=(φ1core,φ1adapt,φ2core,φ2adapt,λ,a,b),ψ= ( _1^core, _1^adapt, _2^core, _2^adapt,λ,a,b ), where φ1core,φ1adapt,φ2core,φ2adapt∈Φ _1^core, _1^adapt, _2^core, _2^adapt∈ and (λ,a,b)∈par(λ,a,b) _par. Define the derived trigger and response by trig(ψ)=φ1core∨φ1adapttrig(ψ)= _1^core _1^adapt and resp(ψ)=φ2core∧φ2adaptresp(ψ)= _2^core _2^adapt. We use the abbreviation ψ=trig(ψ)⇒λ,[a,b]resp(ψ)ψ=trig(ψ) _λ,[a,b]resp(ψ) whenever the component decomposition is not itself under discussion, and write λψ=λ _ψ=λ. A specification without a protected core is represented by the convention φ1core=⊥ _1^core= and φ2core=⊤. _2^core= . Let Ψ⊆Φ4×par ^4×A_par denote the set of all such tuples. Equip Φ with a fixed σ-algebra ΣΦ _ and parA_par with its chosen measurable structure (for instance, the trace Borel σ-algebra when the envelope is Borel). We equip Ψ with the corresponding product/subspace σ-algebra ΣΨ=(ΣΦ⊗4⊗Σpar)|Ψ. _ = . ( _ 4 _A_par ) |_ . Equality in Ψ is componentwise tuple equality. Consequently, two specifications with semantically equivalent derived trigger and response but different core/adaptive decompositions are distinct elements of Ψ . A trigger–response obligation for ψ is generated at event index n if ,n⊧trig(ψ)e,n (ψ). The obligation is successful if there exists an event index m≥nm≥ n such that tm−tn∈[a,b]t_m-t_n∈[a,b] and ,m⊧resp(ψ)e,m (ψ). The success condition is defined with respect to the infinite stream and need not be decidable when the obligation is generated. Define the observation horizon by H(ψ)=maxhzn(trig(ψ)),b+hzn(resp(ψ)).H(ψ)= \! \hzn(trig(ψ)),\;b+hzn(resp(ψ)) \. The response window ends at tn+bt_n+b. The truth of the trigger at n is guaranteed to be observable once the observed stream has advanced beyond tn+hzn(trig(ψ))t_n+hzn(trig(ψ)). The success or failure of the response condition is guaranteed to be observable once the stream has advanced beyond tn+b+hzn(resp(ψ))t_n+b+hzn(resp(ψ)). We adopt the conservative convention that an obligation is completed at the first observed event whose timestamp exceeds tn+H(ψ)t_n+H(ψ). At completion, both the truth of its trigger and, if the trigger holds, its success or failure are observable from the finite prefix. An outcome may become observable earlier, but is recorded as completed only at this boundary. Given a timed stream =e0e1e2⋯e=e_0e_1e_2·s, en=(tn,νn)e_n=(t_n, _n), the self-evolving monitor maintains a sequence of specification versions ψ0,ψ1,ψ2,…. _0, _1, _2,…. We use j exclusively for specification-version indices. Let 0=n0<n1<n2<⋯0=n_0<n_1<n_2<·s be the specification activation indices, with nj∈ℕn_j denoting the event index at which version ψj _j becomes active. At event index n, the active specification is the unique version ψj _j such that nj≤n<nj+1n_j≤ n<n_j+1. If the version sequence is finite and ψj _j is its last version, we use the convention nj+1=∞n_j+1=∞. Example 0 (Specification activation indices). Consider the timed stream =e0e1e2e3e4e5⋯,e=e_0e_1e_2e_3e_4e_5·s, with e0=(0,ν0),e1=(2,ν1),e2=(4,ν2),e3=(7,ν3),e4=(9,ν4),e5=(12,ν5).e_0=(0, _0),\;e_1=(2, _1),\;e_2=(4, _2),\;e_3=(7, _3),\;e_4=(9, _4),\;e_5=(12, _5). Suppose that the specification activation indices are n0=0n_0=0, n1=3n_1=3 and n2=5n_2=5. Then ψ0 _0 is active at event indices 0,1,20,1,2, ψ1 _1 is active at event indices 3,43,4, and ψ2 _2 becomes active at event index 55. Thus, j indexes specification versions, whereas njn_j is an event index identifying where the corresponding specification version becomes active on the timed stream. In particular, e5=(12,ν5)e_5=(12, _5), so ψ2 _2 becomes active at event index 55, corresponding to timestamp t5=12t_5=12, immediately before e5e_5 is processed. The evolution of the specification sequence is governed by an admissible revision relation and an AI proposer. Symbolic governor The admissible revision relation ℛ⊆Ψ×ΨR × is defined a priori by the system designer and specifies which structural changes between specification versions are permitted. Untrusted AI proposer Let Ξ denote the space of random seeds used by the proposer. At runtime, the possibly randomized proposal mechanism is represented by :ℰ∗×Ψ×Ξ→2Ψ. Propose:E × × → 2 . Its internal randomness is included in the selection-time information introduced in Section 6. When ψj _j is active at event index n, the proposer computes from the observed prefix ≤ne_≤ n the set of candidate revisions n,j=(≤n,ψj,ξnprop)⊆Ψ,P_n,j= Propose(e_≤ n, _j, _n^prop) , where ξnprop∈Ξ _n^prop∈ is the random seed used at that invocation. The proposer returns decomposed specification tuples in Ψ . The governor, rather than the proposer, enforces preservation of the incumbent’s protected components through ℛR. Hence, ℛR is a fixed design constraint, whereas n,jP_n,j is a data-dependent candidate set generated online. Specification evolution. We distinguish two transition notions. Definition 0 (Specification evolution transitions). For an active specification ψj _j at event index n, we write ψj→ℛ,ψiffψ∈n,jandψjℛψ. _j [n]R,Pψ ψ _n,j _j Rψ. The relation ψj→ℛ,ψ _j [n]R,Pψ means that ψ is proposed at event index n and is an admissible revision of ψj _j. This transition does not modify the active specification. We write ψj⇒nj+1ψj+1 _j [n_j+1] _j+1 to denote the subsequent certified activation of the next specification version at event index nj+1n_j+1. We refer to this second transition as a specification-version transition. Its formal certification condition is defined later in Section 6. The certified-activation rule of Section 6 implies the following fact: ψj⇒nj+1ψj+1impliesnj≤n<nj+1andψj→ℛ,ψj+1. _j [n_j+1] _j+1 n_j≤ n<n_j+1 _j [n]R,P _j+1. Example 0 (Proposed revision and certified activation). Consider again the timed stream and specification activation indices of Example 3. In particular, ψ0 _0 is active at event indices 0,1,20,1,2, and ψ1 _1 becomes active at n1=3n_1=3. A candidate that will eventually become ψ1 _1 may be proposed and selected while ψ0 _0 is still active, for example at event index n=0n=0. Thus, ψ0→0ℛ,ψ1 _0 [0]R,P _1 does not activate ψ1 _1. It only states that ψ1 _1 has been proposed at event index 00 and is an admissible revision of ψ0 _0. Suppose that sufficiently many post-selection obligations are completed by event index 22 and that the statistical certification condition is satisfied. The specification-version transition ψ0⇒3ψ1 _0 [3] _1 then occurs. We adopt an origin-version semantics. A response obligation generated while ψj _j is active is evaluated according to the temporal interval and trace-level formulas of ψj _j, even if ψj+1 _j+1 becomes active before the obligation is completed. Hence, a revision cannot retroactively change the meaning of an already generated obligation. More precisely, the operational version assigned to an origin index k is the unique ψj _j satisfying nj≤k<nj+1n_j≤ k<n_j+1. This assignment is made at k, even if a future-time trigger cannot yet be decided from ≤ke_≤ k: the monitor retains that origin and its version until the trigger status and, when applicable, the obligation outcome have been resolved. A candidate monitored before activation produces certification-only observations, not operational obligations under the candidate for those earlier origins. The admissible revision relation ℛR and the proposer-generated candidate sets n,jP_n,j are defined in detail in the following sections. A proposed admissible candidate becomes the next active specification only after satisfying the statistical certification conditions defined in Section 6. 4. Controlled Specification Evolution: Admissible Revision Classes Structural admissibility is determined by ℛR, whereas statistical certification and activation are enforced separately by the symbolic governor. Consequently, the structural guarantees below do not depend on the internal architecture, training procedure, or correctness of the proposer. The tuple representation of Definition 2 separates two designer-protected components from two adaptive components. The protected components cannot be modified by specification evolution, whereas either adaptive component may be revised. The disjunction in the derived trigger ensures that every protected trigger remains covered, while the conjunction in the derived response ensures that every successful full response satisfies the protected response component. Definition 0 (Admissible revision). For any ψ,ψ~∈Ψψ, ψ∈ such that ψℛψ~ψ R ψ it holds that: (1) the protected components of ψ and ψ~ ψ are unchanged; (2) at most one of the two adaptive components of ψ~ ψ differs from its counterpart in ψ; (3) the parameter tuple of ψ~ ψ belongs to parA_par; and (4) at least one adaptive component or the parameter tuple of ψ~ ψ differs from its counterpart in ψ. Thus an admissible revision is a pure parameter shift, a trigger-adaptive replacement, or a response-adaptive replacement, where an adaptive replacement may be accompanied by a parameter shift. Structural admissibility does not impose a strengthening order between successive versions. Within the designer-declared envelope, the threshold, temporal interval, and one adaptive component may change in either direction. Whether a structurally admissible candidate may become active is determined separately by statistical certification. Obtaining the decomposition. The deterministic invariant and the core-conditional certification of Section 6 both rest on the protected components φ1core _1^core and φ2core _2^core and on the envelope parA_par, all of which are supplied by the designer before deployment and are never revised. The framework does not infer them, and the guarantees it provides are relative to them: a vacuous protected trigger (φ1core=⊥ _1^core= ) disables core certification and reduces the invariant to the response core and the envelope. Three considerations guide the choice in practice. First, the protected trigger should capture the situations in which the requirement is safety-relevant rather than the typical ones, since the invariant guarantees coverage of exactly those; in the clinical-alarm setting of Section 1 this is the subset of desaturation events that a clinical protocol classifies as requiring escalation, not all alerts. Second, the protected response should retain only the conjuncts whose violation is itself unsafe, because every additional conjunct is a requirement that no future revision may relax, and an over-specified response core makes admissible revisions impossible rather than unsafe. Third, the protected share w induced by φ1core _1^core determines the cost of core certification: as quantified in Remark 1, collecting a fixed amount of core-conditional evidence requires approximately 1/w1/w aggregate trigger observations. A narrowly defined protected trigger may isolate the genuinely critical situations, but if those situations are rare, substantially more aggregate observations are needed. This is an inherent trade-off between the semantic scope of protection and certification latency; the trigger should therefore be defined by the safety requirement, not enlarged or narrowed merely to improve sample efficiency. Theorem 2 (Deterministic protected-envelope invariant). Let ψ0ℛψ1ℛ⋯ℛψq _0 R _1 R·s R _q be any finite chain of admissible revisions, and write the protected components of ψ0 _0 as φ1core _1^core and φ2core _2^core. Then, for every i∈0,…,qi∈\0,…,q\: (1) the protected components of ψi _i are exactly φ1core _1^core and φ2core _2^core; (2) for every timed stream e and event index n, ,n⊧φ1coree,n _1^core implies ,n⊧trig(ψi)e,n ( _i); (3) for every timed stream e and event index m, ,m⊧resp(ψi)e,m ( _i) implies ,m⊧φ2coree,m _2^core; (4) the parameter tuple of ψi _i belongs to parA_par. Theorem 2 is a deterministic guarantee: it holds for every admissible revision chain, rather than with probability 1−δ1-δ. It is intentionally structural. In particular, the trigger implication and response implication are pointwise properties; they do not equate the temporal obligations of versions with different response windows. Preserving the protected response as a conjunct does not by itself guarantee that responses to protected triggers succeed with high probability; the corresponding probabilistic requirement is enforced separately by the core-conditional certification introduced in Section 6. 5. Obligation Outcomes and Regime Semantics 5.1. Response outcomes and regime validity For the statistical statements in this section, fix a probability space (Ω,ℱ,ℙ)( ,F,P) on which the timed stream e is an ℰωE^ω-valued random element. We equip ℰωE^ω and the auxiliary spaces used by the proposal and selection mechanisms with fixed σ-algebras, and equip Ψ with the product/subspace σ-algebra ΣΨ _ defined in Section 3.3. We assume that the timed stream, proposer output, selected candidate, and all other random objects entering the generated σ-algebras below are measurable with respect to their corresponding measurable spaces. All response outcomes and filtrations below are defined on this probability space. Before defining the binary response outcome, we formalize when a trigger–response obligation is generated and when its response window has completed. Definition 0 (Completed trigger–response obligation). Let ψ=φ1⇒λ,[a,b]φ2ψ= _1 _λ,[a,b] _2. A trigger–response obligation is generated at event index n if ,n⊧φ1e,n _1. The obligation generated at n is completed once its binary outcome is guaranteed to be observable, namely if there exists an event index m≥nm≥ n such that tm>tn+H(ψ)t_m>t_n+H(ψ). Note that the response window [tn+a,tn+b][t_n+a,t_n+b] may close before the obligation is completed in the sense above, because evaluating φ2 _2 may itself require future observations. As an example for φ2=◇[0,5]p _2= _[0,5]p it holds hzn(φ2)=5hzn( _2)=5. Completion does not imply satisfaction; satisfaction or violation is determined by the binary response variable defined below. When H(ψ)=0H(ψ)=0, the strict inequality is conservative: it waits until the stream progresses to a strictly later timestamp even though a purely propositional zero-delay outcome may already be decidable at n. For every event index k, define the binary response indicator for a fixed version ψj _j by Xkψj=[∃m≥k:tm−tk∈[aj,bj]∧,m⊧resp(ψj)].X_k _j=1\! [∃ m≥ k:t_m-t_k∈[a_j,b_j] ,m ( _j) ]. When ,n⊧φ1e,n _1, this indicator is the binary outcome of the obligation generated at n: Xnψ=1X_n^ψ=1 denotes satisfaction and Xnψ=0X_n^ψ=0 violation. At runtime this outcome is admitted to monitoring or certification only after the obligation is completed according to Definition 1. Defining XnψX_n^ψ on the whole probability space makes the trigger-conditioned probability used below well defined. Each trigger generates a distinct obligation outcome even when response windows overlap. The following theorem is immediate once origin-version semantics is fixed; its role is not technical depth but removal of a genuine ambiguity about pending obligations when a revision occurs before their response windows have completed. Theorem 2 (Origin-version non-retroactivity). Let an obligation originate at index k under ψj _j. Under origin-version semantics, its trigger status, outcome XkψjX_k _j, and completion index cψj(k):=minm≥k:tm>tk+H(ψj)c_ _j(k):= \m≥ k:t_m>t_k+H( _j)\ depend only on (,k,ψj)(e,k, _j) and are unaffected by subsequent revisions. For every origin index k, there exists exactly one j such that nj≤k<nj+1n_j≤ k<n_j+1. Consequently, the obligation originating at k is assigned to ψj _j, independently of when it completes. The origin-version choice is statistically consequential rather than merely notational. To see this, consider instead a hypothetical active-version semantics that reinterprets an unresolved obligation using the specification active when its response is evaluated. Choose distinct u,v,w∈u,v,w , an admissible parameter envelope containing (1,1,1)(1,1,1), and a specification space Ψ containing the tuples ψ=(u,⊥,⊤,v,1,1,1)ψ=(u, , ,v,1,1,1) and ψ′=(u,⊥,⊤,w,1,1,1)ψ =(u, , ,w,1,1,1). Their derived specifications are u⇒1,[1,1]vu _1,[1,1]v and u⇒1,[1,1]wu _1,[1,1]w, respectively. The revision ψℛψ′ψ Rψ changes only the adaptive response. Let tk=0t_k=0, tk+1=1t_k+1=1, tk+2=2t_k+2=2, with u true at k, v true and w false at k+1k+1. The obligation originates under ψ at k and, by the strict completion convention, completes at k+2k+2. Under origin-version semantics it succeeds regardless of whether ψ′ψ is activated at k+1k+1. Under the hypothetical active-version interpretation, the same unresolved obligation succeeds if ψ remains active, but fails if ψ′ψ is activated at k+1k+1 and its response is used at completion. Thus two activation histories with identical timed observations and the same origin version can produce different active-version outcomes. This counterexample concerns the interpretation of a pending obligation, not whether the hypothetical activation has passed a particular statistical test. Consequently, Assumption 1 below is naturally well-posed under origin-version semantics because it indexes a success probability by a fixed specification ψ. Under active-version semantics, the analogous probability would additionally depend on the stochastic revision process; a statistical treatment would therefore have to enlarge the probabilistic model to include that process explicitly. This observation does not rule out such a model, but it shows why the fixed-ψ regime assumption used in this paper relies on non-retroactivity. Definition 0 (Regime sequence). Behavioral evolution is represented by an ordered sequence of regimes R0,R1,R2,…R_0,R_1,R_2,…, we use r exclusively for regime indices. Each Rr⊆ℕR_r is a nonempty contiguous set of event indices. Whenever Rr+1R_r+1 exists, RrR_r is finite and minRr+1=maxRr+1 \R_r+1\= \R_r\+1. The regime sequence is a model-provided segmentation of the event-index axis and is not defined through the success probabilities of any particular specification. Regimes therefore represent exogenous behavioral phases of the underlying process. Assumption 1 (Regime-level stability). Let Pr denote the probability law governing the random timed stream e. For a specification ψ=φ1⇒λ,[a,b]φ2ψ= _1 _λ,[a,b] _2 and a regime RrR_r, there exists pRr(ψ)∈[0,1]p_R_r(ψ)∈[0,1]. For each n∈Rrn∈ R_r, let En,rψ:=∃m∈Rr:m≥n and tm>tn+H(ψ)E_n,r^ψ:= \∃ m∈ R_r:m≥ n and t_m>t_n+H(ψ) \ be the event that the obligation originating at n can be completed within RrR_r. For every n∈Rrn∈ R_r such that Pr(,n⊧φ1∩En,rψ)>0 (\e,n _1\∩ E_n,r^ψ)>0, we require Pr(Xnψ=1∣,n⊧φ1,En,rψ)=pRr(ψ). \! (X_n^ψ=1 ,n _1,E_n,r^ψ )=p_R_r(ψ). This assumption is invoked only for the particular incumbent or candidate specification whose regime-level interpretation is needed; it is not a simultaneous stationarity assumption over all ψ∈Ψψ∈ . A regime-level success parameter is identified by Assumption 1 only when the regime contains at least one origin index with positive probability of both triggering and completion within the regime. If no such index exists, the assumption is vacuous and no regime-validity claim is made. Whenever Assumption 1 holds and such an index exists, the specification ψ is valid in regime RrR_r if Rr⊧ψ⟺pRr(ψ)≥λψ.R_r ψ p_R_r(ψ)≥ _ψ. The statistical certification results below do not require Assumption 1; it is used only to interpret a certified average predictable success probability as a regime-level success probability. Example 0 (Regime and specification indices). Consider again the timed stream and specification activation indices of Example 3. In particular, n0=0n_0=0, n1=3n_1=3 and n2=5n_2=5. Suppose that the behavioral regime sequence is R0=0,1R_0=\0,1\, R1=2,3,4R_1=\2,3,4\ and R2=5,6,7,…R_2=\5,6,7,…\. Then the transition from R0R_0 to R1R_1 occurs at event index 22, while ψ0 _0 is still active. The specification-version transition from ψ0 _0 to ψ1 _1 occurs only at event index n1=3n_1=3. Hence, regime boundaries and specification activation boundaries need not coincide. In particular, the same specification ψ0 _0 is active in both R0R_0 and the initial part of R1R_1. It may therefore have different regime probabilities pR0(ψ0)≠pR1(ψ0)p_R_0( _0)≠ p_R_1( _0). 6. Statistical Certification and Activation Notational convention. From this section onwards a single specification-version transition is under consideration and we suppress its index j on all run-level quantities, writing n⋆n , ψ⋆ψ , λ⋆λ and H⋆H for the selection index, the selected candidate, its threshold and its observation horizon. Certification quantities then carry a single index: an event index when written m, a certification sample size when written q or s. In particular NmN_m is the sample size available at event index m, so that p¯Nm p_N_m is the running average p¯q p_q evaluated at q=Nmq=N_m, and KmK_m, LmL_m, p^Nm p_N_m are the corresponding trigger set, lower bound and empirical frequency. A superscript corecore marks the protected-trigger subsample, and a group index g∈all,coreg∈\all,core\ is used where the aggregate and core statements have the same form. Objects belonging to the sequence of versions retain the index: ψj _j, njn_j, ξj _j, ℋjH_j, j,sG_j,s, δj _j, mjcertm_j^cert and FjF_j. 6.1. Drift as a proposal gate The governor separates candidate selection from activation. A drift declaration enables an evolution attempt but does not contribute to the activation certificate. Structural admissibility is checked when the candidate is selected, whereas activation depends only on the subsequent certification evidence of Section 6. The prototype uses a deterministic two-window detector. For a fixed window length h, it compares the empirical success frequencies in the two most recent non-overlapping windows of h completed incumbent obligations and declares a decrease when their difference exceeds a fixed margin. The end-to-end experiment of Section 8.3 exercises this detector. The masked-core experiment instead supplies the drift declaration exogenously in order to isolate the certification mechanism. The detector affects when candidate selection begins but not the coverage guarantee of the subsequent certification procedure. A prefix-measurable detector cannot establish the success probability of obligations generated after activation: observationally identical prefixes may admit different continuations. Interpreting the activation certificate as a guarantee for such obligations therefore requires the additional stability condition discussed in Section 6.6. 6.2. Candidate selection Recall that the proposer is a possibly learned and randomized mechanism represented by :ℰ∗×Ψ×Ξ→2Ψ. Propose:E × × → 2 . At event index n, let ψj _j be the active specification. The proposer returns a set of candidate revisions n,j=(≤n,ψj,ξnprop)⊆Ψ,P_n,j= Propose(e_≤ n, _j, _n^prop) , where ξnprop∈Ξ _n^prop∈ is the random seed used at that invocation. The proposer may be implemented by any learned or data-driven model; its internal parameters are outside the trusted computing base. No correctness or soundness assumption is made on Propose. In particular, it may return statistically unsupported candidates, candidates violating protected requirements, or no candidate at all. Recall also that ψj→ℛ,ψ _j [n]R,Pψ denotes a proposed admissible revision while ψj _j remains active, and ψj⇒nj+1ψj+1 _j [n_j+1] _j+1 denotes the subsequent certified activation of the next specification version. The index j labels an actually activated version, not an attempt or a detector alarm. While ψj _j is active, a drift declaration only enables the governor to consider a proposal; selecting an admissible candidate starts its separate, prospective certification. Neither step changes ψj _j. The active specification changes and j advances only after the candidate first meets the activation test defined below. Without a selected and certified candidate there is no next version, and ψj _j remains active. The bounds in this section are therefore used to control the decision to activate a replacement, not to presume that a replacement must occur. The proposer may return multiple candidates in n,jP_n,j. Among them, the admissible candidates are those satisfying ψj→ℛ,ψ _j [n]R,Pψ. For each version ψj _j that becomes active, let n⋆n be the event index of the first (and only) candidate selected by the governor for its possible successor. Set n⋆=∞n =∞ if no candidate is ever selected while ψj _j is active. For version indices never reached by the execution, use the same convention and leave the corresponding candidate undefined. On n⋆<∞\n <∞\, let ψ⋆ψ be the selected candidate. Selection is enabled by a drift declaration and requires ψj→n⋆ℛ,ψ⋆ _j [n ]R,Pψ . The drift declaration and structural admissibility enable selection, not activation. There is at most one certification attempt per active version; an unsuccessful attempt does not create ψj+1 _j+1 and cannot be replaced by a second candidate under the same j. The selection may depend arbitrarily on the observed prefix ≤n⋆e_≤ n , on the candidate set n⋆,jP_n ,j, and on internal randomness available by the selection time, but not on the post-selection outcomes subsequently used for certification. 6.3. Selection-time information Definition 0 (Selection-time information). Recall the extended selection index n⋆∈ℕ∪∞n ∪\∞\. On n⋆<∞\n <∞\, let ξj _j collect the internal randomness used by the runtime decision mechanisms up to selection, including the proposer seed ξn⋆prop _n ^prop and, when applicable, the detector seed ζn⋆ _n . On n⋆=∞\n =∞\, assign fixed cemetery values to the stopped prefix ≤n⋆e_≤ n , the candidate set n⋆,jP_n ,j, the candidate ψ⋆ψ , and ξj _j; these objects are not used for certification on that event. Define ℋj=σ(n⋆<∞,n⋆,≤n⋆,n⋆,j,ψ⋆,ξj).H_j=σ\! (1_\n <∞\,n ,e_≤ n ,P_n ,j,ψ , _j ). Thus the fact of selection, its index, the observed prefix, and all proposal-and-selection information are ℋjH_j-measurable. No post-selection certification outcome is included on paths with finite selection time. On n⋆<∞\n <∞\, ℋjH_j represents the information available when ψ⋆ψ is selected for certification. In particular, it contains no certification outcome generated by a trigger occurring after n⋆n . All subsequent certification samples, filtrations, and bounds are defined only on this event. By construction, σ(≤n⋆)⊆ℋjσ(e_≤ n ) _j. Thus every selection-time decision based on the observed prefix and the internal randomness collected in ξj _j is ℋjH_j-measurable. 6.4. Candidate certification samples On n⋆<∞\n <∞\, let ψ⋆=φ1⇒λ⋆,[a,b]φ2ψ = _1 _λ ,[a,b] _2 be the candidate selected at event index n⋆n , and write Xk:=Xkψ⋆X_k:=X_k^ψ for the binary outcome of the candidate obligation originating at event index k. Aggregate and protected-trigger samples. Two certification samples are used: the aggregate sample of all post-selection completed candidate obligations and, when a protected trigger is present, the core sample restricted to protected triggers. Let g∈all,coreg∈\all,core\ index the enabled samples. The aggregate sample is always enabled; when the superscript is omitted, g=allg=all. For every event index m>n⋆m>n , define Km(all)=k>n⋆:,k⊧φ1,tm>tk+H⋆,Km:=Km(all).K_m^(all)= \k>n :e,k _1,\;t_m>t_k+H \, K_m:=K_m^(all). Thus KmK_m contains exactly the post-selection trigger indices whose obligations under ψ⋆ψ are fully observable by event index m. When φ1core≠⊥ _1^core≠ , define Km(core)=k∈Km:,k⊧φ1core.K_m^(core)= \k∈ K_m:e,k _1^core \. For every enabled group g, set Nm(g):=|Km(g)|,Nm:=Nm(all).N_m^(g):= |K_m^(g) |, N_m:=N_m^(all). In all cases, Km⊆n⋆+1,…,m−1K_m \n +1,…,m-1\. When the core sample is enabled, Km(core)⊆KmK_m^(core) K_m. For every enabled group g, the certification sample available at event index m is (Xk)k∈Km(g). (X_k )_k∈ K_m^(g). The core sample tests the full candidate response resp(ψ⋆)resp(ψ ) on protected triggers, not merely the protected response component in isolation. The trigger condition ,k⊧φ1e,k _1 is a trace-level property and does not depend on which specification version is currently active. Consequently, the selected candidate can be monitored prospectively before activation. The condition tm>tk+H⋆t_m>t_k+H ensures that the trigger status and complete response outcome of the obligation originating at k are observable by event index m. The designer fixes λcore∈[0,1] _core∈[0,1] independently of the proposer and of candidate selection. When φ1core=⊥ _1^core= , the core sample and its certification condition are disabled. Assumption 2 (Post-selection sample recurrence). For every selected candidate and every enabled group g, ⋃m>n⋆Km(g) _m>n K_m^(g) is almost surely infinite. Assumption 2 keeps the certification estimand conditional on actual trigger obligations and makes the time-uniform statement below well defined for every sample size q≥1q≥ 1. A finite-trigger extension can instead be obtained by conservative padding, but it targets a different quantity because non-occurrence is then incorporated into the estimand. For each enabled group g, enumerate the corresponding post-selection origins in increasing order: ⋃m>n⋆Km(g)=k1(g),k2(g),…,k1(g)<k2(g)<⋯. _m>n K_m^(g)= \k_1^(g),k_2^(g),… \, k_1^(g)<k_2^(g)<·s. Define the event index at which the s-th outcome of group g becomes available by τs(g)=minm>n⋆:Nm(g)≥s, _s^(g)= \m>n :N_m^(g)≥ s \, and define the associated completed-outcome filtration by j,0(g)=ℋj,j,s(g)=σ(ℋj,(kr(g),τr(g),Xkr(g))r=1s).G_j,0^(g)=H_j, _j,s^(g)=σ\! (H_j, (k_r^(g), _r^(g),X_k_r^(g) )_r=1^s ). When several outcomes become available at the same event index, they are entered into the certification sequence in increasing order of their origin indices. Thus each outcome is added in one filtration step, even when consecutive completion indices coincide. Both ks(g)k_s^(g) and Xks(g)X_k_s^(g) are j,s(g)G_j,s^(g)-measurable. Moreover, τs(g)≤m=Nm(g)≥s \ _s^(g)≤ m \= \N_m^(g)≥ s \, for every event index m. The latter event is determined by ℋjH_j and ≤me_≤ m; hence τs(g) _s^(g) is a stopping index for the post-selection observation filtration. Because all obligations of the selected candidate share the observation horizon H⋆H and timestamps are non-decreasing, completion preserves the order of their origins. Therefore, for every m>n⋆m>n , (5) Km(g)=k1(g),…,kNm(g)(g).K_m^(g)= \k_1^(g),…,k_N_m^(g)^(g) \. Accordingly, the sample available at event index m consists exactly of Xk1(g),…,XkNm(g)(g)X_k_1^(g),…,X_k_N_m^(g)^(g). 6.5. Anytime-valid certification Certification statistics. For every enabled group g and every s,q≥1s,q≥ 1, define ps(g)=Pr(Xks(g)=1∣j,s−1(g)),p_s^(g)= \! (X_k_s^(g)=1 _j,s-1^(g) ), p¯q(g)=1q∑s=1qps(g),p^q(g)=1q∑s=1qXks(g). p_q^(g)= 1q _s=1^qp_s^(g), p_q^(g)= 1q _s=1^qX_k_s^(g). Because Xks(g)X_k_s^(g) is binary, ps(g)=[Xks(g)∣j,s−1(g)]p_s^(g)=E\! [X_k_s^(g) _j,s-1^(g) ] is also the predictable conditional success probability of the s-th outcome of group g. The quantity p¯q(g) p_q^(g) is the running average of these predictable conditional probabilities, while p^q(g) p_q^(g) is the corresponding observed frequency. By Equation (5), p^Nm(g)(g)=1Nm(g)∑k∈Km(g)Xk p_N_m^(g)^(g)= 1N_m^(g) _k∈ K_m^(g)X_k whenever Nm(g)>0N_m^(g)>0. Hence p^Nm(g)(g) p_N_m^(g)^(g) is precisely the observed success frequency of the outcomes of group g available at event index m. No stationarity or independence assumption is imposed on (ps(g))s≥1(p_s^(g))_s≥ 1. In particular, a certification sample may contain outcomes affected by a behavioural transition. At selection time, fix ℋjH_j-measurable error allocations δjall>0,δjcore≥0,δjall+δjcore≤δj. _j^all>0, _j^core≥ 0, _j^all+ _j^core≤ _j. If the protected trigger is ⊥ , the core group is disabled and δjcore=0 _j^core=0; otherwise δjcore>0 _j^core>0. Conditioning on ℋjH_j therefore fixes all enabled allocations before any post-selection outcome is observed. For every enabled group g and every q≥1q≥ 1, set δj,q(g)=6δj(g)π2q2,∑q≥1δj,q(g)=δj(g). _j,q^(g)= 6\, _j^(g)π^2q^2, _q≥ 1 _j,q^(g)= _j^(g). For Nm(g)>0N_m^(g)>0, define Lm(g)=max0,p^Nm(g)(g)−log(1/δj,Nm(g)(g))2Nm(g),L_m^(g)= \0,\; p_N_m^(g)^(g)- \! (1/ _j,N_m^(g)^(g) )2N_m^(g) \, and set Lm(g)=0L_m^(g)=0 when Nm(g)=0N_m^(g)=0. The bound targets the average predictable success probability of the outcomes actually used for certification rather than assuming a constant regime probability. When the core group is disabled, only the aggregate instance is defined and evaluated. Definition 0 (Statistical certification). The selected candidate ψ⋆ψ is statistically certified at event index m>n⋆m>n if Nm>0N_m>0, Lm≥λ⋆L_m≥λ , and, whenever core-conditional certification is enabled, Nmcore>0N_m^core>0, Lmcore≥λcoreL_m^core≥ _core. This predicate tests the selected candidate using completed post-selection outcomes. Passing it is a prerequisite for activation; evaluating it does not itself change the active specification. Masked core failure: why core-conditional certification is needed. Fix a specification ψj _j and a regime RrR_r satisfying Assumption 1. For each eligible origin index k, protected triggers and adaptive-only triggers partition the event ,k⊧trig(ψj)e,k ( _j) into the disjoint events ,k⊧φ1coree,k _1^core and ,k⊧φ1adapt∧¬φ1coree,k _1^adapt _1^core. Suppose both groups have positive probability, and their conditional probabilities below are independent of the eligible origin index k within RrR_r. Define wr w_r :=Pr(,k⊧φ1core∣,k⊧trig(ψj),Ek,rψj), := (e,k _1^core ,k ( _j),E_k,r _j), prcore p_r^core :=Pr(Xkψj=1∣,k⊧φ1core,Ek,rψj), := (X_k _j=1 ,k _1^core,E_k,r _j), pradapt p_r^adapt :=Pr(Xkψj=1∣,k⊧φ1adapt∧¬φ1core,Ek,rψj). := (X_k _j=1 ,k _1^adapt _1^core,E_k,r _j). The conditional success probabilities concern the full response, not the protected response component alone. The within-group stability assumption is additional to Assumption 1. By the law of total probability, conditioning on the full trigger and within-regime completion and then on this partition yields (6) pRr(ψj)=wrprcore+(1−wr)pradapt.p_R_r( _j)=w_rp_r^core+(1-w_r)p_r^adapt. If only the protected group has positive probability, the identity reduces to pRr(ψj)=prcorep_R_r( _j)=p_r^core; the adaptive-only conditional probability is then left undefined. If the protected group has zero probability, prcorep_r^core is not identified from this regime. In particular, when φ1core=⊥ _1^core= , core certification is disabled and only the aggregate quantity is used. The same decomposition applies to a fixed candidate ψ⋆ψ when the corresponding positivity and within-group assumptions hold; we denote its protected-group conditional probability in regime RrR_r by pRrcore(ψ⋆)p_R_r^core(ψ ). In what follows, aggregate-only certification denotes the ablation of Definition 2 obtained by omitting its core-conditional conjunct. It does not by itself identify the predictable means of its post-selection certification sample with a regime-level probability. The following proposition shows that aggregate certification alone can accept a candidate even when its full response fails systematically on every protected trigger. Proposition 0 (Masked core failure). There exist a protected decomposition, two regimes R0R_0 and R1R_1, and a candidate specification ψ⋆ψ such that pR0(ψ⋆)=pR1(ψ⋆),pR0core(ψ⋆)=0.99,pR1core(ψ⋆)=0.p_R_0(ψ )=p_R_1(ψ ), p_R_0^core(ψ )=0.99, p_R_1^core(ψ )=0. Moreover, if R1R_1 governs an infinite post-selection certification sequence, aggregate-only certification eventually certifies ψ⋆ψ almost surely, whereas the joint aggregate and core-conditional criterion of Definition 2 never certifies it. Remark 1 (Core-sample acquisition cost). Fix λcore∈[0,1) _core∈[0,1) and a core confidence allocation δjcore>0 _j^core>0. On a perfect-response stream, define N⋆:=minq≥1:1−log(π2q2/(6δjcore))2q≥λcore.N := \q≥ 1:1- \! (π^2q^2/(6 _j^core) )2q≥ _core \. Thus N⋆N is the minimum number of completed protected-trigger obligations required for the core conjunct Lmcore≥λcoreL_m^core≥ _core of Definition 2 on a stream with no observed core failures. Suppose that, along the ordered aggregate certification sequence (ks)s≥1(k_s)_s≥ 1, protected-trigger membership is independent across origins and has probability w>0w>0. Define TN⋆:=minq≥1:∑s=1q[,ks⊧φ1core]≥N⋆.T_N := \q≥ 1: _s=1^q1\! [e,k_s _1^core ]≥ N \. Hence TN⋆T_N is the aggregate sample size required to collect N⋆N completed protected-trigger obligations. It has a negative-binomial distribution, with [TN⋆]=N⋆w,Var(TN⋆)=N⋆(1−w)w2.E[T_N ]= N w, (T_N )= N (1-w)w^2. Therefore, under the perfect-response benchmark and for fixed λcore _core and δjcore _j^core, the expected number of completed aggregate obligations that must be examined before the core sample contains N⋆N outcomes, and hence before Lmcore≥λcoreL_m^core≥ _core can hold, scales as 1/w1/w. Thus the expected aggregate sample size is inversely proportional to the protected-trigger probability w: halving w doubles the expected number of completed aggregate obligations required to collect the same core sample. This is a sample-acquisition cost, not by itself the complete activation latency. Statistical certification also requires the aggregate conjunct, and converting a number of completed obligations into event time depends on trigger arrivals and completion delays. For the Hoeffding bound used here, if λcore=0.9 _core=0.9 and the transition budget δ0=0.025 _0=0.025 is split equally, then δ0core=0.0125 _0^core=0.0125 and a perfect-response stream gives N⋆=928N =928. With a protected-trigger share of w=0.01w=0.01, the expected number of completed aggregate obligations required to collect the 928928 protected outcomes is [TN⋆]=9280.01=92,800E[T_N ]= 9280.01=92,800. This calculation quantifies the additional evidence-collection latency introduced by core-conditional certification and makes explicit its main trade-off: stronger protection of a rare subgroup requires a larger aggregate sample. Choice of lower bound. The subsequent results do not depend on the specific Hoeffding formula; they require only that the lower bound cover p¯q(g) p_q^(g) simultaneously for all sample sizes q, conditionally on the selection-time information ℋjH_j. We use the stated Hoeffding bound (Hoeffding, 1963) because it admits the short self-contained proof given below. The bound is conservative. In the controlled i.i.d. Bernoulli experiment of Section 8.1, at true success probability 0.980.98, it required a median of 1,4611,461 completed obligations, compared with 240240 for an exact binomial test using the same spending schedule. The exact test, however, relies on the additional i.i.d. assumption and is not valid under the general history-dependent model used in the formal results. Any sharper lower bound satisfying the same simultaneous conditional coverage property could be substituted without changing the remaining arguments (Waudby-Smith and Ramdas, 2024). The next proposition establishes that each enabled lower bound covers its corresponding average predictable success probability simultaneously at every certification index. Proposition 0 (Anytime-valid lower confidence bound). For each enabled group g∈all,coreg∈\all,core\, conditionally on ℋjH_j, Pr(∀m>n⋆ with Nm(g)>0:p¯Nm(g)(g)≥Lm(g)|ℋj)≥1−δj(g). \! (∀ m>n with N_m^(g)>0:\; p_N_m^(g)^(g)≥ L_m^(g)\; |\;H_j )≥ 1- _j^(g). The core instance is omitted when core certification is disabled. Applying the preceding result to both enabled samples yields their simultaneous coverage without requiring independence between them. Proposition 0 (Simultaneous aggregate and core-conditional coverage). Conditionally on ℋjH_j, Pr(∀g∈all,core enabled,∀m>n⋆ with Nm(g)>0:p¯Nm(g)(g)≥Lm(g)|ℋj)≥1−δj. \! ( array[]c∀\,g∈\all,core\ enabled,\ ∀\,m>n with N_m^(g)>0:\\[2.84526pt] p_N_m^(g)^(g)≥ L_m^(g) array\; |\;H_j )≥ 1- _j. The core instance is omitted when core certification is disabled. No independence between the aggregate and core samples is required. Conditioning on ℋjH_j fixes the selected candidate and its protected-trigger predicate, but not the subsequent trigger origins or response outcomes. The coverage results therefore remain valid after adaptive candidate selection. They control the average predictable success probability p¯q(g) p_q^(g) of the certification sequence. They do not by themselves establish a fixed regime-level probability or the success probability of obligations generated after activation; those interpretations require the additional alignment or stability conditions stated below. The following corollary identifies the additional alignment condition under which simultaneous coverage of the certification samples admits a regime-level interpretation. Corollary 0 (Joint regime-level interpretation). Fix an event index m and a regime RrR_r. For the aggregate group, define pRr(all)(ψ⋆):=pRr(ψ⋆)p_R_r^(all)(ψ ):=p_R_r(ψ ) and λall:=λ⋆ _all:=λ . For the core group, when enabled, retain pRrcore(ψ⋆)p_R_r^core(ψ ) and λcore _core. Assume that pRr(g)(ψ⋆)p_R_r^(g)(ψ ) is well defined for every enabled group g. Suppose that, for every enabled group g∈all,coreg∈\all,core\ and every s≥1s≥ 1, n⋆<m,Nm(g)≥sps(g)=n⋆<m,Nm(g)≥spRr(g)(ψ⋆)a.s.1_\n <m,\;N_m^(g)≥ s\p_s^(g)=1_\n <m,\;N_m^(g)≥ s\p_R_r^(g)(ψ ) .s. Then, conditionally on ℋjH_j, Pr(n⋆<m,ψ⋆ is statistically certified at m,∃g∈all,core enabled:pRr(g)(ψ⋆)<λg|ℋj)≤δj. \! ( array[]cn <m,\;ψ is statistically certified at m,\\ ∃\,g∈\all,core\ enabled:p_R_r^(g)(ψ )< _g array\; |\;H_j )≤ _j. 6.6. Scope of the activation certificate The certificate controls p¯Nm(g)(g) p_N_m^(g)^(g), the average predictable success probability of the outcomes used at the certification index. A regime-level interpretation requires the alignment condition of Corollary 6. The first obligation generated under the successor version is not the next member of the certification sequence. Therefore, the certificate does not by itself control the success probability of obligations generated after activation. Such a conclusion requires an additional stability assumption. Indeed, two probability laws may agree on the entire observed prefix, including the certification samples, lower bounds, and activation decision, while assigning different success probabilities to subsequent obligations. For clarity, the remaining scope restrictions are collected here. Group membership must be compatible with the completed-outcome filtration; fixing a terminal-window length alone does not make a split predictable. Aggregate and core samples may overlap, and their coverage failures are combined by a union bound rather than an independence assumption. The present protocol allows one selected candidate per active version; repeated attempts require an additional predictable error allocation. Certification supplies no liveness guarantee and no future operational guarantee without an additional persistence assumption relating the certification regime to obligations generated after activation. A model-based or hybrid core certificate is admissible if it provides a valid lower bound on the protected-trigger conditional success probability and accounts for its estimation and repeated-use error within the lifetime budget. Aggregate model accuracy alone is insufficient: conditioning on a protected event of probability w may amplify a joint-law error of order εS _S to a conditional error of order εS/w _S/w. More generally, any additional outcome group must be defined so that its certification sequence satisfies the filtration conditions used by the confidence bound. 6.7. Certified activation The end-to-end architecture uses a drift declaration as a necessity gate for candidate selection, as formalized in Section 6.1. It is not a second condition checked at activation: structural admissibility is verified at selection, and once a candidate has been selected its activation depends on the post-selection certification evidence. On n⋆<∞\n <∞\, the governor monitors the fixed, structurally admissible candidate ψ⋆ψ without replacing the incumbent. Define the first eligible certification index by mjcert:=infm∈ℕ: m_j^cert:= \m : m>n⋆,Nm>0,Lm≥λ⋆, m>n ,\ N_m>0,L_m≥λ , (φ1core=⊥∨(Nmcore>0∧Lmcore≥λcore)), ( _1^core= \; \; (N_m^core>0\; \;L_m^core≥ _core ) )\, with inf∅=∞ =∞. If n⋆=∞n =∞, set mjcert=∞m_j^cert=∞. The core test in this definition retains both branches above: it is automatically true only for a specification without a protected trigger. An actual specification change occurs if and only if mjcert<∞m_j^cert<∞. On this event define ψj+1:=ψ⋆,nj+1:=mjcert+1,ψj⇒nj+1ψj+1. _j+1:=ψ , n_j+1:=m_j^cert+1, _j [n_j+1] _j+1. If mjcert=∞m_j^cert=∞, there is no successor version, nj+1=∞n_j+1=∞, and the index j does not advance. The certification decision is made after processing ≤mjcerte_≤ m_j^cert; the new version first governs emjcert+1e_m_j^cert+1. Hence the incumbent ψj _j remains active throughout the selection and certification phases, and the first successful certification test—not the drift alarm or proposal—activates the modification. 6.8. Lifetime guarantee For each possible specification-version transition j, let the total error level δj∈(0,1) _j∈(0,1) be chosen no later than the selection time represented by ℋjH_j. Thus δj _j and its split δjall,δjcore _j^all, _j^core are deterministic or ℋjH_j-measurable and cannot depend on certification outcomes revealed after selection. Assume that, almost surely, ∑j=0∞δj≤δ _j=0^∞ _j≤δ for a fixed lifetime budget δ∈(0,1)δ∈(0,1). Only a finite mjcertm_j^cert creates ψj+1 _j+1. For a version index never reached, or when no candidate is selected or certified, all failure events below are empty. On a run where activation occurs, define Fjall=ψ⋆ is activated and p¯Nnj+1−1<λ⋆.F_j^all= \ψ is activated and p_N_n_j+1-1<λ \. When core-conditional certification is enabled, define Fjcore=ψ⋆ is activated and p¯Nnj+1−1corecore<λcore;F_j^core= \ψ is activated and p^core_N_n_j+1-1^core< _core \; otherwise set Fjcore=∅F_j^core= . Set Fj=Fjall∪FjcoreF_j=F_j^all∪ F_j^core, and Fj=∅F_j= whenever ψj _j is not reached or no successor is activated. Thus FjF_j concerns only activated candidates whose aggregate or (when enabled) core predictable-mean requirement fails at the activation decision. It does not assert regime validity at activation, success of future obligations, or eventual adaptation. The per-transition coverage guarantee extends to the entire sequence of activated versions by allocating a summable error budget across version transitions. Theorem 7 (Proposer-independent lifetime certification). For each version index j≥0j≥ 0, suppose that at most one candidate is selected while ψj _j is active and that, whenever selection occurs, the conditions of Proposition 5 hold with error budget δj _j. Suppose also that each δj _j is fixed no later than selection time and that ∑j=0∞δj≤δ _j=0^∞ _j≤δ almost surely for some δ∈(0,1)δ∈(0,1). Then Pr(⋃j=0∞Fj)≤δ. \! ( _j=0^∞F_j )≤δ. The lifetime bound is independent of the architecture, training procedure, and randomization of the proposer, provided that the selected candidate is ℋjH_j-measurable and is fixed before any post-selection certification outcome is observed. In particular, the protected-trigger predicate defining the core sample cannot be modified during certification. Candidate multiplicity, sample overlap, repeated attempts, and liveness are subject to the restrictions collected in Section 6.6. The theorem itself controls only the unconditional probability of an erroneous activated revision at its decision index. 7. End-to-End Architecture and Algorithm The preceding sections define admissible revisions, candidate selection, post-selection certification, and certified activation. We now state how these components are executed at each event index. The protocol uses the completed-obligation interface and does not assume any transfer of internal monitor states between specification versions. Monitoring across specification versions. For every origin index k, there is a unique specification version ψi _i such that ni≤k<ni+1n_i≤ k<n_i+1. The trigger status, response outcome, and completion index of the obligation originating at k are evaluated using this origin version ψi _i. Consequently, after ψi+1 _i+1 becomes active, ψi _i remains responsible for completing obligations whose origins precede ni+1n_i+1, but it generates no obligations at later origins. This distinction is necessary because an obligation may be completed after its origin version has ceased to be active. In particular, a trigger or response containing future-time operators may become decidable only after a later version has been activated. The subsequent activation does not alter the trigger, response, interval, or outcome attached to the earlier origin. A selected candidate ψ⋆ψ is monitored separately before activation. Its certification-only monitor evaluates candidate obligations with origins k>n⋆k>n and supplies their completed outcomes to the aggregate and, when enabled, core certification samples. These outcomes are certification evidence. They are not reclassified as operational obligations generated under ψ⋆ψ if the candidate is later activated. Figure 1. Ordered governor protocol at event index n.An ordered phase table showing how origin-version obligations, candidate certification, activation, and proposal generation are processed at each event index. Step Phase Condition Governor action 1 Observe Every event ene_n Advance all unresolved origin-version obligations. Record every trigger status and response outcome that becomes observable at n, using the specification version under which the corresponding obligation originated. Update the detector for the active specification ψj _j. 2 Certify A candidate ψ⋆ψ has been selected Advance the certification-only monitor on candidate origins k>n⋆k>n . Add newly completed outcomes to the aggregate sample and, when enabled, to the core sample. Evaluate LnL_n and LncoreL_n^core. 3 Activate ψ⋆ψ satisfies Definition 2 for the first time at n Set mjcert=nm_j^cert=n, ψj+1=ψ⋆ _j+1=ψ , and nj+1=n+1n_j+1=n+1. The new version governs origins from n+1n+1 onward. Obligations with earlier origins retain their origin versions. 4 Propose a drift declaration occurs at n and no candidate has yet been selected while ψj _j is active Obtain n,jP_n,j, discard every candidate that fails ψjℛψ _j Rψ, select at most one survivor, fix its error allocation, set n⋆=n =n, and start prospective certification. 5 Continue Neither activation nor candidate selection occurs Keep ψj _j active. Continue resolving obligations under their origin versions. A drift declaration, proposal, or admissibility check alone does not change the active specification. Execution order. The rows of Figure 1 are evaluated in order. First, the governor processes ene_n and resolves every obligation outcome that becomes observable at that event index. If a candidate has already been selected, these newly available outcomes may enlarge its certification samples and change its lower bounds. Activation is then checked before a new proposal is considered. If the candidate first satisfies the certification condition at n, the certification decision uses only the prefix ≤ne_≤ n and the successor version first governs event en+1e_n+1. Thus nj+1=mjcert+1n_j+1=m_j^cert+1. No obligation with origin at or before mjcertm_j^cert is retroactively assigned to ψj+1 _j+1. If no candidate has been selected and no activation occurs, a drift declaration may enable proposal generation. Selection fixes ψ⋆ψ , n⋆n , and its error allocation using information available at that time. Certification then uses only completed obligations whose origins satisfy k>n⋆k>n . Proposal and selection do not alter ψj _j. The three indices therefore have distinct meanings: n⋆n selects the candidate, mjcertm_j^cert records the certification decision, nj+1n_j+1 starts the successor version. Guarantees enforced by the protocol. Every activated successor satisfies the admissible-revision relation. Therefore, the protected trigger and response components are unchanged and the parameter tuple remains inside the designer-fixed envelope throughout the activated version sequence. The certification samples are separated from the prefix used to select the candidate. At activation, the aggregate lower bound controls the average predictable success probability of the completed aggregate outcomes used by the decision. When core certification is enabled, the core lower bound simultaneously controls the corresponding average on protected triggers. The aggregate and core samples may overlap; their failure probabilities are combined through their error allocations, without an independence assumption. For transition j, the allocation δj _j and its aggregate/core split are fixed at selection time. For example, δj=δ2j+1 _j= δ2^j+1 gives ∑j=0∞δj≤δ _j=0^∞ _j≤δ. Consequently, over the sequence of activated versions, the probability that some activated candidate fails its aggregate or enabled core predictable-mean requirement at its activation decision is at most δ. This guarantee concerns the completed certification outcomes available at the decision index. Obligations generated after activation are not the next members of the certification sequence. Interpreting the certificate as a statement about a regime or about successor-version operational obligations requires the additional alignment condition stated in Corollary 6. Runtime overhead and liveness. While a candidate is being certified, the active specification and the selected candidate are monitored in parallel. In addition, earlier specification versions may still have unresolved origin-version obligations. Once all obligations attributed to an earlier version have been resolved, no further monitoring work is required for that version. The detector continues to update while certification is active, but further declarations do not select another candidate. Under the single-attempt-per-version rule, a selected candidate that never certifies may therefore prevent further adaptation while the incumbent remains active. Repeated attempts would require an additional attempt index and a predictable allocation of δj _j across attempts. 8. Experimental evaluation The evaluation contains three controlled synthetic experiments and a monitored case study, each tied to a stated result. RQ1 illustrates the optional-continuation protection of Proposition 4 and quantifies the conservativeness of the Hoeffding bound. RQ2 illustrates the masked-core counterexample of Proposition 3 at a single activation decision. RQ3 exercises repeated proposal and certification under the lifetime schedule of Theorem 7. The proposer. All three experiments and the case study use the same proposer: a supervised regressor trained offline on 4,000 independent synthetic tasks and frozen before any experiment is run. It receives the prefix aggregate frequency, the trigger coverage, the threshold, and two structural indicators, and predicts a candidate’s aggregate margin. It never receives the protected-trigger success rate. The masked-core failures reported below are therefore produced by a proposer optimising the quantity it can observe, not by an adversary constructed to defeat the governor; responsibility for the protected group rests with the certification rule, not with the proposer. All experiments use one selected candidate and one certification attempt per active version, as required by the protocol in Figure 1. Censored runs are those in which the candidate is not certified by the finite horizon. Wilson intervals below quantify Monte Carlo variation across replications; they are not confidence-sequence bounds. The accompanying script fixes all seeds and regenerates the reported tables, figures, and per-run outputs. 8.1. RQ1: optional continuation and finite-sample latency Question. Does fresh post-selection sampling prevent prefix selection from entering the certificate, and what finite-sample latency is introduced by anytime-valid inspection? This experiment illustrates optional continuation and the conservativeness of the Hoeffding bound; it is not a separate contribution and is reported as a single table. An independent prefix selects the empirically best of eight candidates; the compared rules then receive identical fresh Bernoulli outcomes. Across 1,000 replications, we compare direct activation, repeated misuse of a fixed-time exact test, an exact test with spending, and the paper’s Hoeffding rule. The complete protocol and seeds are provided with the artifact. Table 1 summarizes the activation frequencies and the median numbers of completed post-selection obligations at activation. Table 1. RQ1 synthetic post-selection certification. Each row has 1000 independent replications and 6,000 completed-obligation opportunities. Wilson intervals measure Monte Carlo variation; q is the median completed count at activation. True p Procedure Activations Wilson 95% (%) Median q Censored 0.890 Direct proposal 1000/1000 [99.6, 100.0] 0 0 Fixed-time, repeatedly tested 56/1000 [4.3, 7.2] 107 944 Exact test with spending 0/1000 [0.0, 0.4] – 1000 Paper’s Hoeffding bound 0/1000 [0.0, 0.4] – 1000 0.899 Direct proposal 1000/1000 [99.6, 100.0] 0 0 Fixed-time, repeatedly tested 190/1000 [16.7, 21.5] 249 810 Exact test with spending 0/1000 [0.0, 0.4] – 1000 Paper’s Hoeffding bound 0/1000 [0.0, 0.4] – 1000 0.980 Direct proposal 1000/1000 [99.6, 100.0] 0 0 Fixed-time, repeatedly tested 1000/1000 [99.6, 100.0] 54 0 Exact test with spending 1000/1000 [99.6, 100.0] 240 0 Paper’s Hoeffding bound 1000/1000 [99.6, 100.0] 1,461 0 At the below-threshold probabilities p=0.890p=0.890 and p=0.899p=0.899, direct proposal accepts every candidate, while repeated use of the unadjusted fixed-level test activates in 56/1,000 and 190/1,000 runs. Neither spent procedure activates in these simulations. At the above-threshold probability p=0.98p=0.98, all three statistical procedures eventually activate, but their median completed sample sizes are 5454, 240240, and 1,4611,461 for the repeatedly inspected fixed-level test, the spent exact test, and the Hoeffding bound, respectively. The experiment illustrates the protection required for sequential inspection and the finite-sample cost of the Hoeffding bound; it is not a separate theoretical contribution. 8.2. RQ2: masked-core failure Question. Can an aggregate-oriented AI proposal pass aggregate certification while systematically failing on protected triggers, and does joint certification block it? Write pcorep^core for the protected-group success probability and suppose non-protected responses always succeed. Equation (6) then gives p=1−w+wpcore.p=1-w+wp^core. Asymptotic aggregate certification requires p>λp>λ, whereas core-conditional support fails when pcore<λcorep^core< _core. The masked-core region is therefore (7) pcore∈[0,1]:pcore>1−1−λw,pcore<λcore. \p^core∈[0,1]:p^core>1- 1-λw, p^core< _core \. Its width is max0,λcore−max(0,1−1−λw). \! \0, _core- \! (0,1- 1-λw ) \. The width increases as the lower endpoint decreases but saturates when that endpoint reaches zero; unlike the sampling latency of Remark 1, it does not globally scale as 1/w1/w. Varying the protected share. At event times tn=nt_n=n, trigger A occurs every three events. Conditional on A, protected predicate C occurs independently with probability w. We test w=0.01w=0.01, 0.030.03, 0.050.05, and 0.070.07. Candidate response B is checked at the next event, with λ=λcore=0.9λ= _core=0.9. Every protected response fails and every non-protected response succeeds, so the aggregate probability is 1−w≥0.931-w≥ 0.93. A drift declaration is supplied exogenously to isolate the certification mechanism. A frozen random-forest proposer, trained on 4,000 independent synthetic tasks, selects between the admissible full trigger and its core-only restriction from a separate prefix. Its features contain the aggregate empirical frequency, trigger coverage, threshold, and structural indicators, but no protected-group outcome frequency. Aggregate-only and joint certification see the same 200 streams at each w, up to 45,000 event indices. The proposer selects the full-trigger candidate in all 200 independent prefixes at every tested value of w. This constructed masked-core setting makes the full trigger attractive in aggregate, so it is not by itself an informative accuracy test for the proposer. We therefore audit the same frozen model on 500 independent, deliberately closer four-candidate ranking tasks, varying both adaptive trigger retention and an adaptive response conjunct. Table 2 reports 65 ranking errors and mean true-margin regret 0.00350.0035. These errors make the proposer genuinely fallible while remaining separate from the certification samples; proposer accuracy is descriptive and is not an assumption of the guarantee. Table 2. Independent ranking audit of the frozen RQ2 proposer. Tasks Exact rankings Ranking errors Mean margin regret 500 435 65 0.0035 Core-unsupported activation rate against protected-trigger share. The aggregate-only curve is high, whereas the aggregate-plus-core curve remains at zero. Figure 2. Activations within the finite horizon when protected responses always fail. Each point uses 200 paired streams; bars show Wilson 95% intervals.Core-unsupported activation rate against protected-trigger share. The aggregate-only curve is high, whereas the aggregate-plus-core curve remains at zero. Table 3. RQ2 masked-core experiment with proposals selected by the frozen supervised proposer. A below-core activation occurs while pcore<λcorep^core< _core; brackets give Wilson 95% intervals. w Certification rule Below core Wilson 95% Median event 0.01 Aggregate only 200/200 [98.1, 100.0] 3,305 0.01 Aggregate + core 0/200 [0.0, 1.9] – 0.03 Aggregate only 200/200 [98.1, 100.0] 5,795 0.03 Aggregate + core 0/200 [0.0, 1.9] – 0.05 Aggregate only 200/200 [98.1, 100.0] 12,329 0.05 Aggregate + core 0/200 [0.0, 1.9] – 0.07 Aggregate only 167/200 [77.7, 88.0] 36,158 0.07 Aggregate + core 0/200 [0.0, 1.9] – Figure 2 and Table 3 show aggregate-only activation in every run for w≤0.05w≤ 0.05 and in 167/200 runs for w=0.07w=0.07. joint certification never activates because its core lower bound remains zero. The 33 aggregate-only runs censored at w=0.07w=0.07 reflect the smaller finite-horizon margin 1−w−λ=0.031-w-λ=0.03, not absence of the masked-core phenomenon. Varying protected success. We next fix w=0.2w=0.2 and test pcorep^core at 00, 0.50.5, 0.80.8, 0.880.88, 0.920.92, 0.950.95, and 0.990.99, using 100 paired replications and a horizon of 150,000 event indices. Equation (7) gives the open theoretical interval (0.5,0.9)(0.5,0.9). Two plots show activation rates and median core evidence as the protected success probability increases. Figure 3. Activation rates against protected success at w=0.2w=0.2 (left) and median completed protected obligations at joint activation (right). The dotted line is λcore _core.Two plots show activation rates and median core evidence as the protected success probability increases. Table 4. RQ2 protected-success sweep at w=0.20w=0.20. A dash means that no run activated within the horizon. pcorep^core Aggregate-only activations Joint activations Joint median core q Joint censored 0.00 0/100 0/100 – 100 0.50 0/100 0/100 – 100 0.80 100/100 0/100 – 100 0.88 100/100 0/100 – 100 0.92 100/100 0/100 – 100 0.95 100/100 100/100 4,177 0 0.99 100/100 100/100 1,160 0 Figure 3 and Table 4 report the activation frequencies and the completed core sample sizes across the protected-success sweep. At 0.80.8 and 0.880.88, inside the window, aggregate-only certification activates in 100/100 runs and joint certification in none. The value 0.50.5 is the aggregate boundary and neither rule activates. The value 0.920.92 is outside the masked-core region and is genuinely core-compliant, but remains censored under joint certification at this finite horizon, whose Hoeffding bound is conservative near the threshold. At 0.950.95 and 0.990.99, joint certification activates in every run, after medians of 4,177 and 1,160 protected obligations respectively. Thus censoring near the threshold is a finite-horizon liveness effect, not evidence that the candidate violates the protected requirement. 8.3. RQ3: sequential governed evolution Question. Does joint certification continue to prevent masked-core activations when an AI proposer repeatedly revises the specification over one evolving history? The third experiment exercises the complete loop. The two-window detector of Section 6.1 initiates proposal; the frozen supervised proposer ranks the formally admissible neighbourhood; and the governor applies δj=δ/2j+1 _j=δ/2^j+1 across successive transitions. Candidate generation changes at most one adaptive structural component per transition. Open obligations retain the trigger, response, and temporal parameters of their origin version. Across four regimes the protected success probability follows 0.99→0.97→0.80→0.550.99→ 0.97→ 0.80→ 0.55, while non-protected responses remain easy. We use w=0.3w=0.3, horizon 120,000, λcore=0.9 _core=0.9, parameter envelope 0.95,0.92,0.90\0.95,0.92,0.90\, and 100 paired histories. The proposer predicts each candidate’s aggregate margin from prefix-level aggregate features and never receives the protected success frequency. Training data, model seed, and simulation seeds are fixed independently of the certification samples. Aggregate-only certification activates in below-core regimes; joint certification does not. The protected success schedule decreases across four regimes. Figure 4. Sequential experiment. Left: mean certified activations and activations occurring while the synthetic current regime is below the core threshold. Right: protected-success schedule.Aggregate-only certification activates in below-core regimes; joint certification does not. The protected success schedule decreases across four regimes. Table 5. RQ3 sequential experiment with the frozen supervised AI proposer. ‘Below core’ counts runs with at least one activation during a regime where pcore<λcorep^core< _core. Certification rule Mean activations Mean proposals Below core Sample-target failure Aggregate only 4.82 5.82 27/100 0/100 Aggregate + core 2.68 3.68 0/100 0/100 Figure 4 and Table 5 summarize the activation counts and the protected-success schedule across the paired histories. Aggregate-only certification produces 4.82 activations per history on average and activates while the current regime is below the protected threshold in 27/100 histories. joint certification produces 2.68 activations on average and never does so in these runs. This is the masked-core mechanism operating across a sequence rather than at one decision. The two diagnostics in Table 5 must not be conflated. The lifetime theorem controls activation when the average predictable mean of the certification sample is below its threshold; no such sample-target failure was observed under either certification rule. Whether the synthetic current regime is below the core threshold is a different operational diagnostic, because a certification sample may cross a regime boundary. The experiment therefore illustrates repeated governed decisions under the theorem’s schedule; it neither estimates the lifetime error probability nor proves future operational validity. 8.4. Monitored clinical-alarm case study and runtime cost This case study instantiates the clinical-alarm scenario of Section 1 with an executable bounded-response monitor, rather than sampling obligation outcomes directly. Proposition A denotes a desaturation alarm, C the protocol-critical subset, and B a documented intervention. Alarm origins are separated by more than the largest response horizon so that each intervention is attributable to one obligation. The trace contains 30,000 alarms; protected alarms occur with probability 0.10.1, and full-response probabilities are 0.600.60 and 0.990.99 for protected and non-protected alarms, respectively. The executable monitor evaluates the incumbent and candidate formulas ψ0=A⇒0.9,[1,3]B,ψ⋆=A⇒0.9,[1,8]B, _0=A _0.9,[1,3]B, ψ =A _0.9,[1,8]B, with designer-protected trigger A∧CA C and protected response B. Starting from the incumbent window [1,3][1,3], the frozen supervised proposer ranks an admissible [1,8][1,8] revision using an independent 1,000-obligation prefix. A second proposed revision that removes the protected response B is rejected by structural admissibility before statistical ranking. The selected candidate is then monitored prospectively on the Boolean timed trace. Table 6 reports the resulting certificates and the median of nine reference runs of the executable monitor. Table 6. Monitored clinical-alarm case study and reference runtime. Quantity Result Completed alarm obligations 30,000 Observed protected share 0.099 Candidate aggregate success 0.953 Candidate protected success 0.608 Aggregate-only activation sample 3,321 Joint activation not activated Pending outcome: origin / retroactive 1 / 0 Baseline / governed median runtime 72.0 / 217.6 ms Baseline / governed time per event 0.240 / 0.725 μ Baseline / governed peak memory 30.9 / 60.3 KiB Baseline / governed peak pending 1 / 2 Parallel-governor increment 145.6 ms Reference runtime ratio 3.02× The widened candidate has aggregate success 0.9530.953 but protected success 0.6080.608. Aggregate-only certification activates after 3,321 completed post-selection obligations; joint certification never activates because the core conjunct remains unsupported. A pending alarm whose intervention occurs six events after its origin succeeds under its origin window [1,8][1,8] but would fail under a retroactively substituted [1,3][1,3] window, producing the reported 1/01/0 outcome pair and exercising Theorem 2. The reference timings in the table compare the non-adaptive incumbent monitor with concurrent incumbent and candidate monitors plus group classification, sequential lower bounds, and the activation check. The governed run uses 0.7250.725 rather than 0.2400.240 microseconds per trace event, peaks at 60.360.3 rather than 30.930.9 KiB of Python-tracked allocations, and has at most two rather than one pending obligations because the two monitors run in parallel. Absolute timings are machine-dependent; the artifact regenerates all measurements and retains the obligation counts and decisions as reproducible outputs. The case study therefore exercises the actual obligation interface and both main failure mechanisms. It remains semi-synthetic: its probabilities encode a realistic alarm workflow but are not estimates from patient data. 8.5. Artifact and reproducibility statement The reproducibility artifact is publicly available at https://github.com/ruggerolanotte/protected-cores-artifact. The artifact contains one Python program and requires Python 3.10+, NumPy, SciPy, Matplotlib, and scikit-learn. The command consists of python scripts/fac_experiments.py, followed by one of rq1, rq2, rq3, or case, and --out DIR; these targets regenerate every manuscript table and figure; the all target runs the complete suite and all --quick performs an interface smoke test. All random seeds, model-training sizes, horizons, and confidence allocations are command-line parameters with manuscript defaults. RQ2 and RQ3 archive the paired per-run records, while the case study archives its monitored counts, activation indices, pending-obligation regression result, and reference timings. 9. Conclusion We presented a framework for the certified evolution of temporal specifications under an untrusted AI proposer. The proposer suggests parametric or structural revisions; a symbolic governor checks their admissibility and requires post-selection evidence before activation. Two results organize the framework. Origin-version semantics prevents a revision from changing the outcome of obligations generated under an earlier version. The masked-core counterexample shows that aggregate certification can admit a candidate that fails systematically on protected triggers; adding core-conditional certification addresses this failure mode. A protected-envelope invariant supports admissible revisions, while a proposer-independent lifetime theorem bounds erroneous certifications relative to the predictable means of completed samples, including when aggregate and protected samples overlap. Controlled experiments and a monitored clinical-alarm case study use a frozen supervised proposer to illustrate the masked-core failure at one decision and across repeated governed transitions, while also measuring the cost of prospective certification. Section 6.6 states the condition under which a certificate transfers to obligations generated after activation, and records that it must be assumed rather than inferred: two laws may agree on the entire observed prefix and differ afterwards. That condition is not a third activation guarantee, and the experiments do not infer it from a finite prefix. Acknowledgements. The authors acknowledge the use of ChatGPT (OpenAI) during the preparation of this manuscript to assist with manuscript organization, preliminary reformulation of selected definitions and technical arguments, and language revision. All technical content, proofs, and references were independently reviewed and verified by the authors, who take full responsibility for the final manuscript. References Alur and Henzinger (1993) R. Alur and T. A. Henzinger Real-time logics: complexity and expressiveness. Information and Computation 104 (1), p. 35–77. External Links: Document Cited by: §3.2. Bauer et al. (2011a) A. Bauer, M. Leucker, and C. Schallhart Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology 20 (4), p. 14:1–14:64. External Links: Document Cited by: §1, §2. Bauer et al. (2011b) A. Bauer, M. Leucker, and C. Schallhart Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology 20 (4), p. 14:1–14:64. External Links: Document Cited by: §3.2. Berk et al. (2013) R. Berk, L. Brown, A. Buja, K. Zhang, and L. Zhao Valid post-selection inference. The Annals of Statistics 41 (2), p. 802–837. External Links: Document Cited by: §2. Bombara and Belta (2018) G. Bombara and C. Belta Online learning of temporal logic formulae for signal classification. In 2018 European Control Conference (ECC), New York, NY, USA, p. 2057–2062. External Links: Document Cited by: §2. Bombara and Belta (2021) G. Bombara and C. Belta Offline and online learning of signal temporal logic formulae using decision trees. ACM Transactions on Cyber-Physical Systems 5 (3), p. 22:1–22:23. External Links: Document Cited by: §2. Carwehl et al. (2023) M. Carwehl, T. Vogel, G. N. Rodrigues, and L. Grunske Runtime verification of self-adaptive systems with changing requirements. In 2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), New York, NY, USA, p. 104–114. External Links: Document Cited by: §1, §2. Cherian and Candès (2024) J. J. Cherian and E. J. Candès Statistical inference for fairness auditing. Journal of Machine Learning Research 25 (149), p. 1–49. Cited by: §2. Demir and Ulus (2026) A. Demir and D. Ulus Multi-property temporal logic monitoring. External Links: 2605.13668, Link Cited by: §2. Galesloot et al. (2026) M. F. L. Galesloot, T. Rhemrev, and N. Jansen Robust probabilistic shielding for safe offline reinforcement learning. External Links: 2605.10293, Link Cited by: §2. Gama et al. (2014) J. Gama, I. Žliobaitė, A. Bifet, M. Pechenizkiy, and A. Bouchachia A survey on concept drift adaptation. ACM Computing Surveys 46 (4), p. 44:1–44:37. External Links: Document Cited by: §1, §2. Hoeffding (1963) W. Hoeffding Probability inequalities for sums of bounded random variables. Journal of the American Statistical Association 58 (301), p. 13–30. External Links: Document Cited by: §6.5. Howard et al. (2021) S. R. Howard, A. Ramdas, J. McAuliffe, and J. Sekhon Time-uniform, nonparametric, nonasymptotic confidence sequences. The Annals of Statistics 49 (2), p. 1055–1080. External Links: Document Cited by: §2. le Court et al. (2026) E. H. le Court, T. Badings, A. Abate, F. Belardinelli, and F. Fabiano Robust shielding for safe reinforcement learning. External Links: 2606.00270, Link Cited by: §2. Maler and Nickovic (2004) O. Maler and D. Nickovic Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Lecture Notes in Computer Science, Vol. 3253, Berlin, Heidelberg, p. 152–166. External Links: Document Cited by: §1, §2, §3.2. Perotti et al. (2015) A. Perotti, A. S. d’Avila Garcez, and G. Boella Neural-symbolic monitoring and adaptation. In 2015 International Joint Conference on Neural Networks (IJCNN), New York, NY, USA, p. 1–8. External Links: Document Cited by: §1, §2. Platzer (2024) A. Platzer Intersymbolic AI: interlinking symbolic AI and subsymbolic AI. In Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Cham, p. 162–180. Cited by: §2. Podkopaev and Ramdas (2022) A. Podkopaev and A. Ramdas Tracking the risk of a deployed model and detecting harmful distribution shifts. In International Conference on Learning Representations (ICLR), Virtual. Cited by: §2. Prinster et al. (2025) D. Prinster, X. Liu, S. Saria, and A. Cheng WATCH: adaptive monitoring for AI deployments via weighted-conformal martingales. In Proceedings of the 42nd International Conference on Machine Learning (ICML), Vancouver, Canada, p. 1–25. Cited by: §2. Quansah and Bonnah (2026) P. K. Quansah and E. Bonnah SENTIL: a runtime verification tool for probabilistic temporal logic. External Links: 2605.21676, Link Cited by: §2. Sadigh and Kapoor (2016) D. Sadigh and A. Kapoor Safe control under uncertainty with probabilistic signal temporal logic. In Proceedings of Robotics: Science and Systems, Ann Arbor, Michigan. External Links: Document Cited by: §1, §2. Sengupta (2026) B. Sengupta Self-evolving agents with anytime-valid certificates. External Links: 2607.00871, Link Cited by: §2. Waudby-Smith and Ramdas (2024) I. Waudby-Smith and A. Ramdas Estimating means of bounded random variables by betting. Journal of the Royal Statistical Society Series B: Statistical Methodology 86 (1), p. 1–27. External Links: Document Cited by: §2, §6.5. Wu et al. (2025) X. Wu, S. Yin, Y. Kang, X. Zhang, Q. Xu, Z. Chen, and W. Zhang SGM: a statistical gödel machine for risk-controlled recursive self-modification. External Links: 2510.10232, Link Cited by: §2. Appendix A Proofs A.1. Proof of Theorem 2 Proof. The claim is immediate for i=0i=0. Suppose it holds for ψi _i and ψiℛψi+1 _i R _i+1. By Definition 1, the two protected components are copied unchanged into ψi+1 _i+1 and its parameter tuple remains in parA_par. Moreover, trig(ψi+1)=φ1core∨φ1,i+1adapttrig( _i+1)= _1^core _1,i+1^adapt, so every occurrence of the protected trigger satisfies the derived trigger, and resp(ψi+1)=φ2core∧φ2,i+1adaptresp( _i+1)= _2^core _2,i+1^adapt, so every successful derived response satisfies the protected response. Induction completes the proof. ∎ A.2. Proof of Theorem 2 Proof. The trigger is evaluated as ,k⊧trig(ψj)e,k ( _j). When it holds, the outcome is Xkψj=[∃m≥k:tm−tk∈[aj,bj]∧,m⊧resp(ψj)].X_k _j=1\! [∃ m≥ k:t_m-t_k∈[a_j,b_j] ,m ( _j) ]. The completion index is cψj(k)c_ _j(k) as defined in the statement; it is finite because H(ψj)<∞H( _j)<∞ and timed streams are non-Zeno. All three expressions use the fixed origin specification ψj _j and the same timed stream e; none depends on a subsequent revision. Each origin index has a unique active specification by the activation-interval convention, which establishes unique attribution as well. ∎ A.3. Proof of Proposition 3 Proof. Let A,C,B∈A,C,B , and consider the protected decomposition φ1core=A∧C,φ1adapt=A∧¬C,φ2core=B,φ2adapt=⊤. _1^core=A C, _1^adapt=A C, _2^core=B, _2^adapt= . Take ψ⋆:=((A∧C)∨(A∧¬C))⇒0.9,[a,b](B∧⊤).ψ := ((A C) (A C) ) _0.9,[a,b](B ). Then trig(ψ⋆)=(A∧C)∨(A∧¬C)=A,resp(ψ⋆)=B.trig(ψ )=(A C) (A C)=A, (ψ )=B. Thus each obligation is generated exactly when A holds. We may therefore restrict the remainder of the argument to the sequence of A-triggered obligations. Let the designer-fixed protected threshold be λcore=0.9 _core=0.9. We now construct an explicit timed-stream law. Place the origins of A-triggered obligations at deterministic times separated by more than H(ψ⋆)H(ψ ). This prevents the response assigned to one obligation from affecting any other obligation. Choose regime R0R_0 to contain a nonempty finite collection of such obligations, each completed within R0R_0, and let R1R_1 contain an infinite sequence of completed obligations with origins k1<k2<⋯k_1<k_2<·s. For every A-triggered obligation in either regime, independently draw Gs∼Bern(0.01)G_s (0.01) and set C true at its origin if and only if Gs=1G_s=1. Hence Gs=1,for a protected trigger A∧C,0,for an adaptive-only trigger A∧¬C,G_s= cases1,&for a protected trigger A C,\\ 0,&for an adaptive-only trigger A C, cases and protected triggers have conditional share Pr(Gs=1)=Pr(,ks⊧C∣,ks⊧A)=0.01. (G_s=1)= \! (e,k_s C ,k_s A )=0.01. In regime R0R_0, independently of the group indicators, draw Ys∼Bern(0.99)Y_s (0.99) and make B true within the response window of obligation s if and only if Ys=1Y_s=1. Consequently, Xksψ⋆=YsX_k_s^ψ =Y_s in R0R_0, independently of whether the trigger is protected or adaptive-only. Therefore, PrR0(Xksψ⋆=1∣Gs=1)=PrR0(Xksψ⋆=1∣Gs=0)=0.99. _R_0\! (X_k_s^ψ =1 G_s=1 )= _R_0\! (X_k_s^ψ =1 G_s=0 )=0.99. It follows that pR0core(ψ⋆)=0.99andpR0(ψ⋆)=0.01⋅0.99+0.99⋅0.99=0.99.p_R_0^core(ψ )=0.99 p_R_0(ψ )=0.01· 0.99+0.99· 0.99=0.99. In regime R1R_1, use the same group law but make B true within the response window of obligation s if and only if Gs=0G_s=0. Equivalently, Xksψ⋆=1−Gs.X_k_s^ψ =1-G_s. Thus every protected-trigger obligation fails and every adaptive-only obligation succeeds: PrR1(Xksψ⋆=1∣Gs=1)=0,PrR1(Xksψ⋆=1∣Gs=0)=1. _R_1\! (X_k_s^ψ =1 G_s=1 )=0, _R_1\! (X_k_s^ψ =1 G_s=0 )=1. Hence pR1core(ψ⋆)=0,p_R_1^core(ψ )=0, whereas the aggregate probability remains pR1(ψ⋆)=0.01⋅0+0.99⋅1=0.99=pR0(ψ⋆).p_R_1(ψ )=0.01· 0+0.99· 1=0.99=p_R_0(ψ ). Suppose now that candidate selection occurs before any outcome generated in R1R_1 is observed. Since the variables (Gs)s≥1(G_s)_s≥ 1 are independent Bernoulli variables with parameter 0.010.01, the aggregate outcomes (Xksψ⋆)s≥1=(1−Gs)s≥1 (X_k_s^ψ )_s≥ 1=(1-G_s)_s≥ 1 are independent Bernoulli variables with parameter 0.990.99. By the strong law of large numbers, p^q=1q∑s=1qXksψ⋆⟶0.99almost surely. p_q= 1q _s=1^qX_k_s^ψ 0.99 surely. For every fixed aggregate error allocation δjall>0 _j^all>0, the radius of the aggregate lower bound satisfies log(π2q2/(6δjall))2q⟶0. \! (π^2q^2/(6 _j^all) )2q 0. Consequently, Lτq>0.9L_ _q>0.9 for all sufficiently large q, almost surely. Aggregate-only certification therefore eventually certifies ψ⋆ψ almost surely. Because Pr(Gs=1)=0.01>0 (G_s=1)=0.01>0, protected triggers occur infinitely often almost surely. Every outcome in the resulting core subsequence equals zero. Therefore, for every nonempty core sample, p^qcore=0,Lτqcorecore=0<λcore. p_q^core=0, L_ _q^core^core=0< _core. Before the first protected-trigger obligation is completed, Nmcore=0N_m^core=0, so the nonempty-core-sample requirement of Definition 2 fails. After the first such completion, the core lower bound remains zero at every event index. Hence the joint aggregate and core-conditional criterion never certifies ψ⋆ψ . ∎ A.4. Proof of Proposition 4 Proof. Fix an enabled g and condition on ℋjH_j, which fixes the candidate, protected-trigger predicate, and budget. All selected obligations share the finite horizon H⋆H ; selected origin indices are increasing, and timestamps are non-decreasing. Completion by event index m of a selected obligation therefore implies completion of every earlier selected obligation in the same group. Consequently the outcomes available at m are exactly Xk1(g),…,XkNm(g)(g)X_k_1^(g),…,X_k_N_m^(g)^(g). By definition of the completed-outcome filtration and conditional mean, [Xks(g)−ps(g)∣j,s−1(g)]=0,Xks(g)−ps(g)∈[−ps(g),1−ps(g)].E\! [X_k_s^(g)-p_s^(g) _j,s-1^(g) ]=0, X_k_s^(g)-p_s^(g)∈[-p_s^(g),1-p_s^(g)]. The predictable interval has width one. Conditional Hoeffding for martingale differences therefore gives, for every fixed q≥1q≥ 1, Pr(p^q(g)−p¯q(g)>log(1/δj,q(g))2q|ℋj)≤δj,q(g). \! ( p_q^(g)- p_q^(g)> (1/ _j,q^(g))2q\; |\;H_j )≤ _j,q^(g). A union bound over q≥1q≥ 1 costs ∑q≥1δj,q(g)=δj(g) _q≥ 1 _j,q^(g)= _j^(g). On the complementary event the inequality holds for every q simultaneously. For an enabled group g, let ℐg:=⋂q≥1p¯q(g)≥p^q(g)−log(1/δj,q(g))2q.I_g:= _q≥ 1 \ p_q^(g)≥ p_q^(g)- \! (1/ _j,q^(g) )2q \. The preceding argument gives Pr(ℐg∣ℋj)≥1−δj(g) (I_g _j)≥ 1- _j^(g). Fix a sample path in ℐgI_g and an event index m>n⋆m>n with Nm(g)>0N_m^(g)>0. Set q=Nm(g)q=N_m^(g) on that sample path. By Equation (5), the outcomes available at m are exactly the first q outcomes of group g. Hence p¯Nm(g)(g)≥p^Nm(g)(g)−log(1/δj,Nm(g)(g))2Nm(g). p_N_m^(g)^(g)≥ p_N_m^(g)^(g)- \! (1/ _j,N_m^(g)^(g) )2N_m^(g). Moreover, p¯Nm(g)(g)≥0 p_N_m^(g)^(g)≥ 0 because it is an average of conditional probabilities. Therefore, p¯Nm(g)(g)≥max0,p^Nm(g)(g)−log(1/δj,Nm(g)(g))2Nm(g)=Lm(g). p_N_m^(g)^(g)≥ \0,\, p_N_m^(g)^(g)- \! (1/ _j,N_m^(g)^(g) )2N_m^(g) \=L_m^(g). Since the sample path and m were arbitrary, the inequality holds simultaneously for every m>n⋆m>n with Nm(g)>0N_m^(g)>0. This pathwise substitution requires no predictability of future origin indices. ∎ A.5. Proof of Proposition 5 Proof. For each enabled g, Proposition 4 bounds its conditional failure probability by δj(g) _j^(g). A union bound over the at most two enabled groups gives δjall+δjcore≤δj _j^all+ _j^core≤ _j. The two groups may overlap; independence is not used. ∎ A.6. Proof of Corollary 6 Proof. Let jC_j denote the simultaneous coverage event of Proposition 5. Conditionally on ℋjH_j, Pr(j∣ℋj)≥1−δj (C_j _j)≥ 1- _j. Fix a sample path in jC_j on which n⋆<mn <m and ψ⋆ψ is statistically certified at m. By Definition 2, for every enabled group g, Nm(g)>0N_m^(g)>0 and Lm(g)≥λgL_m^(g)≥ _g. Because the sample path belongs to jC_j, p¯Nm(g)(g)≥Lm(g)≥λg p_N_m^(g)^(g)≥ L_m^(g)≥ _g for every enabled group g. For every s=1,…,Nm(g)s=1,…,N_m^(g), the event n⋆<m,Nm(g)≥s\n <m,\;N_m^(g)≥ s\ holds on this sample path. The alignment assumption therefore gives ps(g)=pRr(g)(ψ⋆)p_s^(g)=p_R_r^(g)(ψ ) almost surely. Consequently, p¯Nm(g)(g)=1Nm(g)∑s=1Nm(g)ps(g)=pRr(g)(ψ⋆). p_N_m^(g)^(g)= 1N_m^(g) _s=1^N_m^(g)p_s^(g)=p_R_r^(g)(ψ ). Hence, on jC_j, statistical certification at m implies pRr(g)(ψ⋆)≥λgp_R_r^(g)(ψ )≥ _g for every enabled group g. It follows that the event n⋆<m,ψ⋆ is statistically certified at m,∃g∈all,core enabled:pRr(g)(ψ⋆)<λg \ array[]cn <m,\;ψ is statistically certified at m,\\ ∃\,g∈\all,core\ enabled:p_R_r^(g)(ψ )< _g array \ is contained, up to a null set, in jcC_j^c. Therefore, conditionally on ℋjH_j, its probability is at most δj _j. ∎ A.7. Proof of Theorem 7 Proof. Fix j. If the version is never reached or n⋆=∞n =∞, there is no activation and Fj=∅F_j= . On paths with finite selection time, use the simultaneous aggregate and (when enabled) core coverage event. Define it globally by j=n⋆=∞∪n⋆<∞|∀m>n⋆ with Nm>0:p¯Nm≥Lm;and, if core certification is enabled,∀m>n⋆ with Nmcore>0:p¯Nmcorecore≥Lmcore.C_j=\n =∞\∪ \n <∞\; |\; array[]l∀ m>n with N_m>0:\\ p_N_m≥ L_m;\\[2.84526pt] and, if core certification is enabled,\\ ∀ m>n with N_m^core>0:\\ p^core_N_m^core≥ L_m^core array \. The displayed inequalities are required only for their respective nonempty samples. Thus jC_j holds automatically when no candidate is selected, while its core condition is omitted only when core certification is disabled. By Proposition 5, n⋆<∞Pr(jc∣ℋj)≤n⋆<∞δja.s.1_\n <∞\ (C_j^c _j) 1_\n <∞\ _j .s. If activation occurs, its first-crossing definition gives mjcert=nj+1−1m_j^cert=n_j+1-1, nonempty aggregate and, when enabled, core samples, and both lower bounds at least their respective thresholds. Since jC_j holds at every eligible sample size, it holds in particular at this random decision index. Consequently, on jC_j neither FjallF_j^all nor FjcoreF_j^core can occur, so Fj⊆n⋆<∞∩jc.F_j \n <∞\ _j^c. The selection indicator and the budget δj _j are ℋjH_j-measurable. Conditional expectation therefore gives Pr(Fj)≤[n⋆<∞Pr(jc∣ℋj)]≤[n⋆<∞δj]≤[δj]. (F_j) \! [1_\n <∞\ (C_j^c _j) ] \! [1_\n <∞\ _j ] [ _j]. Finally, countable subadditivity, Tonelli’s theorem, and the almost-sure lifetime budget give Pr(⋃j=0∞Fj)≤∑j=0∞Pr(Fj)≤∑j=0∞[δj]=[∑j=0∞δj]≤δ. \! ( _j=0^∞F_j )≤ _j=0^∞ (F_j)≤ _j=0^∞E[ _j]=E\! [ _j=0^∞ _j ]≤δ. No independence between attempts, versions, or the two certification samples is used. ∎