1 Introduction↩︎

Many deployed AI systems are used either as assistants that answer questions or as agents that perform actions. Both kinds may proceed through a series of iterations.

Such systems are often discussed in two ways that we find misleading. As magic systems: as if their behaviour could not be decomposed and understood, akin to machine learning as alchemy [1]. As oracles: as if an answer produced by the system were already the fact or world state of interest; other works warn against conflating fluent generated text with factuality [2]–[5].

Thus important questions are difficult to answer with precision: what is accepted knowledge in a given domain? What are the reference sources? What do they say? What can the system use at this point in time? Does this differ from accepted domain knowledge or reference sources? What part of the world can the system observe or change? Is the system allowed to? Can we record, examine and check what led to a consequential step such as an observation of or a change to the world?

We start from the stance that AI systems should be treated as engineered semantic abstractions, not as magic or oracles: an AI system’s output is not the object it appears to describe, but rather, like Magritte’s pipe, a representation of it. At a high level, we consider a system to consist of:

• Knowledge Bases: possibly erroneous material available to the system, e.g. prose or code;

• Prompts: the user’s queries, refinements, and steering during an interaction;

• Compute Components: e.g., one model or a cohort of models that transform prompts and reference sources into messages, artefacts, or actions, as well as Agent Services such as cameras;

• Actuations: the responses, artefacts, actions, or world modifications produced by the system;

• an Orchestrator: a possibly empty orchestration layer around the Compute Components that may call tools, retrieve files, or iterate before actuation.

A system does not manipulate the semantic objects of interest directly: retrieving sources, calling tools, proposing updates, is done through interfaces. This interface layer embodies the core distinction of this work: an AI answer, prompt or tool call is but a message whose meaning, source, authority, and effect have to be interpreted and checked w.r.t. an underlying semantics.

1.0.0.1 Outline

Sections 2 and 3 define knowledge bases, the communication language used by the system, the world, traces, contexts and prompts. Section 4 defines the Information State of an AI system. Section 5 explains how messages become candidate claims, when those are supported and may be relied on. Section 6 examines Information State mismatches, which we hope gives a taxonomy of what is often called hallucination. Section 7 defines compute components such as neural and symbolic components, services, and orchestrators. Section 8 assembles these layers into the definition of an AI system and gives quality judgments.

Thus we propose that AI systems are abstractions of ideal semantic systems. An ideal semantic system relies on an underlying semantics and its actuations are grounded over that semantics. An AI system operates through partial, lossy, and sometimes speculative abstractions of that semantics.

Of course in certain domains, the underlying semantics may be unclear, e.g. when dealing with prose. But our framework may still help locate a system’s obligations and failure modes.

2 Knowledge Base↩︎

This section defines the machinery used for knowledge bases. A knowledge base \(K=\langle D,F,R,t\rangle\) at time \(t\in\mathbb{N}\) features a domain \(D\) (a collection of objects, e.g. sets, types…), facts \(F\in\wp(D)\), and a rule system \(R\) over domain \(D\). A rule \(\frac{P}{c}\) has premises \(P\in\wp(D)\) and a conclusion \(c\in D\). If \(P=\emptyset\) the rule is called an axiom. The rule system \(R\triangleq\Bigl\{\frac{P_i}{c_i}\Bigm| i\in\rho\Bigr\}\) over \(D\) is a possibly infinite family of rules indexed by a set \(\rho\).

Standard [6], intuitionistic [7], and modal [8] logics can be formalised using such Hilbert-style proof systems [9]. Although introduced for logics [9], such rule-based definitions can define any subset of a domain \(D\), hence encompass grammars [10], databases [11], knowledge graphs [12], and deductive systems [13], and may also contain contradictory facts.

Next we need to say what consequences may be justified by \(R\) from the facts in \(F\):

• Proofs. A theorem has hypotheses \(H\in\wp(D)\), a conclusion \(c\in D\), and a proof. If every premise set \(P_i\) of every rule \(\frac{P_i}{c_i}\) in \(R\) is finite, the proof is a sequence \(p_1 p_2\ldots p_n\) s.t. each \(p_i\) is a hypothesis in \(H\), a fact in \(F\), or the conclusion of a rule s.t. all elements of \(P_i\) previously appeared in the sequence, and the last element in the sequence is the conclusion of the theorem. If some premises are infinite, the proof may rely on the principle of transfinite induction [14].

  For Oma: A proof step may be s.t. if freshness and official sources have been checked, then the draft may be marked ready.

• Inference. If \(X\) is the set of facts already reached, then \(\textsf{Infer}_{\!R}(F)(X)\triangleq F\cup X\cup\{c_i\mid i\in\rho\wedge P_i\subseteq F\cup X\}\) adds facts \(F\) to \(X\), and every conclusion whose premises are available from \(F\cup X\).

  For Oma: A proof step may add “the draft may be marked ready” only after the required source, picture-check, CheckForm, and ConfirmDraft facts are already reached.

• Chaining. Forward chaining repeatedly applies \(\textsf{Infer}_{R}(F)\) to justify consequences from the facts already available. Backward chaining replaces a set of goals \(G\subseteq D\) by the premises \(P\) of a rule \(R\) that would prove it: \(G \leadsto_{R} (G\setminus\{c\})\cup P when \frac{P}{c}\in R and c\in G\).

  For Oma: Forward chaining starts from observations and sources and justifies claims such as “picture respects rules” or “form ready”. Backward chaining starts from “may mark ready?” and reduces it to source freshness, picture compliance, form completion, CheckForm, and Oma’s confirmation.

• Closure. For a set \(B\subseteq D\), let \(\textsf{Infer}^{\ast}_{R}(B)\triangleq \textsf{lfp}^{\subseteq}\bigl(\lambda X.\textsf{Infer}_{R}(B)(X)\bigr)\), where \(\textsf{lfp}^{\subseteq}\) is the least fixed point in order \(\subseteq\), which exists by Tarski’s theorem [15] since \(X\mapsto \textsf{Infer}_{R}(B)(X)\) is \(\subseteq\)-monotone in \(X\). A conclusion \(c\) is justified from facts \(F\) and hypotheses \(H\) when \(c\in\textsf{Infer}^{\ast}_{R}(F\cup H)\).

• Paraconsistent justification. Given \(K=\langle D,F,R,t\rangle\), we say that \(K\) justifies a claim \(c\) when \(K\vdash c \triangleq c\in\textsf{Infer}^{\ast}_{R}(F)\), and that \(K\) does not justify \(c\) when \(K\not\vdash c \triangleq c\notin\textsf{Infer}^{\ast}_{R}(F)\). A knowledge base may justify a fact, its negation, both, or neither. Thus \(K\vdash c\) may not mean that \(c\) is reliable. Absence of justification is not negation: \(K\not\vdash c\) does not imply \(K\vdash\neg c\). We distinguish four base statuses: \(K\vdash^{+}c \triangleq K\vdash c\wedge K\not\vdash\neg c\), \(K\vdash^{-}c \triangleq K\vdash\neg c\wedge K\not\vdash c\), \(K\vdash^{\pm}c \triangleq K\vdash c\wedge K\vdash\neg c\), \(K\vdash^{?}c\triangleq K\not\vdash c\wedge K\not\vdash\neg c\). We also use the derived shorthand \(K\vdash^{\oplus}c \triangleq K\vdash^{+}c \oplus K\vdash^{-}c\) for one-sided justification. When the time index is useful, we write \(K\vdash^{\times}_t c\) for the corresponding base status at time \(t\), with \(\times\in\{+,-,\pm,?\}\), and use \(K\vdash^{\oplus}_t c\) as the derived one-sided shorthand.

3 Communication Language, World, Traces, Context, Prompts↩︎

This section introduces messages, world states, event traces, contexts, and prompts.

3.1 Communication Language↩︎

To communicate, the components of an AI system share a common language \(\textit{Lang}\). This language may include labels, token sequences, communication codes, matrices, computer programs, data tables, URLs, tool-call schemas, etc, for the usage of the AI system.

Below, the objects written \(m_{*}\) are communication-language messages: elements of \(\textit{Lang}\). They are not world objects and not semantic facts.

3.2 Semantics of the Communication Language↩︎

Now we need to determine the meaning of messages. We write \(\mathsf{denotation}_{\textit{Lang}} : \textit{Lang}\rightharpoonup \mathsf{SourceItems}\) for the denotation of messages, where \(\mathsf{SourceItems}\) is the set of source items, which we discuss more amply in Section 4.2. Because denotation may not be defined, we write: \[\mathsf{Denotes}_{\textit{Lang}}(m,s) \triangleq m\in\textit{Lang} \wedge s\in\mathsf{SourceItems} \wedge \mathsf{denotation}_{\textit{Lang}}(m)=s \text{ is defined}.\]

Thus denotation alone does not make a source item usable.

3.3 Model of the World↩︎

Our model of the world is a formal representation of the external state that an AI system can observe, affect, or be affected by. It includes at least:

• the set of possible world states \(W\); at time \(t\), the current world state is \(w_t\);

• the history \(w_1, \ldots, w_t\) of world states at time \(t\);

• what the AI system can observe, via \(\mathsf{observation}\);

• what the AI system can change, via \(\mathsf{actuation}\);

• which world changes are due to the AI system, users, tools, or external events;

• specifications saying which reads and writes are allowed or correct.

The system may observe only part of the world. We write \(\mathsf{observation}\in \textit{Services}\times W\rightarrow \textit{Lang}\) for the service-relative observation interface, possibly lossy, permission-limited, and time-dependent.

The AI system may also modify part of the world. We write \(\mathsf{actuation}\in (W\times \textit{Lang})\rightarrow W\) for the actuation interface. Thus \(\mathsf{actuation}(w,m)\) should be effectless when the message \(m\in\textit{Lang}\) is not an allowed update from world state \(w\).

3.4 Traces↩︎

The world state may change outside the system’s control. A user, a tool, an external service, may move \(w_t\) to \(w_{t+1}\). The relation between the two states may be unknown to the system.

Thus we keep separate records: the history \(w_1\ldots w_t\), an event trace recording what happened, and the context, i.e. material selected from that trace for a particular component call. An event is a record \(e=\langle \mathsf{name},\mathsf{comment},\mathsf{actor},\mathsf{message},\mathsf{kind},\mathsf{resource}, \mathsf{observation},\mathsf{actuation},\mathsf{authority},\mathsf{witness} \rangle \in \textit{Ev}.\) We write e.g. \(e.\mathsf{message}\) for the \(\mathsf{message}\) field of the event \(e\).

The actor may be e.g. the user, a compute component, the environment… The kind records whether the event is a read, write, check, authority event, internal computation, or external mutation. The resource says what was read, written, or checked. The observation and actuation fields hold messages in a language discussed in Section 3.1. The authority field records permission, consent, revocation, or delegation. The witness field records source pointers, tool results, proof objects, checker results, timestamps, or trace slices.

A trace is a finite event sequence \(\textit{trace}=e_1\ldots e_n\in\mathsf{Trace}\triangleq \textit{Ev}^\ast\). For \(0\le k\le n\), let \(\textit{trace}_{\le k}\triangleq e_1\ldots e_k\), with \(\textit{trace}_{\le 0}=\epsilon\), be the prefix of the trace available after \(k\) events. Often, we identify the time \(t\) with the current number of events recorded in the trace.

The world state history, event trace, and context are related but not identical. A read may add an event without changing the physical world. A write may both add an event and move the world from \(w_t\) to \(w_{t+1}\). An external mutation may change the world before the AI system has observed it. The context may omit trace events, summarise them, or include computed communication messages, but it is not the authority record used by event specifications.

3.5 Context↩︎

Calls to AI systems are often talked about in terms of their context. We let \(\textit{ctx}\in\textit{Lang}^{\ast}\) range over messages available to the system at some point in the trace. More specifically, ctx is an application-specific abstraction of trace: \(\textit{ctx}_t \in \mathsf{Select}_t(\textit{trace})\): when selecting context, the system may compress, forget, compact, rearrange the context as required by the application. The selection may use the orchestrator policy, component being called, memory state, and context-window budget.

3.6 Prompts↩︎

Users communicate with a system via prompts: a system prompt is a standing constraint recorded in the trace and reflected in the contexts selected from it. A user prompt is what the system is being asked to do right now, also recorded in the trace.

Some prompts gather information, e.g. reading files or making web searches. Other prompts require actions from the system, e.g. answering questions, creating or editing files, calling tools.

4 Information State of an AI system↩︎

