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

Ruggero Lanotte

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…