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

arXiv: https://arxiv.org/abs/2609.33461 · HTML: https://mlsanity.com/paper/2609.33461/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 23 references that are in the map.
- First posted on arXiv 27 Sep 2026.

## Builds on (most cited first, 11 of 11)

- [Time-uniform, nonparametric, nonasymptotic confidence sequences](https://mlsanity.com/paper/1810.08240/) (2018)
- [Estimating means of bounded random variables by betting](https://mlsanity.com/paper/2010.09686/) (2020)
- [Tracking the risk of a deployed model and detecting harmful distribution shifts](https://mlsanity.com/paper/2110.06177/) (2021)
- [WATCH: Adaptive Monitoring for AI Deployments via Weighted-Conformal Martingales](https://mlsanity.com/paper/2505.04608/) (2025)
- [Self-Evolving Agents with Anytime-Valid Certificates](https://mlsanity.com/paper/2607.00871/) (2026)
- [Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI](https://mlsanity.com/paper/2406.11563/) (2024)
- [Runtime Verification of Self-Adaptive Systems with Changing Requirements](https://mlsanity.com/paper/2303.16530/) (2023)
- [Robust Probabilistic Shielding for Safe Offline Reinforcement Learning](https://mlsanity.com/paper/2605.10293/) (2026)
- [Robust Shielding for Safe Reinforcement Learning](https://mlsanity.com/paper/2606.00270/) (2026)
- [Multi-Property Temporal Logic Monitoring](https://mlsanity.com/paper/2605.13668/) (2026)
- [SENTIL: A Runtime Verification Tool for Probabilistic Temporal Logic](https://mlsanity.com/paper/2605.21676/) (2026)

## Abstract (arXiv)

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.