We aim to distinguish the underlying semantics from the reference sources, and to distinguish these two objects from what the AI system is using. Thus we introduce three different knowledge bases which, together with the reference sources \(\textit{Src}_t\) constitute the Information State of an AI system:

• Section 4.1 defines the universal knowledge base \(K_{U,t}\): accepted domain knowledge.

• The reference sources \(\textit{Src}_t\) consist of source pointers or resources: pages, files, tool results….

• Section 4.2 defines the source-derived knowledge base \(K_{S,\textit{Src},t}\), computed from facts extracted from \(\textit{Src}_t\): it may be wrong, incomplete, stale, or inconsistent.

• Section 4.3 defines the AI system’s effective knowledge base \(K_{E,\textit{ctx},t}\): what the system can use from the current context ctx, including mistaken, stale, compressed material. \(K_{E,\textit{ctx},t}\) is not what is in context; rather the context is an input to \(K_{E,\textit{ctx},t}\).

Throughout the paper, when we use conceptual objects that exist in the mathematics but may not appear directly in an AI system implementation, we highlight them with an overline, e.g. \(\bar{U}\).

4.1 Universal Knowledge Base↩︎

The domain of the universal knowledge base \(K_{U,t}\) is a universe \(\bar{U}\) such that:

• The elements of the universe \(\bar{U}\) encode facts, objects, and reasoning steps: token sequences, pictures, videos, recordings, theorems, proofs, laws, programs, events, permissions…One can read \(\bar{U}\) as many-sorted, or as a single encoded universe with tags for the different sorts of objects;

• Without loss of generality, \(\bar{U}\) need not evolve in time: it can be a sufficiently large set of representations, and contain the objects we need: functions, relations, sets, sequences, traces…

The Universal Knowledge Base w.r.t. a universe \(\bar{U}\) and a rule system \(\bar{R}_t\) over \(\bar{U}\) at a time \(t\) consists of selected hypotheses \(\bar{H}_t\subseteq\bar{U}\) together with the rule system \(\bar{R}_t\): \(K_{U,t}\triangleq\langle \bar{U}, \bar{H}_t,\bar{R}_t,t\rangle\).

4.2 Source-derived Knowledge Base↩︎

We assume that an AI system cannot always range over everything in \(\bar{U}\). Instead, a system has a scope \(\overline{\textit{Scope}}\subseteq\bar{U}\), and within that scope it may lose distinctions that are present in the universal knowledge base. We model these two limits by an ignorance abstraction and a forgetfulness abstraction, which yield Galois connections in abstract interpretation [16].

4.2.1 Ignorance and Forgetfulness Abstractions↩︎

4.2.1.1 Ignorance.

The \(\overline{\textit{ignore}}\) abstraction ignores what falls outside this scope: \(\overline{\textit{ignore}}(X)=X\cap \overline{\textit{Scope}}\) for \(X\in\wp(\bar{U})\). The same restriction applies to rules: \(\overline{\textit{ignore}}(\bar{R}_t) \triangleq \Bigl\{ \frac{P}{c}\in \bar{R}_t \Bigm| P\subseteq \overline{\textit{Scope}}\wedge c\in \overline{\textit{Scope}}\, \Bigr\}\). Thus \(\overline{\textit{ignore}}(\bar{R}_t)\) is sound but incomplete relative to \(\bar{R}_t\): any proof in \(\overline{\textit{Scope}}\) is also a proof in \(\bar{U}\), but some proofs in \(\bar{U}\) disappear because some facts, premises, or rules are outside the system’s scope.

4.2.1.2 Forgetfulness.

The \(\overline{\textit{forget}}\) abstraction formalises loss of distinctions inside the system’s scope. We write \(\equiv_f\) for the application-specific equivalence relation on \(\overline{\textit{Scope}}\) that identifies semantic objects the AI system’s representation cannot distinguish, and \([x]_{\equiv_f}\) for the equivalence class represented by \(x\). On sets, \(\overline{\textit{forget}}(X)=\{[x]_{\equiv_f}\mid x\in X\}\). On rules, \(\overline{\textit{forget}}(R) \triangleq \biggl\{ \frac{\{\,[p]_{\equiv_f}\;|\; p\in P\,\}}{\ustrut[c]_{\equiv_f}} \biggm| \frac{P}{c}\in R \biggr\}\,\), so abstract rules can no longer distinguish equivalent pieces of information.

4.2.2 Source-derived Knowledge Base and its semantics↩︎

The reference sources \(\textit{Src}_t\) are not themselves facts: source-item facts \(F_{S,\textit{Src},t}\subseteq\mathsf{SourceItems}\) (with \(\mathsf{SourceItems}\triangleq \overline{\textit{Scope}}/{\equiv_f}\)) are extracted from \(\textit{Src}_t\). The corresponding rule system is \(R_{S,t}\triangleq \overline{\textit{forget}}\,(\overline{\textit{ignore}}\,(\bar{R}_t))\). Thus the source-derived knowledge base is \(K_{S,\textit{Src},t}\triangleq \langle \mathsf{SourceItems}, F_{S,\textit{Src},t}, R_{S,t}, t \rangle\). Its inference operator is \(\textsf{Infer}_{R_{S,t}}\), and \(\mathsf{denotation}_{U} \in\mathsf{SourceItems}\rightarrow\wp(\bar{U})\) defines the semantics of the source-derived knowledge base \(K_{S,\textit{Src},t}\) w.r.t. the universal knowledge base \(K_{U,t}\).

4.3 Effective knowledge base↩︎

This section defines the Effective knowledge base of an AI system, i.e. the material the system works with. It may be distinct from the Universal and Source-derived Knowledge Bases, and instead be built from what is often called the context \(\textit{ctx} \in \mathsf{Select}_t(\textit{trace})\), gathered e.g.from interactions with the world recorded in trace.

4.3.1 Effective knowledge base and its Semantics↩︎

We let \(K_{E,\textit{ctx},t}\) be the effective knowledge of an AI system: \(K_{E,\textit{ctx},t}\triangleq \langle \textit{Lang},F_{E,\textit{ctx},t},R_{E,\textit{ctx},t},t\rangle\).

Recall that the context ctx is gathered by the orchestrator by interaction with users or external agents. The facts \(F_{E,\textit{ctx},t}\triangleq\{m\mid m\in\textit{ctx\/}\}\) are directly extracted from this context ctx.

4.3.2 Context is not Effective Knowledge↩︎

Recall that context \(\textit{ctx}\) is an application-specific abstraction of the trace (which may include loss or extrapolation). Thus \(\textit{ctx}\) lives in \(\textit{Lang}\): it is not itself a knowledge base, nor is it a subset of the effective knowledge \(K_{E,\textit{ctx},t}\).

Indeed context can contain something the system fails to use. A retrieved document may state the correct rule, but the model may overlook it: the rule is in context, but not justified by \(K_{E,\textit{ctx},t}\).

A context window is a bounded fragment of the context, sent as a response to a call: the bound is imposed by the model and its deployment: tokens, bytes, image slots, file attachments, retrieved chunks, tool-result size, latency, cost, or policy.

4.3.3 Context is not Trace↩︎

At a high-level, trace is the event history: observations, actions, tool calls, UI events, confirmations, invalidations, timestamps, provenance, and ctx is an application-specific abstraction (including potential loss and extrapolation) available to the AI system for building \(K_{E,\textit{ctx},t}\). Thus \(K_{E,\textit{ctx},t}\) depends solely on ctx, not the whole trace.

By contrast, event validity and source witness provenance often need trace, because ctx may omit or summarise the events that matter.

Without the distinction, we may accidentally assume either ctx = trace so the system has perfect access to the whole event history, or trace = ctx which means we will not really be able to audit the system, because we will only have access to the context.

4.4 Knowledge Base Statuses↩︎

Justification of a claim by a knowledge base is only potential by default. Writing \(+\), \(-\), \(\pm\), and \(?\) for the base justification statuses of Section [sec:paracons], and \(\oplus\) for the derived one-sided shorthand, we record what is justified by the Effective knowledge base \(K_{E,\textit{ctx},t}\), the Source-derived knowledge base \(K_{S,\textit{Src},t}\), and the Universal knowledge base \(K_{U,t}\). To keep the selected knowledge base explicit, each status predicate takes it as a parameter \((\times \in \{+, -, \pm, ?\})\): \[\begin{align} \mathsf{Effective}_{\times,t}(m,s;K_{E,\textit{ctx},t}) &\triangleq \mathsf{Denotes}_{\textit{Lang}}(m,s) \wedge K_{E,\textit{ctx},t}\vdash^{\times}_t m \\ \mathsf{Source}_{\times,t}(s;K_{S,\textit{Src},t}) &\triangleq s\in\mathsf{SourceItems} \wedge K_{S,\textit{Src},t}\vdash^{\times}_t s \\ \mathsf{Universal}_{\times,t}(c;K_{U,t}) &\triangleq c\in\bar{U} \wedge K_{U,t}\vdash^{\times}_t c \end{align}\]

4.5 Relationships between Knowledge Bases↩︎

An AI system may not normally possess the universal knowledge base directly. Rather it builds an Effective knowledge base from reference sources, observations, tool results, memory, local system state, and traces. An AI actuation, whether an answer to a question or an action performed, comes from that effective knowledge base. It may or may not match the reference sources, and it may or may not match the universal knowledge base. Contrary to mathematics, reference sources need not be consistent: both a conclusion and its contrary may be reached from defective sources.

The universal knowledge base \(K_{U,t}\) is assumed given: in general \(K_{U,t}\) will be application-dependent and thus the only general comment about it is that it needs rules describing known facts (axioms) and reasoning steps (induction rules). But in many domains, natural-language semantics is unclear, disputed, or changing, so \(K_{U,t}\) is not fully available as a clean mathematical object. In other domains, such as mathematics, certain formally specified programming languages, controlled forms, or controlled English, \(K_{U,t}\) may be precise enough to state obligations, but checking those obligations may still be undecidable, expensive, approximate, or domain-specific.

Source evidence has a different status. A source pointer \(\mathit{sp}\in \textit{Src}_t\), recorded in a trace witness field, can witness that the system retrieved or cited a source. It does not by itself show that the source was current, official, complete, or authoritative, nor does it show that the system correctly interpreted the source: that is an obligation on the construction of \(K_{S,\textit{Src},t}\) from \(\textit{Src}_t\).

Finally, even if a source item is present in the system’s effective knowledge \(K_{E,\textit{ctx},t}\), that only says that the system can currently use that item. It does not by itself show that any semantic claim asserted through the item is justified by \(K_{S,\textit{Src},t}\), true in \(K_{U,t}\), or authorised by the user.

These limitations are not a reason to abandon the formalisation. They mark where the obligations sit. If \(K_{U,t}\) is unclear, an application written over \(K_{U,t}\) should explicitly disclaim that. If source material is stale or unofficial, the issue is in \(\textit{Src}_t\). If extraction or interpretation is wrong, the issue is in \(K_{S,\textit{Src},t}\). If the system relies on a compressed, inferred, or approximate item, the issue is in \(K_{E,\textit{ctx},t}\). If a witness only supports the fact that a source said something, and not the semantic claim itself, that distinction should remain visible in the trace through source pointers and witness fields.

5 From Candidate Claims to Reliable Claims↩︎

We aim to determine when a claim made or used by the system may be reliable. The following diagram illustrates relationships between the concepts we introduce:

5.1 Candidate Claims↩︎

The Effective knowledge base \(K_{E,\textit{ctx},t}\) over Lang records what the system is justified to use at time \(t\) for the context ctx. For a message \(m\in\textit{Lang}\), its being justified by the Effective knowledge base does not mean it is true.

For a message \(m\) justified by \(K_{E,\textit{ctx},t}\), the map \(\mathsf{CandidateClaims}\in \textit{Lang}\rightarrow\wp(\bar{U})\) records which claims \(m\) might be standing for. We let \(s_m\) be the unique source item \(s\) s.t. \(\mathsf{Denotes}_{\textit{Lang}}(m,s)\). Then: \[\mathsf{CandidateClaims}(m)\triangleq \begin{cases} \mathsf{denotation}_{U}(s_m), & \text{if } s_m \text{ is defined},\\ \emptyset, & \text{otherwise.} \end{cases}\] When \(s_m\) is defined, the claims in \(\mathsf{CandidateClaims}(m)\) are the semantic claims associated with the source item \(s_m\). This may be a set with several elements because of the forgetfulness abstraction. If \(s_m\) is undefined, \(m\) has no candidate claims.

