Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications

Ruggero Lanotte

cs.LOSep 27, 2026

Protected Cores Are Not Enough: Certifying AI-Proposed Revisions of Temporal Specifications

Authors: Ruggero Lanotte

Organizations: University of Insubria, Varese, Italy

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.

Figures & tables

Step	Phase	Condition	Governor action
1	Observe	Every event $e_{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 $\psi_{j}$ .
2	Certify	A candidate $\psi^{\star}$ has been selected	Advance the certification-only monitor on candidate origins $k>n^{\star}$ . Add newly completed outcomes to the aggregate sample and, when enabled, to the core sample. Evaluate $L_{n}$ and $L_{n}^{\mathrm{core}}$ .
3	Activate	$\psi^{\star}$ satisfies Definition 2 for the first time at $n$	Set $m_{j}^{\mathrm{cert}}=n$ , $\psi_{j+1}=\psi^{\star}$ , and $n_{j+1}=n+1$ . The new version governs origins from $n+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 $\psi_{j}$ is active	Obtain $\mathcal{P}_{n,j}$ , discard every candidate that fails $\psi_{j}\mathrel{\mathcal{R}}\psi$ , select at most one survivor, fix its error allocation, set $n^{\star}=n$ , and start prospective certification.
5	Continue	Neither activation nor candidate selection occurs	Keep $\psi_{j}$ active. Continue resolving obligations under their origin versions. A drift declaration, proposal, or admissibility check alone does not change the active specification.

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.

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

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.

Tasks	Exact rankings	Ranking errors	Mean margin regret
500	435	65	0.0035

Table 2. Independent ranking audit of the frozen RQ2 proposer.

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.

$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]	–

Table 3. RQ2 masked-core experiment with proposals selected by the frozen supervised proposer. A below-core activation occurs while

p^{\mathrm{core}}<\lambda_{\mathrm{core}}

; brackets give Wilson 95% intervals.

Figure 3. Activation rates against protected success at

w=0.2

(left) and median completed protected obligations at joint activation (right). The dotted line is

\lambda_{\mathrm{core}}

. Two plots show activation rates and median core evidence as the protected success probability increases.

$p^{\mathrm{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

Table 4. RQ2 protected-success sweep at

w=0.20

. A dash means that no run activated within the horizon.

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.

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

Table 5. RQ3 sequential experiment with the frozen supervised AI proposer. ‘Below core’ counts runs with at least one activation during a regime where

p^{\mathrm{core}}<\lambda_{\mathrm{core}}

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

Table 6. Monitored clinical-alarm case study and reference runtime.

Explore similar work

Jun 30, 2026cs.CR

Certified Speculative Execution for Untrusted AI Agents

Hard-constrained sequential decision systems have no certified way to spend the test-time compute of modern AI: executing the multi-step drafts of a learned policy or a frozen LLM forfeits the feasibility guarantee a trusted solver provides, while invoking the solver at every step forfeits the speed the AI offers. Certificate-Gated Prefix Acceptance (CGPA) closes this gap with a certified speculative-execution contract for untrusted AI agents: a trusted verifier rejects constraint-violating transitions exactly, a conformally calibrated value boundary gates the longest low-cost prefix within a per-segment regret budget, and the rest defers to the solver, so safety, regret, and speed decouple by construction. The contract drives every untrusted proposal source - adversarial drafters and six heterogeneous frozen LLMs (including a 12B model that violates constraints in 98% of direct rollouts) - to zero applied violations; a certificate-aware learned boundary, conformally calibrated, drives mean regret three orders of magnitude below unguarded acceptance, to within sampling noise of the stepwise oracle (95% CI spanning zero), and under calendar shift a learned proposal source overtakes it on 15 of 18 held-out days. On a deployment-scale unit-commitment instance it turns a frozen 8B LLM into a 2.96x per-episode wall-clock speedup at 2.1% regret, outpacing the domain heuristic (1.79x) and a safe receding-horizon baseline (1.07x): the more capable the untrusted source, the faster the certified system, at guarantees that never change.

Chenyu Zhou, Qiliang Jiang, Shuning Wu +1

School of Engineering, Institute of Science Tokyo, Japan · College of Control Science and Engineering, Zhejiang University, China · Department of Electrical and Computer Engineering, National University of Singapore, Singapore

Trustworthy Artificial Intelligence Cryptographic Merkle Tree Commitments Artificial Intelligence Agents Self-Speculative Certificates

Ask PDF

Jun 26, 2026cs.LO

Algorithmic Unverifiability of Safety for Fixed and Recursively Self-Improving Systems

We establish mathematical limits of algorithmic safety verification for Turing-complete self-modifying systems, the class in which recursive self-improvement takes place, both for a fixed system and across its own modification. Statically, no verifier is sound, complete and tractable: over unbounded domains by Rice's and Gödel's theorems, over all finite configurations by Trakhtenbrot's theorem, and over succinctly described finite environments because verifying a policy against an adversary is coNP-complete and synthesising one is PSPACE-complete. Dynamically, we model one step of self-modification as a computable transformation of code and ask whether a safety property survives it. If the transformation depends only on behaviour, this is Rice's theorem one level up; if it reads the code, as self-modification does, the question is no longer semantic, yet the same s-m-n reduction works inside a class of behaviourally identical programs and inherits the halting degree. One step is never harder than the property; persistence along the whole trajectory can be

Π^0_2

-complete. Certification by a total algorithm is possible only for transformations of restricted expressivity, not merely for systems that stop changing. No tower of supervisors helps, and every total supervisor errs on an undecidable set of systems. For effectively pointwise properties, every faithful bounded scheme that certifies on finite behavioural evidence admits evolution traces certified at every stage while the property is violated. What survives is exact: a monitor that raises an alarm on violation semidecides it, and comparison against a frozen reference keeps the full theory.

Jose Pascual Gumbau Mezquita

University Jaume I de Castell´o, Spain

Artificial Intelligence Safety Probabilistic Safety Artificial Intelligence Systems Certification Barriers

Ask PDF

Sep 17, 2026cs.CR

Trust, but Validate the Instrument: Auditing AI-Generated RTL Verification Plans on Authored Security-Regression Proxies

AI-generated RTL verification plans can satisfy a provider schema yet fail at the boundary to trusted execution. We present SecTB-RTL, an auditable framework covering 31 tasks and 124 authored hardware-security regressions. A deterministic non-AI baseline killed 36, 75, and 78 mutants at increasing resource limits. The first confirmatory run (C1-R2) failed before model execution because the provider rejected its response schema. After a schema-only repair made without viewing outcomes, a separately frozen follow-up run (C1-R3) completed 1,860 calls. The provider accepted 1,857 responses, but only nine passed the production semantic validator. The generation and execution rules did not match. We therefore preserve the run as an instrument-validation incident and report no prompt-effect estimate. This incident shows that provider or schema acceptance does not establish execution validity. Compilation and coverage are only diagnostics; the exact saved artifact must pass the full production path. A subsequent follow-up is excluded because it did not satisfy the preregistered evidence-completeness gate and is treated only as future work. We release the benchmark, failure-preserving contract, incident provenance, and governance controls needed to prevent infrastructure behavior from being misreported as model behavior.

Hang Xiao, Chuhong Xu, Kainan Zhou +2

Fortinet, Inc. Sunnyvale, CA, USA · Sony Corporate of America San Jose, CA, USA · Google LLC Mountain View, CA, USA

Runtime Enforcement Model Auditing AI Trustworthiness Vulnerable Code Incident Response Register Transfer Level

Ask PDF