An empty candidate-claim set does not by itself make an event valid: event validity separately requires the event message to have defined denotation when the event is checked.

The definition of \(\mathsf{CandidateClaims}\), like that of the underlying semantics, is application-dependent. It is the role of e.g. application developers and semanticists to define suitable semantics and corresponding maps, given a domain and application. For an item \(m\), \(\mathsf{CandidateClaims}(m)\) needs to say which underlying claims \(m\) is allowed to stand for. There may be a priori more than one, and the application developers and semanticists need to determine which claims must be distinguished.

5.2 Asserted Claims↩︎

The map \(\mathsf{CandidateClaims}\) records what a message could mean. To say which of those candidate claims the system is actually asserting through the message, we use an application-specific predicate \(\mathsf{Asserts}_{E,\textit{ctx},t}(m,c)\), s.t. \(\mathsf{Asserts}_{E,\textit{ctx},t}(m,c) \Rightarrow m\in\textit{Lang}\wedge c\in\mathsf{CandidateClaims}(m)\).

The asserted claims of \(m\) are then: \[\mathsf{AssertedClaims}_{E,\textit{ctx},t}(m)\triangleq \{\,c\in\mathsf{CandidateClaims}(m)\mid K_{E,\textit{ctx},t}\vdash^{+}_t m \wedge \mathsf{Asserts}_{E,\textit{ctx},t}(m,c)\,\}.\] Thus \(\mathsf{CandidateClaims}(m)\) records possible meanings, while \(\mathsf{AssertedClaims}_{E,\textit{ctx},t}(m)\) records the candidate claims that the system actually asks the user, caller, or downstream component to rely on. The positive effective-knowledge condition \(K_{E,\textit{ctx},t}\vdash^{+}_t m\) excludes messages that are refuted, contradictory, or unjustified in \(K_{E,\textit{ctx},t}\). This does not entail that any asserted claim is justified by the source-derived knowledge base, let alone by the universal knowledge base.

5.3 Supported Claims↩︎

Source support records which semantic claim a source-derived item supports. We write \(\mathsf{SourceSupport}_t\) \(\subseteq \mathsf{SourceItems}\times \bar{U}\) and read \(\mathsf{SourceSupport}_t(s,c)\) as: at time \(t\), source item \(s\) supports the semantic claim \(c\). Source support is application-defined, but it must respect denotation: \(\mathsf{SourceSupport}_t(s,c) \Rightarrow s\in\mathsf{SourceItems}\wedge c\in\mathsf{denotation}_{U}(s)\).

For a message \(m\) justified by \(K_{E,\textit{ctx},t}\), i.e.\(K_{E,\textit{ctx},t}\vdash^{+}_t m\), the corresponding candidate claims are \(\mathsf{CandidateClaims}(m)\). This does not mean that those claims are justified by the source-derived knowledge base \(K_{S,\textit{Src},t}\), let alone the universal knowledge base \(K_{U,t}\). The predicate \[\begin{align} &\mathsf{SupportedClaim}_t (m,c;K_{U,t},K_{S,\textit{Src},t})\triangleq m\in\textit{Lang} \wedge c\in\mathsf{CandidateClaims}(m) \\ &\qquad{}\wedge \exists s\in\mathsf{SourceItems}\mathrel{.} \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\qquad{}\wedge \mathsf{Universal}_{+,t}(c;K_{U,t}) \wedge \mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t}) \wedge \mathsf{SourceSupport}_t(s,c). \end{align}\] says that \(c\) is definitely justified by the Universal Knowledge base, and that it is supported by a source item \(s\) definitely justified by the Source-derived Knowledge base.

5.4 Reliable Claims↩︎

\(\mathsf{SupportedClaim}\) checks whether the candidate claim \(c\) is justified by the universal and source-derived knowledge bases. Reliability also requires that the message \(m\) through which the system uses \(c\) is justified by current effective knowledge and that \(c\) is one of the asserted claims of \(m\). With \(\mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c)\triangleq m\in\textit{Lang}\wedge c\in\mathsf{AssertedClaims}_{E,\textit{ctx},t}(m)\), the full reliability predicate is \[\begin{align} &\mathsf{ReliableClaim}_t(m,c; K_{E,\textit{ctx},t},K_{S,\textit{Src},t},K_{U,t},\textit{ctx}) \triangleq\\ &\qquad \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c)\wedge K_{E,\textit{ctx},t}\vdash^{+}_t m \wedge\mathsf{SupportedClaim}_t(m,c;K_{U,t},K_{S,\textit{Src},t}) . \end{align}\] Thus \(K_{E,\textit{ctx},t}\) appears in the judgment for what the system may use, while the support check is grounded in the source-derived and universal knowledge bases.

6 What could possibly go wrong↩︎

A number of things could go wrong, and we distinguish at least two cases: reliance failures occur when the various layers of knowledge disagree, leading to an unreliable claim; history failures occur when the trace disagrees with certain claims, for example when a source becomes stale.

6.1 Reliance failure diagnostics↩︎

A reliance failure is a claim which may not be relied on: \[\mathsf{RelianceFailure}_{t,\textit{ctx}}(m,c)\triangleq\mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge\neg\,\mathsf{ReliableClaim}_t(m,c; K_{E,\textit{ctx},t},K_{S,\textit{Src},t},K_{U,t},\textit{ctx}).\]

This section gives reasons leading to reliance failures: the semantic machinery established in the previous section allows us to diagnose mismatches for asserted claims.

Given a message \(m\in\textit{Lang}\) whose denotation is defined, let \(s=\mathsf{denotation}_{\textit{Lang}}(m)\in\mathsf{SourceItems}\). The claims to classify are \(\mathsf{AssertedClaims}_{E,\textit{ctx},t}(m)\), not every candidate claim that the denoted source item could have stood for. Each diagnostic is a sufficient reason for a reliance failure:

• Refuted Assertion. If \(\mathsf{Universal}_{-,t}(c;K_{U,t})\) also holds, \(K_{U,t}\) refutes the claim: \[\mathsf{RefutedAssertion}_t(m,c;\textit{ctx}) \triangleq{} \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge\mathsf{Universal}_{-,t}(c;K_{U,t}).\]

• Unsupported Assertion. If \(\mathsf{Universal}_{?,t}(c;K_{U,t})\) holds, the use is an unsupported assertion: \[\begin{align} &\qquad{}\mathsf{UnsupportedAssertion}_t(m,c;\textit{ctx}) \triangleq\mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \exists s\in\mathsf{SourceItems}\mathrel{.}\, \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\qquad{}\qquad{}\wedge \mathsf{Effective}_{\oplus,t}(m,s;K_{E,\textit{ctx},t}) \wedge\mathsf{Universal}_{?,t}(c;K_{U,t}) \wedge \neg\,\mathsf{SupportedClaim}_t(m,c;K_{U,t},K_{S,\textit{Src},t}) . \end{align}\]

  The unsupported claim may originate with \(\mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t})\), or it may be invented by the AI system when \(\mathsf{Source}_{\pm,t}(s;K_{S,\textit{Src},t})\) or \(\mathsf{Source}_{?,t}(s;K_{S,\textit{Src},t})\) holds. This corresponds to what is often referred to as hallucinations, e.g. invented citations; fabricated details…

• Extrapolation. This is the assertion of a claim \(c\) through a message \(m\) when the corresponding source item \(s\) is not one-sided and the universal status of \(c\) is contradictory: \[\begin{align} &\mathsf{Extrapolation}_t(m,c;\textit{ctx})\triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \exists s\in\mathsf{SourceItems}\mathrel{.}\, \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\qquad{}\wedge \mathsf{Effective}_{\oplus,t}(m,s;K_{E,\textit{ctx},t})\wedge \neg\,\mathsf{Source}_{\oplus,t}(s;K_{S,\textit{Src},t}) \wedge\mathsf{Universal}_{\pm,t}(c;K_{U,t}). \end{align}\]

• Source-Derived vs Universal Mismatch. If a message \(m\) denotes a source item \(s\) justified by \(K_{S,\textit{Src},t}\), and an asserted claim \(c\in\mathsf{denotation}_{U}(s)\) is contradictory in \(K_{U,t}\), there is a mismatch: \[\begin{align} &\mathsf{SourceUniversalMismatch}_t(m,s,c;\textit{ctx}) \triangleq\mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\qquad{}\wedge c\in\mathsf{denotation}_{U}(s) \wedge\mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t}) \wedge\mathsf{Universal}_{\pm,t}(c;K_{U,t}). \end{align}\]

• Spurious Support. \[\begin{align} &\mathsf{SpuriousSupport}_{t} (m,s,c;\textit{ctx}) \triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s)\wedge \mathsf{Universal}_{+,t}(c;K_{U,t})\\ &\qquad{} \wedge \neg\mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t}) \end{align}\] The claim is true, but the specific source item cited for it is refuted, contradictory, or unknown. Therefore a debunked or unverifiable source is cited for something that happens to be correct.

• Source Support Gap.

  \[\begin{align} &\mathsf{SourceSupportGap}_{t}(m,s,c;\textit{ctx}) \triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s)\\ &\qquad{}\wedge \mathsf{Universal}_{+,t}(c;K_{U,t}) \wedge \mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t}) \wedge \neg \mathsf{SourceSupport}_t(s,c) \end{align}\] The claim is true and the cited source item is itself well-justified but it just doesn’t actually support this particular claim.

• Refuted Source, Contradictory Claim Although the universal semantics finds \(c\) contradictory, the source item \(s\) is definitely refuted: \[\begin{align} &\mathsf{RefutedSourceContradictoryClaim}_t(m,s,c;\textit{ctx}) \triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s)\\ &\quad{}\wedge \mathsf{Universal}_{\pm,t}(c;K_{U,t}) \wedge \mathsf{Source}_{-,t}(s;K_{S,\textit{Src},t}) \end{align}\]

The exhaustiveness result below classifies reliance failures only for asserted claims whose message has defined denotation; events with undefined denotation are rejected by event validity rather than by this reliance taxonomy. We give all proof sketches in appendix.

6.2 History failure diagnostics↩︎

• Stale Source. This is a temporal instance of \(\mathsf{SourceUniversalMismatch}\), for which we need a notion of a source witness: an event present at time \(t_0\) that records a source pointer \(\mathit{sp}\) as provenance for an item \(s\). We assume the existence of an application-specific predicate \(\mathsf{ExtractedFrom}\), which records that event \(e\) is the trace event whose extraction procedure produced source item \(s\) from source pointer \(\mathit{sp}\). We require this predicate to be well-typed: \[\begin{align} \mathsf{ExtractedFrom}_{t_0}(s,\mathit{sp};e_s)\Rightarrow{}& e_s\in \textit{Ev} \wedge s\in\mathsf{SourceItems} \wedge \mathit{sp}\in\textit{Src}_{t_0} \\ &{}\wedge \mathit{sp}\in e_s.\mathsf{witness} \wedge \mathsf{Denotes}_{\textit{Lang}}(e_s.\mathsf{message},s) . \end{align}\]

  Then we record provenance for an extracted source item: \(\mathsf{SourceWitness}_{t_0}(\mathit{sp},s;\textit{trace})\triangleq \exists e_s\in\textit{trace}_{\le t_0}\mathrel{.} \mathit{sp}\in\textit{Src}_{t_0} \wedge \mathsf{ExtractedFrom}_{t_0}(s,\mathit{sp};e_s) \wedge s\in F_{S,\textit{Src},t_0}\).

  A stale source error arises when a source witness comes from an older pointer at time \(t_0\), and \(\mathsf{Universal}_{+,t_0}(c;K_{U,t_0})\) is replaced at time \(t\):

  \(\begin{aligned} &\mathsf{StaleSource}_t(m,\mathit{sp},s,c;\textit{ctx},\textit{trace}) \triangleq\mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge\mathsf{Denotes}_{\textit{Lang}}(m,s)\\ &\qquad{}\wedge c\in\mathsf{denotation}_{U}(s) \wedge \exists t_0<t\mathrel{.}\, \bigl(\mathsf{SourceWitness}_{t_0}(\mathit{sp},s;\textit{trace}) \wedge\mathsf{Universal}_{+,t_0}(c;K_{U,t_0})\bigr)\\ &\qquad{}\wedge\mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t})\\ &\qquad{}\wedge \bigl(\mathsf{Universal}_{-,t}(c;K_{U,t}) \vee\mathsf{Universal}_{?,t}(c;K_{U,t}) \vee\mathsf{Universal}_{\pm,t}(c;K_{U,t})\bigr). \end{aligned}\)

• Refuted Source. Such a source satisfies \(\mathsf{Universal}_{-,t}(c;K_{U,t})\) while \(\mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t})\) holds: \[\begin{align} &\mathsf{RefutedSource}_t(m,s,c;\textit{ctx}) \triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\qquad{}\wedge \mathsf{Source}_{+,t}(s;K_{S,\textit{Src},t}) \wedge \mathsf{Universal}_{-,t}(c;K_{U,t}). \end{align}\] This is stronger than lack of justification for claim \(c\): the universal knowledge base justifies \(\neg c\). It is an AI system error when the system uses this claim, or when source knowledge is itself being presented as authority for \(c\); otherwise it is a source or source-processing issue that the AI system must not silently turn into authority.

• Added Hypothesis. Such an error occurs when a system claim actually depends on a hypothesis \(h\) that is not among the claims on which the system may currently rely. The relation below records actual dependence, not merely possible derivability. When the system exposes derivation, explanation, or provenance records, this relation may be realized as: \[\begin{align} &\mathsf{DependsOn}_{E,\textit{ctx},t}(m,c,h) \triangleq \exists \pi\in \mathsf{UsedDerivations}_{E,\textit{ctx},t}(m,c)\mathrel{.} \\ &\qquad{} h\in\mathsf{Premises}(\pi) \wedge c\in\textsf{Infer}^{\ast}_{\bar{R}_t}(\mathsf{Premises}(\pi)) \wedge c\notin \textsf{Infer}^{\ast}_{\bar{R}_t} (\mathsf{Premises}(\pi)\setminus\{h\}) . \end{align}\] Here \(\mathsf{UsedDerivations}_{E,\textit{ctx},t}(m,c)\) is the set of derivation, explanation, or provenance records actually used by the system in asserting \(c\) through \(m\), and \(\mathsf{Premises}(\pi)\) is the set of semantic premises used by \(\pi\).

  Let \(\mathcal{R}_{t,\textit{ctx}} \triangleq \{\,c\in\bar{U}\mid \exists m_c\in\textit{Lang}\mathrel{.}\, \mathsf{ReliableClaim}_t( m_c,c; K_{E,\textit{ctx},t},K_{S,\textit{Src},t},K_{U,t}, \textit{ctx})\,\}\). An asserted claim \(c\) in message \(m\) depends on an added hypothesis when the system asserted \(c\), actually used \(h\), \(c\) is justified if we add \(h\) but not justified from currently reliable claims alone, \(h\) itself has no reliable witnessing message \(m_h\), and \(c\) is not otherwise directly supported: \[\begin{align} &\mathsf{AddedHypothesis}_t(h,c;m,\textit{ctx}) \triangleq \mathsf{ClaimUse}_{E,\textit{ctx},t}(m,c) \wedge h\in\bar{U} \wedge \mathsf{DependsOn}_{E,\textit{ctx},t}(m,c,h) \\ &\qquad{}\wedge \neg\,\exists m_h\in\textit{Lang}\mathrel{.}\, \mathsf{ReliableClaim}_t( m_h,h; K_{E,\textit{ctx},t},K_{S,\textit{Src},t},K_{U,t}, \textit{ctx}) \\ &\qquad{}\wedge c\in\textsf{Infer}^{\ast}_{\bar{R}_t} (\mathcal{R}_{t,\textit{ctx}}\cup\{h\}) \wedge c\notin\textsf{Infer}^{\ast}_{\bar{R}_t} (\mathcal{R}_{t,\textit{ctx}}) \wedge \neg\,\mathsf{SupportedClaim}_t(m,c;K_{U,t},K_{S,\textit{Src},t}). \end{align}\]

• Unsupported Use. When does an unsupported claim enter the trace? If \(e\) is a new event extending a trace \(\textit{trace}\) at time \(t\), write \(\textit{trace}'=\textit{trace}\cdot e\). Let \(\textit{ctx}_{t}\in\mathsf{Select}_t(\textit{trace})\) and \(\textit{ctx}_{t+1}\in\mathsf{Select}_{t+1}(\textit{trace}')\) be the selected contexts before and after the extension. An unsupported use is a transition from \(\neg\,\mathsf{Effective}_{+,t}(m,s;K_{E,\textit{ctx}_{t},t})\) to \(\mathsf{Effective}_{+,t+1} (m,s;K_{E,\textit{ctx}_{t+1},t+1})\) while the asserted claim \(c\) still fails the support check: \[\begin{align} &\mathsf{UnsupportedUse}_{t+1} (e,m,s,c;\textit{trace},\textit{ctx}_{t},\textit{ctx}_{t+1}) \triangleq \textit{trace}'=\textit{trace}\cdot e \\ &\quad{}\wedge \textit{ctx}_{t}\in\mathsf{Select}_t(\textit{trace}) \wedge \textit{ctx}_{t+1}\in\mathsf{Select}_{t+1}(\textit{trace}') \wedge e.\mathsf{message}=m \wedge \mathsf{Denotes}_{\textit{Lang}}(m,s) \\ &\quad{}\wedge \neg\,\mathsf{Effective}_{+,t}(m,s;K_{E,\textit{ctx}_{t},t}) \wedge \mathsf{Effective}_{+,t+1} (m,s;K_{E,\textit{ctx}_{t+1},t+1}) \wedge \mathsf{ClaimUse}_{E,\textit{ctx}_{t+1},t+1}(m,c) \\ &\qquad{}\wedge \neg\,\mathsf{SupportedClaim}_{t+1} (m,c;K_{U,t+1},K_{S,\textit{Src},t+1}) . \end{align}\]

7 Compute Components↩︎

Compute components are the engineered interfaces through which an AI system turns input messages into further messages, checks, observations, or actuations.

7.1 Symbolic Components↩︎

A symbolic component features base facts, and inference rules. An inference engine justifies new conclusions from facts, e.g. by forward or backward chaining, DPLL-style search, fixpoint iteration, or another symbolic strategy.

Thus a symbolic component is an abstraction of the rule system \(\bar{R}_t\), more precisely of the rules available after scope restriction and forgetting. This abstraction arises for a number of reasons: some universal rules may not be expressible in the component’s modelling language, some expressible rules may not be implemented or used by the engine, and some speculative or buggy rules may be added although they do not exist in \(\bar{R}_t\).

7.1.1 Definition↩︎

A symbolic component uses a language \(\textit{ModLang}\) that abstracts \(\mathsf{SourceItems}\) (where \(\mathsf{SourceItems}\triangleq \overline{\textit{Scope}}/{\equiv_f}\)). Its intended semantics is \(\mathsf{sem}_{\textit{ModLang}}\in \textit{ModLang}\rightarrow \mathsf{SourceItems}\). Conversely, statements in \(\mathsf{SourceItems}\) must be approximated by \(\textit{ModLang}\): \(\mathsf{encode}_{\textit{ModLang}}\in \mathsf{SourceItems}\rightarrow \textit{ModLang}\). In practice these maps may be implicit: a language such as SMT-LIB is often understood operationally by solvers and users without a fully exposed semantic map. To communicate with the rest of the AI system, the modelling language may be embedded in \(\textit{Lang}\); otherwise the component needs communication encoders and decoders \(\mathsf{enc}_{\textit{ModLang}}\in \textit{Lang}\rightarrow \wp(\textit{ModLang})\) and \(\mathsf{dec}_{\textit{ModLang}}\in \textit{ModLang}\cup\{\bot\}\rightarrow \textit{Lang}\).

For a black-box symbolic component, we can represent the inference engine as \(\textit{inference}_{\textit{ModLang}}\in \wp(\wp(\textit{ModLang})\times(\textit{ModLang}\cup\{\bot\}))\), where \(\bot\) represents timeout, failure, or absence of an answer. This relation abstracts search over \(\overline{\textit{forget}}(\overline{\textit{ignore}}(\bar{R}_t))\), but may omit rules or add incorrect ones.

7.1.2 Scoped correctness↩︎

A symbolic component is correct within the system’s scope if each non-\(\bot\) result it returns corresponds, through \(\mathsf{sem}_{\textit{ModLang}}\), to a consequence of the scoped underlying rules:

\[\begin{align} &\forall H_{\textit{ModLang}}\subseteq\textit{ModLang}\mathrel{.}\, \forall c\in\textit{ModLang}\mathrel{.}\, \bigl( \langle H_{\textit{ModLang}},c\rangle \in\textit{inference}_{\textit{ModLang}} \bigr) \\ &\Rightarrow \mathsf{sem}_{\textit{ModLang}}(c) \in \textsf{Infer}^{\ast}_{R_{S,t}} (\{\mathsf{sem}_{\textit{ModLang}}(h)\mid h\in H_{\textit{ModLang}}\}). \end{align}\]

This is a scoped correctness condition, which must be stated relative to \(\pair{\bar{U}}{\bar{R}_t}\): forgetting can introduce abstract consequences that are not consequences of the ideal rule system.

7.1.3 In practice↩︎

Verification of a symbolic component can use the standard repertoire for transition systems and logic programs: testing, model checking, static analysis, deductive verification, consistency checks, type checks, termination arguments, and runtime verification.

7.2 Neural Components↩︎

A neural component encodes an input into vectors, applies a neural network, and decodes the result into an output. We assume that the component communicates through \(\textit{Lang}\).

Large language models are neural components specialised to token sequences. Their inputs and outputs are messages in \(\textit{Lang}\), typically natural language or token sequences.

7.2.1 Definition↩︎

A neural component is a black box \(\textit{decode}_{N\!N}\circ N\!N\circ\textit{encode}_{N\!N}\in \textit{Lang}\rightarrow \textit{Lang}\), where \(\textit{encode}_{N\!N}\in \textit{Lang}\rightarrow\mathbb{R}^n\), \(N\!N\in\mathbb{R}^n\rightarrow\mathbb{R}^m\), and \(\textit{decode}_{N\!N}\in\mathbb{R}^m\rightarrow \textit{Lang}\) define the encoder \(\textit{encode}_{N\!N}\), the neural network \({N\!N}\) itself and the decoder \(\textit{decode}_{N\!N}\).

The encoder \(\textit{encode}_{N\!N}\) is the interface between communication-level inputs and the input layer of the neural network \({N\!N}\). It maps input data to a fixed-size vector of machine numbers. This encoding is already an abstraction: if relevant information is lost before the network sees the input, the network cannot recover it.

The neural network \({N\!N}\) can be decomposed into transformers between layers \(N\!N=N\!N_\ell\circ\cdots\circ N\!N_1\). The transformers \(N\!N_1\), …, \(N\!N_\ell\) map vectors using weights, calls, and optimisation procedures such as backpropagation and gradient descent. \(N\!N_1\) is the transformer of the input layer into the first hidden layer and is applied first. \(N\!N_\ell\) is the transformer of the last hidden layer into the output layer. This final transformer \(N\!N_\ell\) shapes the result for the task: classification, regression, sequence generation, or another result format.

The decoder \(\textit{decode}_{N\!N}\) translates the result vector back into a communication message in \(\textit{Lang}\).

7.2.2 Output Reliability↩︎

A neural component output is reliable for a selected context when every claim asserted by the output is reliable for that context. Reliability is checked after interpretation by \(\mathsf{denotation}_{\textit{Lang}}\), expansion by \(\mathsf{CandidateClaims}\), assertion selection by \(\mathsf{AssertedClaims}_{E,\textit{ctx},t}\), and the support checks in \(\mathsf{ReliableClaim}_t\).

The reliability obligation on this output is not that every element of \(\mathsf{CandidateClaims}(\textit{output})\) be reliable, but rather that every claim \(c\in\mathsf{AssertedClaims}_{E,\textit{ctx},t}(\textit{output})\) asserted by the output be reliable for the selected context \(\textit{ctx}\): \(\mathsf{ReliableClaim}_t(\textit{output},c; K_{E,\textit{ctx},t},K_{S,\textit{Src},t},K_{U,t},\textit{ctx})\).

7.2.3 In practice↩︎

Validation of neural components is usually empirical. It may test properties of the trained system, using adversarial inputs, invariance tests, boundary cases, and monitoring for data drift. Empirical checks ask whether the test distribution matches the training distribution or whether a measured property points to a failure. PAC-style learning properties concern the learning algorithm rather than a particular trained network. Formal methods can sometimes prove properties of networks, especially small or piecewise-linear networks, but large networks require approximation and abstraction techniques [17]–[19].

7.3 Agent Services↩︎

Agent services enable interactions with the world, e.g. tools, web search, code interpreters, sensors, actuators, access to external servers via the model context protocol (MCP) [20].

7.3.1 Definition↩︎

An agent service \(\textit{Serv}\) is formalised by internal states \(\textit{States}_{\textit{Serv}}\) and a transition relation \(\textit{trans}_{\textit{Serv}}\in \wp((\textit{States}_{\textit{Serv}}\times \textit{Lang}\times \textit{Lang})\times(\textit{States}_{\textit{Serv}}\times \textit{Lang}\times \textit{Lang}))\).

A transition \(\pair{\triple{s_{\textit{Serv}}}{m_{ai}}{m_w}} {\triple{s'_{\textit{Serv}}}{m'_{ai}}{m'_w}} \in\textit{trans}_{\textit{Serv}}\) means that the service is in state \(s_{\textit{Serv}}\), reads a communication message \(m_{ai}\) from the AI system, reads the observed world message \(m_w=\mathsf{observation}(\textit{Serv},w)\), changes its internal state to \(s'_{\textit{Serv}}\), returns a communication message \(m'_{ai}\) to the AI system, and may request a world update represented by \(m'_w\), producing \(w'=\mathsf{actuation}(w,m'_w)\).

7.3.2 Service Conformance↩︎

A conformance relation for a service Serv has the form \(\textit{trans}_{\textit{Serv}}\subseteq \textsf{Spec}_{\textit{Serv}}\) where \(\textsf{Spec}_{\textit{Serv}}\in \wp((\textit{States}_{\textit{Serv}}\times \textit{Lang}\times \textit{Lang})\times(\textit{States}_{\textit{Serv}}\times \textit{Lang}\times \textit{Lang}))\) is the relational input-output specification.

Because agent services are transition systems, standard specification and validation methods apply: testing, code review, model checking, static analysis, deductive verification, and runtime monitoring. These checks do not establish soundness of the whole system per se.

7.3.3 In practice↩︎

The specification of an agent service is application dependent. A service may otherwise behave arbitrarily, e.g. modify an account it should not. Some task services should eventually return an answer, but termination is not universal for monitoring or reactive services. Beyond safety and liveness, services may need to satisfy, e.g., confidentiality or privacy.

7.3.4 Prompt↩︎

The Prompt is an example of an agent service, which takes information and directives as input. In response to prompts, an LLM may produce messages in Lang, which are added to the orchestrator state (including information recorded in the context ctx).

7.4 Orchestration↩︎

The orchestrator coordinates the calls and communications of symbolic or neural components, and agent services. This part of the AI system selects which component to call, passes messages through \(\textit{Lang}\), records intermediate state, and handles observations or updates of the world.

The user normally interacts with the orchestrator through prompts in \(\textit{Lang}\). Commands such as shell commands, web requests, code execution, or file writes are represented as service calls and actuations mediated by the orchestrator.

7.4.1 Definition↩︎

Let \(W\) be the world and let the components of an orchestrator be

• Language \(\textit{Lang}\) with \(\mathsf{denotation}_{\textit{Lang}}\), \(\mathsf{CandidateClaims}\), \(\mathsf{observation}\), and \(\mathsf{actuation}\);

• Symbolic components \(\quadruple{\textit{ModLang}}{\mathsf{enc}_{\textit{ModLang}}} {\mathsf{dec}_{\textit{ModLang}}}{\textit{inference}_{\textit{ModLang}}} \in \textit{Symbolic}\);

• Neural components \(\triple{\textit{encode}_{N\!N}}{N\!N}{\textit{decode}_{N\!N}}\in \textit{Neural}\);

• Agent services \(\pair{\textit{States}_{\textit{Serv}}} {\textit{trans}_{\textit{Serv}}}\in \textit{Services}\).

An orchestrator has internal states \(s_{\textit{Orch}}\in \textit{States}_{\textit{Orch}}\). The orchestrator also records the states \(s_{\textit{Serv}}\) indexed by services \(\textit{Serv}\in \textit{Services}\), although these states can only be read and modified by their services. It communicates with the components through messages in \(\textit{Lang}\) and with the world through \(\mathsf{observation}\) and \(\mathsf{actuation}\). Together these form a closed system, whose states are: \[\textit{ClosedSystemStates}\triangleq \textit{States}_{\textit{Orch}}\times \prod_{\textit{Serv}\in \textit{Services}} \textit{States}_{\textit{Serv}}\times W\times\mathsf{Trace}.\] Its transition relation \(\textit{trans}_{\textit{Orch}}\in \wp((\textit{ClosedSystemStates}\times\textit{Lang})\times \textit{ClosedSystemStates})\) reacts to an input in Lang and includes world changes, such as a doorbell ringing, that the orchestrator did not cause but may later observe.

There are five kinds of orchestrator transitions: call a symbolic or neural component, an agent service (including prompts), update an internal state, or observe a world change.

Let \(s_{\textit{Closed}}\triangleq\quadruple{s_{\textit{Orch}}}{\vec{s}_{\textit{Serv}}}{w}{\textit{trace}}\) and \(s'_{\textit{Closed}}\triangleq\quadruple{s'_{\textit{Orch}}}{\vec{s}\,'_{\!\textit{Serv}}}{w'}{\textit{trace}'}\), where \(\vec{s}_{\textit{Serv}}\) is the family of service states and \(\textit{trace}\) is the event trace. For \(\textit{Comp}\in\{\textit{Symbolic},\textit{Neural},\textit{Service}, \textit{Internal},\textit{World}\}\), the transition relations are \(\textit{trans}_{\textit{Orch}}^{\textit{Comp}} \subseteq (\textit{ClosedSystemStates}\times\textit{Lang})\times\textit{ClosedSystemStates}\).

The orchestrator transition relation is their union: \(\textit{trans}_{\textit{Orch}}\triangleq\bigcup_{\textit{Comp}}\textit{trans}_{\textit{Orch}}^{\textit{Comp}}\). Thus each transition in \(\textit{trans}_{\textit{Orch}}\) satisfies at least one of the following clauses. The symbol \(m'\), when it appears below, names a message produced inside the transition and recorded in \(s'_{\textit{Closed}}\) or in the appended event; it is not a separate output of \(\textit{trans}_{\textit{Orch}}\).

• Service: the orchestrator calls a tool, sensor, actuator, browser, client, or other service. The service may observe the world and may request a world update. For services that do not observe the world, we use a distinguished no-observation message \(o_{\bot}\in\textit{Lang}\), and stipulate that \(\mathsf{observation}(\textit{Serv},w)=o_{\bot}\). For services that do not request a world update, we use a distinguished no-actuation message \(m_{\bot}\in\textit{Lang}\), and stipulate that \(\mathsf{actuation}(w,m_{\bot})=w\). Let \(\mathsf{NoActuation}(\textit{Serv})\) mark services that cannot request world updates. Thus the following clause treats observation and actuation uniformly; actual read-only or write-free services are represented by these no-op messages. Formally, if \(\pair{\pair{s_{\textit{Closed}}}{m}}{s'_{\textit{Closed}}} \in\textit{trans}_{\textit{Orch}}^{\textit{Service}}\), then there exist \(\textit{Serv}\in\textit{Services}\) with transition structure \(\pair{\textit{States}_{\textit{Serv}}} {\textit{trans}_{\textit{Serv}}}\), an observation message \(o\in\textit{Lang}\), a world-update message \(m'_w\in\textit{Lang}\), and an event \(e'\in\textit{Ev}\) such that \(o=\mathsf{observation}(\textit{Serv},w)\), \(\pair{ \triple{\vec{s}_{\textit{Serv}}(\textit{Serv})}{m}{o}} {\triple{\vec{s}\,'_{\!\textit{Serv}}(\textit{Serv})}{m'}{m'_w}} \in\textit{trans}_{\textit{Serv}}\), \(\bigl(\mathsf{NoActuation}(\textit{Serv}) \Rightarrow m'_w=m_{\bot}\bigr)\), \(w'=\mathsf{actuation}(w,m'_w)\), and \(\vec{s}\,'_{\!\textit{Serv}}(\textit{OtherServ}) =\vec{s}_{\textit{Serv}}(\textit{OtherServ})\) for all \(\textit{OtherServ}\in \textit{Services}\setminus\{\textit{Serv}\}\), \(e'.\mathsf{kind}=\textit{Service}\), \(e'.\mathsf{message}=m'\), and \(\textit{trace}'=\textit{trace}\cdot e'\). The service reads the communication message \(m\), observes the world through \(\mathsf{observation}\), returns a message \(m'\) recorded in \({s'_{\textit{Closed}}}\), and updates the world through \(\mathsf{actuation}\). No-observation and no-actuation services use the distinguished no-op messages above.

• Symbolic: the orchestrator calls a symbolic component by sending a message in Lang which is encoded by \(\mathsf{enc}_{\textit{ModLang}}\), receives a result which is decoded by \(\mathsf{dec}_{\textit{ModLang}}\) into Lang. This message back is recorded by the orchestrator in its next state \(s'_{\textit{Closed}}\). Formally, if \(\pair{\pair{s_{\textit{Closed}}}{m}}{s'_{\textit{Closed}}} \in\textit{trans}_{\textit{Orch}}^{\textit{Symbolic}}\), then there exist \(\quadruple{\textit{ModLang}}{\mathsf{enc}_{\textit{ModLang}}} {\mathsf{dec}_{\textit{ModLang}}}{\textit{inference}_{\textit{ModLang}}} \in \textit{Symbolic}\), a hypothesis set \(H\subseteq\textit{ModLang}\), a result \(r\in\textit{ModLang}\cup\{\bot\}\), and an event \(e'\in\textit{Ev}\) such that \(H=\mathsf{enc}_{\textit{ModLang}}(m)\), \(\pair{H}{r}\in\textit{inference}_{\textit{ModLang}}\), \(m'=\mathsf{dec}_{\textit{ModLang}}(r)\), \({\vec{s}\,'_{\!\textit{Serv}}}=\vec{s}_{\textit{Serv}}\), \(w'=w\), \(e'.\mathsf{kind}=\textit{Symbolic}\), \(e'.\mathsf{message}=m'\), \(e'.\mathsf{observation}=o_{\bot}\), \(e'.\mathsf{actuation}=m_{\bot}\) (the distinguished no-observation and no-actuation messages of the Service clause above), and \(\textit{trace}'=\textit{trace}\cdot e'\). The orchestrator state changes from \(s_{\textit{Orch}}\) to \(s'_{\textit{Orch}}\) to record the call and its result.

• Neural: the orchestrator calls a neural component by sending a message \(m\in\textit{Lang}\), receives a generated message \(m'\), and records the step and its result \(m'\) in its next state \({s'_{\textit{Closed}}}\). Formally, if \(\pair{\pair{s_{\textit{Closed}}}{m}}{s'_{\textit{Closed}}} \in\textit{trans}_{\textit{Orch}}^{\textit{Neural}}\), then there exists \(\triple{\textit{encode}_{N\!N}}{N\!N}{\textit{decode}_{N\!N}}\in \textit{Neural}\) and an event \(e'\in\textit{Ev}\) such that \(m'=\textit{decode}_{N\!N}(N\!N(\textit{encode}_{N\!N}(m))), {\vec{s}\,'_{\!\textit{Serv}}}= \vec{s}_{\textit{Serv}}\), \(w'=w\), \(e'.\mathsf{kind}=\textit{Neural}\), \(e'.\mathsf{message}=m'\), \(e'.\mathsf{observation}=o_{\bot}\), \(e'.\mathsf{actuation}=m_{\bot}\), and \(\textit{trace}'=\textit{trace}\cdot e'\). For a large language model LLM, \(m' = \textit{decode}_{\textit{LLM}}(\textit{NN}(\textit{encode}_{\textit{LLM}}(m)))\) is the call to LLM on a context window, \(\textit{encode}_{\textit{LLM}}\) feeds the selected context window and \(\textit{decode}_{\textit{LLM}}\) records the generated token sequence. Updating the context window is an orchestrator-state update.

• Internal: the orchestrator changes its own state, for example to route, pause, resume, update context, or choose the next control label. Formally, if \(\pair{\pair{s_{\textit{Closed}}}{m}}{s'_{\textit{Closed}}} \in\textit{trans}_{\textit{Orch}}^{\textit{Internal}}\), then \({\vec{s}\,'_{\!\textit{Serv}}}={\vec{s}_{\textit{Serv}}}\), \(w'=w\), and \(\textit{trace}'=\textit{trace}\). The internal state change from \(s_{\textit{Orch}}\) to \(s'_{\textit{Orch}}\) can reflect control flow and local computations (as in the state-based small-step operational semantics of programming languages). Any communication message produced by the internal step is recorded in \(s'_{\textit{Orch}}\) or in a later event, rather than as a separate output of \(\textit{trans}_{\textit{Orch}}\).

• World: the world changes independently, e.g. because the doorbell rings. If the mutation is unobserved, the trace can remain unchanged; when the system observes or records the mutation, that later observation has an event. Formally, if \(\pair{\pair{s_{\textit{Closed}}}{m}}{s'_{\textit{Closed}}} \in\textit{trans}_{\textit{Orch}}^{\textit{World}}\), then \({s'_{\textit{Orch}}}={s_{\textit{Orch}}}\), \({\vec{s}\,'_{\!\textit{Serv}}}={\vec{s}_{\textit{Serv}}}\), \(\textit{trace}'=\textit{trace}\), since only the world changes from \(w\) to \(w'\). A later read or service call may observe the new world state and update the orchestrator state.

7.4.2 Orchestrator Invariants↩︎

Orchestrator validation is mostly validation of the AI system as a whole. Some properties can nevertheless be checked at the orchestration layer. For safety properties one can define an orchestration invariant \(I \in\wp(\textit{ClosedSystemStates})\) which must be proved to hold initially and remains true after each transition \(\textit{trans}_{\textit{Orch}}\). Since \(\textit{trans}_{\textit{Orch}}\) includes external mutations of the world, such a proof must also state the admissible environment steps. Equivalently, one proves invariance for AI-controlled steps and assumes an environment relation \(Env\subseteq W\times W\) for external changes allowed by the model of the world.

Liveness properties are more application specific, such as: a reactive orchestrator should not terminate before receiving a termination condition, the body of a reactive cycle should terminate when it is meant to, forbidden services should not be reachable from a given prompt class, and service results should be inserted into the context only through the specified communication channel. Variant functions can prove termination or progress of bounded phases. Recurrent obligations need temporal assumptions such as fairness or explicit scheduling.

8 AI systems↩︎

An AI system is the whole engineered system that connects knowledge, prompts, components, services, orchestration, and actuations.

8.1 Definition↩︎

This section describes an AI system as a combination of components that communicate through a common language, may interact with the world, and be orchestrated, as shown in Figure [fig:AISystem]

An AI system is \(\langle \mathsf{Information\;State},\mathsf{Components}, \mathsf{Orchestrator},\mathsf{Interface},\mathsf{Claims}, \mathsf{Specifications}\rangle\):

• \(\mathsf{Information\;State} \triangleq \langle \textit{Src}_t,K_{U,t},K_{S,\textit{Src},t},K_{E,\textit{ctx},t}\rangle\) is the information-state layer: the reference sources \(\textit{Src}_t\), the universal knowledge base \(K_{U,t}\), the source-derived knowledge \(K_{S,\textit{Src},t}\), and the AI system’s effective working knowledge \(K_{E,\textit{ctx},t}\).

• \(\mathsf{Components} \triangleq \langle \textit{Symbolic},\textit{Neural},\textit{Services}\rangle\) is the components layer: \(\textit{Symbolic}\) components, \(\textit{Neural}\) components, and \(\textit{Services}\) e.g. prompts, tools, sensors, browsers, APIs, or actuators.

• \(\mathsf{Orchestrator} \triangleq \langle \textit{States}_{\textit{Orch}},\textit{trans}_{\textit{Orch}}\rangle\) is the orchestrator layer: the orchestrator states \(\textit{States}_{\textit{Orch}}\), including control state, selected context ctx, memory and trace pointers, routing information, and the transition relation \(\textit{trans}_{\textit{Orch}}\) that advances the closed system by calling components, services, updating internal state, observing world changes, or producing messages and world updates.

• \(\mathsf{Interface} \triangleq \langle \textit{Lang},W,\textit{Ev},\mathsf{Trace}, \mathsf{observation},\mathsf{actuation}\rangle\) is the interface layer: the communication language \(\textit{Lang}\), the set \(W\subseteq \bar{U}\) of possible world states, the event records \(\textit{Ev}\), the traces \(\mathsf{Trace}=\textit{Ev}^\ast\), the \(\mathsf{observation}\) interface from the world into the system, and the \(\mathsf{actuation}\) interface by which system messages may change the world.

• The claims layer is: \[\begin{align} \quad\mathsf{Claims}\triangleq \langle{}& \mathsf{denotation}_{\textit{Lang}}, \mathsf{CandidateClaims}, \mathsf{Asserts}_{E,\textit{ctx},t}, \\ \quad& \mathsf{AssertedClaims}_{E,\textit{ctx},t}, \mathsf{SourceSupport}_t, \mathsf{SupportedClaim}_t, \mathsf{ReliableClaim}_t, \mathsf{DependsOn}_{E,\textit{ctx},t} \rangle . \end{align}\] It contains the maps, application-specific relations, and judgments that connect communication-level items to underlying semantic claims. Messages map to intended source items via \(\mathsf{denotation}_{\textit{Lang}}\). \(\mathsf{CandidateClaims}\) maps messages in Lang to candidate semantic meanings. \(\mathsf{Asserts}_{E,\textit{ctx},t}\) selects which candidate claims are actually asserted, and \(\mathsf{SourceSupport}_t\) records which source items support which semantic claims. The remaining judgments separate assertion, external support, reliability, and actual derivational dependence.

• The specifications layer is: \[\begin{align} \mathsf{Specifications}\triangleq\langle{}& \mathsf{AllowedEvent}_{\textsf{Spec}}, \mathsf{worldmap}_{\textsf{Spec}}, \mathsf{interp}_{\textsf{Spec}}, \mathsf{Requires}_{\textsf{Spec}}, \\ & \mathsf{CurrentWitnessesOK}_{\textsf{Spec}}, \mathsf{AuthorityOK}_{\textsf{Spec}}, \mathsf{ActuationOK}_{\textsf{Spec}} \rangle . \end{align}\] It says which observations, actions, and other candidate events are sound; the specification-relative map from world states to semantic facts; the specification-relative map from event records to semantic claims or records; the specification-relative map from trace and world states to required semantic claims; and the checks for current witnesses, authority, and permitted actuation. It is checked against the trace, the current world state, and the candidate event, using the semantic record when semantic context is needed.

8.2 Specifications↩︎

Specifications state which system-controlled events are permitted, so that traces can be checked against the semantic and operational obligations the system is meant to respect. For simplicity, we assume that a specification Spec requires universally positive claims.

Let \(\textit{trace}=e_1\ldots e_n\in\mathsf{Trace}\) be the event trace so far, let \(w_t\in W\) be the current world state, and let \(e\in \textit{Ev}\) be the next event. A specification supplies: \[\begin{align} \mathsf{worldmap}_{\textsf{Spec}} &: W\rightharpoonup \wp(\bar{U}), & \mathsf{AuthorityOK}_{\textsf{Spec}} &: \mathsf{Trace}\times W\times\textit{Ev} \rightarrow\{\mathsf{true},\mathsf{false}\},\\ \mathsf{interp}_{\textsf{Spec}} &: \textit{Ev}\rightharpoonup \wp(\bar{U}), &\mathsf{ActuationOK}_{\textsf{Spec}} &: \mathsf{Trace}\times W\times\textit{Ev}\times W \rightarrow\{\mathsf{true},\mathsf{false}\},\\ \mathsf{Requires}_{\textsf{Spec}} &: \mathsf{Trace}\times W \rightarrow \wp(\bar{U}), &\mathsf{AllowedEvent}_{\textsf{Spec}} &: \mathsf{Trace}\times W \times \textit{Ev} \rightarrow\{\mathsf{true},\mathsf{false}\}. \\ \rlap{\mathsf{CurrentWitnessesOK}_{\textsf{Spec}}: \mathsf{Trace}\times W\times\textit{Ev} \rightarrow\{\mathsf{true},\mathsf{false}\}.} \end{align}\] For a partial map \(f:X\rightharpoonup Y\), write \(f(x)\downarrow\) when \(f(x)\) is defined and \(f(x)\uparrow\) when it is undefined; definedness does not require \(f(x)\) to be nonempty when \(Y\) is a powerset. Here \(\mathsf{worldmap}_{\textsf{Spec}}(w)\) records the semantic facts about world state \(w\) that matter to \(\textsf{Spec}\), while \(\mathsf{interp}_{\textsf{Spec}}(e)\) records the semantic content of event \(e\): what it claims, records, witnesses, authorizes, observes, or changes. The set \(\mathsf{Requires}_{\textsf{Spec}}(\textit{trace},w_t)\) records the task-relevant semantic claims that \(\textsf{Spec}\) requires at the current trace and world state. The predicates \(\mathsf{CurrentWitnessesOK}_{\textsf{Spec}}\), \(\mathsf{AuthorityOK}_{\textsf{Spec}}\), and \(\mathsf{ActuationOK}_{\textsf{Spec}}\) record the remaining acceptance obligations checked by the safeguard: witness freshness, permission or delegation, and whether the candidate actuation from \(w_t\) to \(w'\) is permitted. The content of \(\mathsf{worldmap}_{\textsf{Spec}}\) is the reference against which an application instantiates \(\mathsf{Requires}_{\textsf{Spec}}\) and \(\mathsf{ActuationOK}_{\textsf{Spec}}\), which may consult it when relating required claims and permitted updates to the current and proposed world states.

If \(\mathsf{worldmap}_{\textsf{Spec}}(w_t)\uparrow\), some prior \(\mathsf{interp}_{\textsf{Spec}}(e_i)\uparrow\), or \(\mathsf{interp}_{\textsf{Spec}}(e)\uparrow\), then \(e\) is not checkable under \(\textsf{Spec}\) and is not valid; an implementation may reject, pause, or route to fallback.

\(\mathsf{AllowedEvent}_{\textsf{Spec}}\) lists the constraints given by Spec. If \(e\) is an external mutation, user action, or other event not controlled by the system, there is no direct requirement on the system. There may still be invariants, e.g. the orchestrator state must remain consistent with the resulting world state once the event is observed. If \(e\) is performed by the system then the specification can require \(\mathsf{AllowedEvent}_{\textsf{Spec}}(\textit{trace},w_t,e)\). We write \(\mathsf{SystemControlled}(e)\) when \(e\) is performed by the system, rather than by a user, external agent, or the world. For reads, this can express e.g. that the private information is not read, or the read belongs to the user-specified boundaries. For writes, this can express e.g. that private information is not modified, or an actuation had the required authority.

9 Soundness of Controlled Transitions↩︎

Here we examine what it means for the orchestrator to make sound transitions. Controlled transition soundness requires every system-controlled step to be justified before it goes ahead.

9.1 Conditions on events and orchestrator steps↩︎

Events and orchestrator steps connect messages to state changes, so each step must record that the event, message, interface interpretation, and resulting transition agree. We define a number of concepts to do so:

• Reliable assertions. This says that the claims made by the message of an event \(e\) are reliable: \[\begin{align} &\mathsf{ReliableAssertions}_{t,\textit{ctx}}(\textit{trace};e) \triangleq |\textit{trace}|=t \wedge \textit{ctx}\in\mathsf{Select}_t(\textit{trace}) \\ &\quad{}\wedge \forall c\in \mathsf{AssertedClaims}_{E,\textit{ctx},t}(e.\mathsf{message}) \mathrel{.}\\ &\quad{} \mathsf{ReliableClaim}_t(e.\mathsf{message},c; K_{E,\textit{ctx},t}, K_{S,\textit{Src},t},K_{U,t},\textit{ctx}) . \end{align}\]

• Validity. This says that the event is meaningful and that every claim asserted by its message may be relied upon in every selected context. It does not itself assert \(\mathsf{AllowedEvent}_{\textsf{Spec}}\): \[\begin{align} &\mathsf{Validity}_{t,\textsf{Spec}}(\textit{trace},w;e) \triangleq |\textit{trace}|=t \wedge \mathsf{worldmap}_{\textsf{Spec}}(w)\downarrow \wedge \bigl(\forall e_j\in\textit{trace}\mathrel{.}\, \mathsf{interp}_{\textsf{Spec}}(e_j)\downarrow\bigr) \\ &\quad{}\wedge \mathsf{interp}_{\textsf{Spec}}(e)\downarrow \wedge \forall\textit{ctx}\in\mathsf{Select}_t(\textit{trace})\mathrel{.}\, \mathsf{ReliableAssertions}_{t,\textit{ctx}}(\textit{trace};e). \end{align}\]

• Interface Agreement. The event record must match what the observation and actuation interfaces actually did: \[\begin{align} &\mathsf{InterfaceOK}(\textit{Serv},e,w,w') \triangleq \textit{Serv}\in\textit{Services} \wedge \bigl( e.\mathsf{observation}=o_{\bot} \vee e.\mathsf{observation}={}\\ &\quad{}\mathsf{observation}(\textit{Serv},w) \bigr)\\ &\quad{} \wedge \bigl( (e.\mathsf{actuation}=m_{\bot}\wedge w'=w) \vee \mathsf{actuation}(w,e.\mathsf{actuation})=w' \bigr). \end{align}\] Here \(\textit{Serv}\) is the service whose observation interface is being checked, and \(o_{\bot}\) and \(m_{\bot}\) are the no-observation and no-actuation messages used by the service semantics.

• Step Satisfies Interface. We define the derived step relation \[\begin{align} &\mathsf{Step}_{\textit{Orch}} (s,\vec{s},\textit{trace},w,e, s',\vec{s}',w') \\ &\quad\triangleq \exists m\in\textit{Lang}\mathrel{.} \bigl\langle \bigl\langle \langle s,\vec{s},w,\textit{trace}\rangle, m \bigr\rangle, \langle s',\vec{s}',w',\textit{trace}\cdot e\rangle \bigr\rangle \in\textit{trans}_{\textit{Orch}} . \end{align}\]

  Now, this invariant says that the step taken satisfies the interface agreement: \[\begin{align} &\mathsf{StepOK}(\mathsf{Step}_{\textit{Orch}}) \triangleq \forall s,\vec{s},s',\vec{s}',\textit{trace},w,w',e\mathrel{.}\\ &\qquad \mathsf{Step}_{\textit{Orch}} (s,\vec{s},\textit{trace},w,e,s',\vec{s}',w') \Rightarrow \exists \textit{Serv}\in\textit{Services}\mathrel{.}\, \mathsf{InterfaceOK}(\textit{Serv},e,w,w'). \end{align}\]

9.2 Transition Safeguard↩︎

A transition safeguard is a check that determines whether a proposed system action has enough reliable support, authority and freshness to proceed. Before adding \(e\) to the trace, it would be desirable for an orchestrator to run \(\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx})\). At a high-level, the safeguard either accepts the event \(e\) or rejects it. Here we discuss the acceptance case, and rejection cases are discussed later in Section 9.3:

• Acceptance. A result \(\mathsf{Accept}(e,w')\) records \(e\) and commits the world update \(w'\). We write: \[\mathsf{SafeguardAccept}_{\textsf{Spec}} (\textit{trace},w,e,w',\textit{ctx}) \triangleq\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx}) =\mathsf{Accept}(e,w').\]

• Acceptance certificate. An acceptance result is not itself a proof that \(e\) is allowed. The safeguard must establish a structured certificate. First, every claim required by \(\textsf{Spec}\) at the current trace and world must have a reliable message: \[\begin{align} &\mathsf{RequiredClaimsOK}_{\textsf{Spec},t,\textit{ctx}} (\textit{trace},w;e) \triangleq |\textit{trace}|=t \wedge \textit{ctx}\in\mathsf{Select}_t(\textit{trace}) \\ &\quad{}\wedge \forall c\in\mathsf{Requires}_{\textsf{Spec}}(\textit{trace},w) \mathrel{.}\, \exists m_c\in\textit{Lang}\mathrel{.}\\ &\quad{} \mathsf{ReliableClaim}_t(m_c,c; K_{E,\textit{ctx},t}, K_{S,\textit{Src},t},K_{U,t},\textit{ctx}) . \end{align}\] \(\mathsf{Validity}\) ranges over every context in \(\mathsf{Select}_t(\textit{trace})\) since a later call may select differently from the same trace, whereas \(\mathsf{RequiredClaimsOK}\) fixes the single context under which the safeguard runs and whose reliable messages it can actually inspect. The remaining certificate predicates are specification-relative checks: \(\mathsf{CurrentWitnessesOK}\) checks that required witnesses are present and not invalidated, \(\mathsf{AuthorityOK}\) checks permission and delegation, and \(\mathsf{ActuationOK}\) checks that the proposed world update is permitted. The complete acceptance certificate is: \[\begin{align} &\mathsf{AcceptOK}_{\textsf{Spec},t,\textit{ctx}} (\textit{trace},w,e,w') \triangleq \mathsf{Validity}_{t,\textsf{Spec}}(\textit{trace},w;e) \wedge \mathsf{RequiredClaimsOK}_{\textsf{Spec},t,\textit{ctx}} (\textit{trace},w;e) \\ &\quad{}\wedge \mathsf{CurrentWitnessesOK}_{\textsf{Spec}}(\textit{trace},w;e) \wedge \mathsf{AuthorityOK}_{\textsf{Spec}}(\textit{trace},w;e) \\ &\quad{}\wedge \mathsf{ActuationOK}_{\textsf{Spec}}(\textit{trace},w;e,w') . \end{align}\]

• Acceptance adequacy and safeguard soundness. Acceptance adequacy is the declarative specification claim that the acceptance certificate is strong enough to imply that the event is allowed: \[\begin{align} &\mathsf{AcceptAdequate}_{\textsf{Spec}} \triangleq\\ &\quad \forall \textit{trace},w,e,w',\textit{ctx}\mathrel{.}\, \mathsf{AcceptOK}_{\textsf{Spec},|\textit{trace}|,\textit{ctx}} (\textit{trace},w,e,w') \\ &\qquad\Rightarrow \mathsf{AllowedEvent}_{\textsf{Spec}}(\textit{trace},w,e). \end{align}\] The implementation-level safeguard contract says that every accept result comes with such a certificate: \[\begin{align} &\mathsf{SafeguardAcceptSound}_{\textsf{Spec}} (\mathsf{Safeguard}_{\textsf{Spec}}) \triangleq\\ &\quad \forall \textit{trace},w,e,w',\textit{ctx}\mathrel{.}\, \mathsf{Safeguard}_{\textsf{Spec}} (\textit{trace},w,e,w',\textit{ctx}) =\mathsf{Accept}(e,w') \\ &\qquad\Rightarrow \mathsf{AcceptOK}_{\textsf{Spec},|\textit{trace}|,\textit{ctx}} (\textit{trace},w,e,w'). \end{align}\]

• Valid step. A valid step is a system-controlled orchestrator step whose proposed event has been accepted by the safeguard: \[\begin{align} &\mathsf{ValidStep}_{\textsf{Spec}} (\mathsf{Step}_{\textit{Orch}}, \mathsf{Safeguard}_{\textsf{Spec}}, \textit{trace},w,w',e,\textit{ctx}, s,\vec{s},s',\vec{s}') \triangleq && \\ &\quad \mathsf{Step}_{\textit{Orch}} (s,\vec{s},\textit{trace},w,e, s',\vec{s}',w') \wedge \mathsf{SystemControlled}(e) \wedge \mathsf{SafeguardAccept}_{\textsf{Spec}} (\textit{trace},w,e,w',\textit{ctx}). && \end{align}\]

An accepted controlled transition is sound when the safeguard acceptance is sound, the acceptance certificate is adequate, and the recorded step agrees with the observation/actuation interfaces:

9.3 Rejection diagnostics↩︎

Safeguard rejection has several cases: for controlled-transition soundness, every rejected transition must identify a failed semantic obligation for \(\mathsf{AcceptOK}\), i.e. reliable support, current witness, authority, or allowed actuation. These obligations are not properties one could prove of an arbitrary safeguard; like the acceptance contract \(\mathsf{SafeguardAcceptSound}_{\textsf{Spec}}\), they define the implementation-level rejection contract.

Reject-soundness ties each rejection to a true failure statement. To conclude that a rejected transition refutes the acceptance certificate \(\mathsf{AcceptOK}\), the failure predicates must also refute the corresponding certificate predicates \(\mathsf{CurrentWitnessesOK}_{\textsf{Spec}}\), \(\mathsf{AuthorityOK}_{\textsf{Spec}}\), and \(\mathsf{ActuationOK}_{\textsf{Spec}}\), which Spec otherwise leaves opaque. This is a coherence condition on Spec alone:

Under these two assumptions, diagnostic adequacy is a genuine implication: every rejection refutes an actual conjunct of the acceptance certificate.

Together with acceptance soundness, a total safeguard then decides the certificate:

10 Related Work↩︎

Our framework draws on abstraction, formal semantics, and many-valued accounts of knowledge: abstract interpretation supports reasoning about precise objects through explicit approximations [22]; trivalent, epistemic, and Belnap–Dunn/FDE logics separate truth, falsity, uncertainty, belief, knowledge, both, and neither [23]–[26]; and denotational semantics gives mathematical meanings to computational expressions independently of implementation [27], [28]. Galton’s critique helps delimit our scope: we do not offer a theory of natural-language meaning, but a formal account of when messages, source-derived items, and universal claims may justify reliance in an agentic execution trace [29], with our treatment of messages as signs echoing Peirce’s semiotic epistemology and Frege’s distinction between expression, sense, and reference [30], [31].

Justification logic, truth maintenance, and belief revision make evidence, dependency, retraction, and theory change explicit [32]–[36]. Our witness fields, status predicates, and diagnostics adapt this tradition to trace events and source items, checking whether reliance is supported, stale, refuted, or hypothesis-dependent rather than maintaining a reasoner’s full belief state. Provenance, audit, and runtime-verification systems provide the operational analogue: they record lineage, derivations, and violations in executions and logs [37]–[42]. Our records differ in requiring semantic support relative to \(K_{S,\textit{Src},t}\) and \(K_{U,t}\), not lineage alone; evidence logic and attribution evaluation give the corresponding epistemic and empirical views of \(\mathsf{Asserts}_{E,\textit{ctx},t}\) and \(\mathsf{SourceSupport}_t\) [43]–[45].

Prompt programming and prompt-containing software treat prompts as program-like artefacts with constraints, control flow, maintenance obligations, and tests [46]–[48]. Retrieval-augmented and citation-bearing generation improve the use of external documents, while work on language models as knowledge bases and knowledge conflicts studies the tension between parametric knowledge, retrieved context, and conflicting sources [49]–[55]. For us prompts constrain proof/search over \(K_{E,\textit{ctx},t}\), whereas retrieval and citation mechanisms populate or test \(K_{S,\textit{Src},t}\); neither model fluency nor a source pointer alone establishes truth in \(K_{U,t}\).

Formal methods for AI and machine-learning components verify properties of workflows or models, often treating a neural network as a mathematical function with a specification [17], [18], [56], [57]. Checked-generation systems e.g. WybeCoder, SAIL, formal-method-guided vibe coding, and intent-formalization work put LLM outputs inside verifier, repair, proof-obligation, or specification loops [58]–[62]. We treat these as component-level or artefact-level guarantees inside a wider system semantics that also includes sources, prompts, traces, authority, and world-changing actions.

Work on tool use, agents, and harness engineering studies the infrastructure around language models: modular tools, API calls, reasoning/action loops, memory, orchestration, environments, benchmarks, observability, verification, and governance [63]–[76]. Our abstraction is stack-neutral: a tool is an agent service, a tool call is an event, a result is a witness only relative to a specification, and orchestration is part of the transition system that builds traces and effective knowledge.

Recent formal and systems work on secure LLM agents constrains the agent through the surrounding harness rather than trusting the model itself. AgentSpec and Progent introduce domain-specific policy languages for runtime constraints and privilege control over tool calls; CaMeL, Fides, RTBAS, and IsolateGPT instead emphasize data/control-flow separation, information-flow labels, and execution isolation; and Schlapbach gives a process-calculus semantics for schema-guided dialogue and MCP agent-tool protocols [77]–[83]. These works are closest to our treatment of tools as agent services and tool calls as trace events. Our distinction is that a tool result is not itself a fact: it becomes a witness only relative to source-derived knowledge, universal knowledge, effective knowledge, and the validity condition on the event trace.

This also connects to works on policy logics, runtime enforcement, and proof-carrying evidence: authorization languages such as SecPAL, Ponder, XACML, and Binder give logics for permissions, delegation, and obligations; execution monitors and edit automata characterize which trace properties can be enforced at runtime; proof-carrying code and certifying algorithms show how untrusted outputs can be accompanied by independently checkable evidence [84]–[93].

Finally, control theory, runtime assurance, agent verification, and agent security provide languages for constraining behaviour over time [94]–[108]. Agent-security works treat the model as an untrusted component and enforce invariants through the surrounding system [78], [109], [110]. We adopt the same systems stance, but make the semantic objects explicit: observations, actuations, authority, witnesses, event specifications, and the difference between generated representations and the objects they purport to represent.

11 Conclusion↩︎

An AI system output is not the object it represents: a generated answer, filled form, citation, or action must be interpreted and examined against the universal knowledge base \(K_{U,t}\), the source-derived knowledge \(K_{S,\textit{Src},t}\), and the AI system’s effective knowledge \(K_{E,\textit{ctx},t}\).

Issues arise when these are conflated: outdated guidance treated as being current, plausible output as justified claim. Our framework makes these distinctions explicit. Messages denote source items, and generate candidate claims via the denotation of their source items; candidate claims require support from the universal and source-derived knowledge bases; and actuations must also satisfy event specifications and authority constraints.

We do not suggest that finding the universal knowledge base is always feasible. Our contribution is to locate where obligations sit: by separating representation from object, source from domain knowledge, effective knowledge from authority, and trace evidence from world state, we obtain a vocabulary for specifying and checking AI systems.

12 Theorems and Proofs↩︎

This appendix gives proof sketches for our theorems.

12.1 Theorem 1: Exhaustiveness↩︎

12.2 Theorem 2: Trace soundness↩︎

12.3 Theorem 3: Valid steps for accepted controlled transitions↩︎

12.4 Theorem 4: Rejection Adequacy↩︎

12.5 Theorem 5: Safeguard Decision↩︎

13 Transition Safeguard Rejection Cases↩︎

For completeness, this appendix gives the formal rendition of every transition-safeguard rejection constructor: for each constructor, the failure predicate carried by its payload, and the implication that the constructor obliges. The formal rendition of reject-soundness (Definition 1) is then \(\mathsf{SafeguardRejectSound}_{\textsf{Spec}} (\mathsf{Safeguard}_{\textsf{Spec}})\triangleq{}\)the conjunction of the five constructor implications below, universally quantified over \(\textit{trace}\), \(w\), \(e\), \(w'\), \(\textit{ctx}\), and the respective payloads. The complete rejection-result family is \[\begin{array}{rcl} \mathsf{Reject}_{\textsf{Spec}} &::=& \mathsf{RejectMissingClaim}(c) \\ &&{}\mid \mathsf{RejectRelianceFailure}(m,c,d) \\ &&{}\mid \mathsf{RejectStaleWitness}(c,e_j) \\ &&{}\mid \mathsf{RejectMissingAuthority}(a) \\ &&{}\mid \mathsf{RejectForbiddenActuation}(r). \end{array}\]

13.1 \(\mathsf{RejectMissingClaim}\)↩︎

\[\begin{align} &\mathsf{Unjustifiability}_{t,\textit{ctx}}(c;\textit{trace},w_t,\textsf{Spec}) \triangleq\\ &\quad |\textit{trace}|=t \wedge \textit{ctx}\in\mathsf{Select}_t(\textit{trace}) \\ &\quad{}\wedge c\in\mathsf{Requires}_{\textsf{Spec}}(\textit{trace},w_t) \wedge \mathsf{Universal}_{+,t}(c;K_{U,t}) \\ &\quad{}\wedge \neg\,\exists m_c\in\textit{Lang}\mathrel{.}\, \mathsf{ReliableClaim}_t( m_c,c; K_{E,\textit{ctx},t}, K_{S,\textit{Src},t}, K_{U,t}, \textit{ctx}) . \end{align}\]

\[\begin{align} &\mathsf{Safeguard}_{\textsf{Spec}} (\textit{trace},w,e,w',\textit{ctx}) =\mathsf{RejectMissingClaim}(c) \\ &\quad \Rightarrow \mathsf{Unjustifiability}_{|\textit{trace}|,\textit{ctx}} (c;\textit{trace},w,\textsf{Spec}). \end{align}\]

13.2 \(\mathsf{RejectRelianceFailure}\)↩︎

\[\begin{align} &\mathsf{DiagnosticOK}_{t,\textit{ctx}}(d;m,c,e,\textit{trace}) \triangleq\\ &\quad \bigl(d=\textsf{Extrapolation} \wedge\mathsf{Extrapolation}_{t}(m,c;\textit{ctx})\bigr) \\ &\quad{}\vee \bigl(d=\textsf{RefutedAssertion} \wedge\mathsf{RefutedAssertion}_{t}(m,c;\textit{ctx})\bigr) \\ &\quad{}\vee \bigl(d=\textsf{UnsupportedAssertion} \wedge\mathsf{UnsupportedAssertion}_{t}(m,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists s\mathrel{.}\, \bigl(d=\textsf{SourceUniversalMismatch}(s) \wedge \mathsf{SourceUniversalMismatch}_{t}(m,s,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists s\mathrel{.}\, \bigl(d=\textsf{SpuriousSupport}(s) \wedge \mathsf{SpuriousSupport}_{t}(m,s,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists s\mathrel{.}\, \bigl(d=\textsf{SourceSupportGap}(s) \wedge \mathsf{SourceSupportGap}_{t}(m,s,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists s\mathrel{.}\, \bigl( d=\textsf{RefutedSourceContradictoryClaim}(s) \bigr. \\ &\qquad{}\bigl. \wedge \mathsf{RefutedSourceContradictoryClaim}_{t} (m,s,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists \mathit{sp},s\mathrel{.}\, \bigl(d=\textsf{StaleSource}(\mathit{sp},s) \wedge \mathsf{StaleSource}_{t} (m,\mathit{sp},s,c;\textit{ctx},\textit{trace})\bigr) \\ &\quad{}\vee \exists s\mathrel{.}\, \bigl(d=\textsf{RefutedSource}(s) \wedge\mathsf{RefutedSource}_{t}(m,s,c;\textit{ctx})\bigr) \\ &\quad{}\vee \exists h\mathrel{.}\, \bigl(d=\textsf{AddedHypothesis}(h) \wedge \mathsf{AddedHypothesis}_{t}(h,c;m,\textit{ctx})\bigr) \\ &\quad{}\vee \exists s,\textit{ctx}_{t+1}\mathrel{.}\, \bigl( d=\textsf{UnsupportedUse}(s) \\ &\qquad{}\wedge \textit{ctx}_{t+1}\in\mathsf{Select}_{t+1}(\textit{trace}\cdot e) \\ &\qquad{}\wedge \mathsf{UnsupportedUse}_{t+1} \\ &\qquad{} (e,m,s,c;\textit{trace},\textit{ctx},\textit{ctx}_{t+1}) \bigr). \end{align}\]

\[\begin{align} &\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx}) =\mathsf{RejectRelianceFailure}(m,c,d) \\ &\quad\Rightarrow m=e.\mathsf{message} \wedge \mathsf{RelianceFailure}_{|\textit{trace}|,\textit{ctx}}(m,c) \\ &\qquad{}\wedge \mathsf{DiagnosticOK}_{|\textit{trace}|,\textit{ctx}} (d;m,c,e,\textit{trace}). \end{align}\]

13.3 \(\mathsf{RejectStaleWitness}\)↩︎

\[\begin{align} &\mathsf{TraceWitness}_{\textsf{Spec}}(e_i,e,c;\textit{trace}) \triangleq\\ &\quad e_i\in\textit{trace} \wedge \mathsf{interp}_{\textsf{Spec}}(e_i)\downarrow \wedge c\in\mathsf{interp}_{\textsf{Spec}}(e_i) \\ &\quad{}\wedge \Bigl( e_i\in e.\mathsf{witness} \\ &\qquad{}\vee \exists I\subseteq[1,|\textit{trace}|]\mathrel{.}\, I\in e.\mathsf{witness} \wedge \exists k\in I\mathrel{.}\,e_i=\textit{trace}[k] \\ &\qquad{}\vee \exists t_0,\mathit{sp},s\mathrel{.}\, \mathit{sp}\in e.\mathsf{witness} \wedge \mathsf{SourceWitness}_{t_0}(\mathit{sp},s;\textit{trace}) \wedge \mathsf{ExtractedFrom}_{t_0}(s,\mathit{sp};e_i) \Bigr). \end{align}\]

\[\begin{align} &\mathsf{StaleWitness}_{\textsf{Spec}} (\textit{trace},w;e,c,e_j) \triangleq\\ &\quad \mathsf{worldmap}_{\textsf{Spec}}(w)\downarrow \\ &\quad{}\wedge \bigl(\forall e_k\in\textit{trace}\mathrel{.}\, \mathsf{interp}_{\textsf{Spec}}(e_k)\downarrow\bigr) \\ &\quad{}\wedge \mathsf{interp}_{\textsf{Spec}}(e)\downarrow \\ &\quad{}\wedge \exists i,j\in[1,|\textit{trace}|]\mathrel{.}\, i<j \wedge \textit{trace}[j]=e_j \\ &\quad{}\wedge \mathsf{TraceWitness}_{\textsf{Spec}} (\textit{trace}[i],e,c;\textit{trace}) \\ &\quad{}\wedge a witness-invalidation clause of \textsf{Spec}classifies e_j \\ &\qquad as invalidating \textit{trace}[i] for cat (\textit{trace},w) \\ &\quad{}\wedge \neg\,\exists \ell\in[j+1,|\textit{trace}|]\mathrel{.}\, \mathsf{TraceWitness}_{\textsf{Spec}} (\textit{trace}[\ell],e,c;\textit{trace}) \\ &\qquad{}\wedge \(\textsf{Spec}\) classifies \textit{trace}[\ell]as a current witness for c. \end{align}\]

\[\begin{align} &(\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx}) =\mathsf{RejectStaleWitness}(c,e_j)) \\ &\quad\Rightarrow \mathsf{StaleWitness}_{\textsf{Spec}}(\textit{trace},w;e,c,e_j). \end{align}\]

13.4 \(\mathsf{RejectMissingAuthority}\)↩︎

\[\begin{align} &\mathsf{MissingAuthority}_{\textsf{Spec}}(\textit{trace},w;e,a) \triangleq\\ &\quad \mathsf{worldmap}_{\textsf{Spec}}(w)\downarrow \\ &\quad{}\wedge \bigl(\forall e_j\in\textit{trace}\mathrel{.}\, \mathsf{interp}_{\textsf{Spec}}(e_j)\downarrow\bigr) \\ &\quad{}\wedge \mathsf{interp}_{\textsf{Spec}}(e)\downarrow \\ &\quad{}\wedge \textsf{Spec}\;requires prior authority afor e at (\textit{trace},w) \\ &\quad{}\wedge \neg\,\exists j\in[1,|\textit{trace}|]\mathrel{.}\, \bigl( \textit{trace}[j]=a \vee a\in\textit{trace}[j].\mathsf{authority} \vee a\in\mathsf{interp}_{\textsf{Spec}}(\textit{trace}[j]) \bigr). \end{align}\]

\[\begin{align} &\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx}) =\mathsf{RejectMissingAuthority}(a) \\ &\quad\Rightarrow \mathsf{MissingAuthority}_{\textsf{Spec}}(\textit{trace},w;e,a). \end{align}\]

13.5 \(\mathsf{RejectForbiddenActuation}\)↩︎

\[\begin{align} &\mathsf{ForbiddenActuation}_{\textsf{Spec}}(\textit{trace},w;e,w',r) \triangleq\\ &\quad \mathsf{worldmap}_{\textsf{Spec}}(w)\downarrow \\ &\quad{}\wedge \bigl(\forall e_j\in\textit{trace}\mathrel{.}\, \mathsf{interp}_{\textsf{Spec}}(e_j)\downarrow\bigr) \\ &\quad{}\wedge \mathsf{interp}_{\textsf{Spec}}(e)\downarrow \wedge r=e.\mathsf{actuation} \wedge r\neq m_{\bot} \wedge \mathsf{actuation}(w,r)=w' \\ &\quad{}\wedge no actuation clause of \textsf{Spec} allows the tuple\\ &\qquad (\textit{trace},w,e.\mathsf{name},e.\mathsf{kind},e.\mathsf{resource}, e.\mathsf{authority},e.\mathsf{witness},e.\mathsf{actuation},r). \end{align}\]

\[\begin{align} &(\mathsf{Safeguard}_{\textsf{Spec}}(\textit{trace},w,e,w',\textit{ctx}) =\mathsf{RejectForbiddenActuation}(r)) \\ &\quad\Rightarrow \mathsf{ForbiddenActuation}_{\textsf{Spec}}(\textit{trace},w;e,w',r). \end{align}\]

14 Example implementation of a specification written in cat [21]↩︎

References↩︎