Ceci n’est pas une pipe: AI systems as semantic abstractions JADE ALGLAVE and PATRICK COUSOT An AI system’s output is not the fact or world state it appears to describe, but rather an engineered representation. We propose a semantic framework to describe AI systems, to be able to examine the correctness of such representations. To do so, we distinguish what is justified by accepted domain knowledge, what reference sources say, and what the system can currently use. This allows us to give precise definitions to common failures: extrapolation, refuted or unsupported assertion, sources versus knowledge mismatch, stale or refuted source, added hypotheses, unsupported use…We hope our framework gives a useful vocabulary for specifying and checking AI systems whose outputs, citations, tool calls, and world-changing actions must be justified by reliable claims and explicit authority rather than apparent fluency.
arXiv:2607.09489v1 [cs.AI] 10 Jul 2026
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 [77]. 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 [14, 15, 49, 103]. 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. We use this example throughout: Oma needs to renew her passport using an AI-aided application. The system may need to inspect her old passport, check current guidance on what pictures are acceptable, take or evaluate a picture, fill in a form, handle an interruption such as the doorbell, save progress, check that everything is ready for submission, and ask Oma for confirmation to submit. The Knowledge Bases need to contain official passport requirements; the Prompts may be Oma’s requests and corrections; Compute Components may be an LLM procured by the government, and Oma’s phone camera; the Orchestrator may be a software stack around the LLM that decides whether to retrieve, ask, check, save, or mark the application ready, and Actuation may consist of a local PDF export.
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 Contact Information: Jade Alglave, [email protected],[email protected]; Patrick Cousot, [email protected].
2
Alglave & Cousot
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. Consider Oma completing the form to renew her passport. The system records a trace of events: route selection (e.g. UK or FR), passport observation, form population, picture and form checks, application readiness check, Oma’s confirmation, permission, and submission. The readiness event is not itself proof that the application is ready. Its message must be interpreted, checked against sources, and supported by the current trace before the system may rely on it. The later definitions formalise this path and the failure modes that arise when necessary observations, witnesses, authority, or freshness conditions are missing.
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. A prototype, which can be made available upon request, exemplifies the concepts introduced in this paper: the app lets a user, or an agent on behalf of that user, fill in a passport renewal form, take a picture of themselves, scan their existing passport page, and save the current draft when the doorbell rings…
2 Knowledge Base This section defines the machinery used for knowledge bases. A knowledge base 𝐾 = ⟨𝐷, 𝐹 , 𝑅, 𝑡⟩ at time 𝑡 ∈ ℕ features a domain 𝐷 (a collection of objects, e.g. sets, types…), facts 𝐹 ∈ ℘(𝐷), and a rule system 𝑅 over domain 𝐷 . A rule 𝑃𝑐 has premises 𝑃 ∈ ℘(𝐷) and a conclusion 𝑐 ∈ 𝐷 . If 𝑃 = ∅ 𝑃
the rule is called an axiom. The rule system 𝑅 ≜ { 𝑐 𝑖 | 𝑖 ∈ 𝜌} over 𝐷 is a possibly infinite family of 𝑖 rules indexed by a set 𝜌 . Standard [88], intuitionistic [96], and modal [17] logics can be formalised using such Hilbertstyle proof systems [46]. Although introduced for logics [46], such rule-based definitions can define any subset of a domain 𝐷 , hence encompass grammars [22], databases [89], knowledge graphs [48], and deductive systems [1], and may also contain contradictory facts. For Oma: One rule may say that if a candidate passport picture respects current official guidance, then the picture respects the overall rules for the application.
Next we need to say what consequences may be justified by 𝑅 from the facts in 𝐹 : • Proofs. A theorem has hypotheses 𝐻 ∈ ℘(𝐷), a conclusion 𝑐 ∈ 𝐷 , and a proof. If every premise 𝑃 set 𝑃𝑖 of every rule 𝑐 𝑖 in 𝑅 is finite, the proof is a sequence 𝑝1 𝑝2 … 𝑝𝑛 s.t. each 𝑝𝑖 is a hypothesis 𝑖 in 𝐻 , a fact in 𝐹 , or the conclusion of a rule s.t. all elements of 𝑃𝑖 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 [76].
Ceci n’est pas une pipe
3
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 𝑋 is the set of facts already reached, then Infer𝑅 (𝐹 )(𝑋 ) ≜ 𝐹 ∪ 𝑋 ∪ {𝑐𝑖 ∣ 𝑖 ∈ 𝜌 ∧ 𝑃𝑖 ⊆ 𝐹 ∪ 𝑋 } adds facts 𝐹 to 𝑋 , and every conclusion whose premises are available from 𝐹 ∪ 𝑋 . For Oma: A proof step may add “the draft may be marked ready” only after the required source, picturecheck, CheckForm, and ConfirmDraft facts are already reached.
• Chaining. Forward chaining repeatedly applies Infer𝑅 (𝐹 ) to justify consequences from the facts already available. Backward chaining replaces a set of goals 𝐺 ⊆ 𝐷 by the premises 𝑃 of a rule 𝑅 that would prove it: 𝐺 ⇝𝑅 (𝐺 ∖ {𝑐}) ∪ 𝑃 when 𝑃𝑐 ∈ 𝑅 and 𝑐 ∈ 𝐺 . 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 𝐵 ⊆ 𝐷 , let Infer∗𝑅 (𝐵) ≜ lfp⊆ (𝜆𝑋 .Infer𝑅 (𝐵)(𝑋 )), where lfp⊆ is the least fixed point in order ⊆, which exists by Tarski’s theorem [93] since 𝑋 ↦ Infer𝑅 (𝐵)(𝑋 ) is ⊆-monotone ∗ in 𝑋 . A conclusion 𝑐 is justified from facts 𝐹 and hypotheses 𝐻 when 𝑐 ∈ Infer𝑅 (𝐹 ∪ 𝐻 ). • Paraconsistent justification. Given 𝐾 = ⟨𝐷, 𝐹 , 𝑅, 𝑡⟩, we say that 𝐾 justifies a claim 𝑐 when 𝐾 ⊢ 𝑐 ≜ 𝑐 ∈ Infer∗𝑅 (𝐹 ), and that 𝐾 does not justify 𝑐 when 𝐾 ⊬ 𝑐 ≜ 𝑐 ∉ Infer∗𝑅 (𝐹 ). A knowledge base may justify a fact, its negation, both, or neither. Thus 𝐾 ⊢ 𝑐 may not mean that 𝑐 is reliable. Absence of justification is not negation: 𝐾 ⊬ 𝑐 does not imply 𝐾 ⊢ ¬𝑐 . We distinguish four base statuses: 𝐾 ⊢+ 𝑐 ≜ 𝐾 ⊢ 𝑐 ∧ 𝐾 ⊬ ¬𝑐 , 𝐾 ⊢− 𝑐 ≜ 𝐾 ⊢ ¬𝑐 ∧ 𝐾 ⊬ 𝑐 , 𝐾 ⊢± 𝑐 ≜ 𝐾 ⊢ 𝑐 ∧ 𝐾 ⊢ ¬𝑐 , 𝐾 ⊢? 𝑐 ≜ 𝐾 ⊬ 𝑐 ∧ 𝐾 ⊬ ¬𝑐 . We also use the derived shorthand 𝐾 ⊢⊕ 𝑐 ≜ 𝐾 ⊢+ 𝑐 ⊕ 𝐾 ⊢− 𝑐 for one-sided justification. When the time index is useful, we write 𝐾 ⊢×𝑡 𝑐 for the corresponding base status at time 𝑡 , with × ∈ {+, −, ±, ?}, and use 𝐾 ⊢⊕ 𝑡 𝑐 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 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 𝑚∗ are communication-language messages: elements of Lang. They are not world objects and not semantic facts. For Oma: In the app, 𝑚ready ≜ result = passed is recorded in event 𝑒ready in the trace, which comes from clicking the button Check Everything Ready for Submission to run checks on the current draft.
3.2
Semantics of the Communication Language
Now we need to determine the meaning of messages. We write denotationLang ∶ Lang ⇀ SourceItems for the denotation of messages, where SourceItems is the set of source items, which we discuss more amply in Section 4.2. Because denotation may not be defined, we write: DenotesLang (𝑚, 𝑠) ≜ 𝑚 ∈ Lang ∧ 𝑠 ∈ SourceItems ∧ denotationLang (𝑚) = 𝑠 is defined.
4
Alglave & Cousot
For Oma: Consider the application readiness check message 𝑚ready . Its denotationLang (𝑚ready ) = 𝑠readinessChecksPassed records the fact that according to the app design, the message denotes a passed readiness check. But if Oma edited a required field or replaced the picture after the check, the message still has the same denotation, but the trace no longer supports using it for submission readiness.
Thus denotation alone does not make a source item usable. For Oma: In the prototype, denotationLang is a schema: a communication message 𝑚 ∈ Lang carries explicit fields, and denotationLang (𝑚) = 𝑠 is defined only when exactly one row matches. Thus for the 𝑚ready message above, the app records 𝑚 = {messageType = CheckResultMessage, actionKind = checkReady, resourceKind = currentDraft, payloadKind = readinessResult, result = passed}, which matches exactly one row: denotationLang (𝑚) = 𝑠readinessChecksPassed . If no row matches, denotation is undefined; if more than one row matches, the orchestrator records failed denotation rather than choosing silently. The action, resource, result kind, and any state on which denotation depends must be explicit in 𝑚 or in the trace; hidden browser state, model state, or guessing is not allowed to decide the denotation.
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 𝑊 ; at time 𝑡 , the current world state is 𝑤𝑡 ; • the history 𝑤1 , … , 𝑤𝑡 of world states at time 𝑡 ; • what the AI system can observe, via observation; • what the AI system can change, via 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 observation ∈ Services ×𝑊 → Lang for the service-relative observation interface, possibly lossy, permission-limited, and time-dependent. For Oma: The interface observation covers things such as reading a prompt, observing an uploaded passport page, capturing or importing a picture, reading the current draft form, inspecting checker results, retrieving official guidance, and observing an interruption or later form edit.
The AI system may also modify part of the world. We write actuation ∈ (𝑊 × Lang) → 𝑊 for the actuation interface. Thus actuation(𝑤, 𝑚) should be effectless when the message 𝑚 ∈ Lang is not an allowed update from world state 𝑤 . For Oma: The interface actuation covers things such as filling a field, saving a draft, taking or importing a picture, exporting a PDF, and recording readiness.
3.4
Traces
The world state may change outside the system’s control. A user, a tool, an external service, may move 𝑤𝑡 to 𝑤𝑡+1 . The relation between the two states may be unknown to the system. For Oma: The app may populate fields in the form from the old passport. At the same time, Oma may edit a field, replace the uploaded picture, reset the form… We must therefore record observations and invalidations of the current form state before the system may rely on a prior readiness check.
Thus we keep separate records: the history 𝑤1 … 𝑤𝑡 , 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 𝑒 = ⟨name, comment, actor, message, kind, resource, observation, actuation, authority, witness⟩ ∈ Ev. We write e.g. 𝑒.message for the message field of the event 𝑒 .
Ceci n’est pas une pipe
5
For Oma: Pressing the UI button “Check Everything Ready for Submission” produces an event:
𝑒ready = {
name = CheckReady, actor = AppAgent,
comment = Everything ready for submission checked, message = 𝑚ready …}
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. For Oma: A picture-check event might record 𝑒.witness = {spgov-pic-guidance , 𝑟pic-check }, with spgov-pic-guidance a source pointer and 𝑟pic-check a checker result.
A trace is a finite event sequence trace = 𝑒1 … 𝑒𝑛 ∈ Trace ≜ Ev∗ . For 0 ≤ 𝑘 ≤ 𝑛, let trace≤𝑘 ≜ 𝑒1 … 𝑒𝑘 , with trace≤0 = 𝜖 , be the prefix of the trace available after 𝑘 events. Often, we identify the time 𝑡 with the current number of events recorded in the trace. For Oma: A trace for the scenario where Oma successfully submits her UK passport renewal application by scanning her old passport to populate the form is as follows: ⟨UKRenewalPicked, ObservePassport, PopulateFields, CheckPicture, CheckForm, ConfirmDraft, CheckEverything ReadyForSubmission, SubmissionPermit, Submit⟩. The events’ names are shorthands for the events, e.g. CheckReady for the event 𝑒ready above.
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 𝑤𝑡 to 𝑤𝑡+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. For Oma: The model of the world rules out states that cannot be true of the passport renewal application: the same current draft cannot both contain and not contain a required field value; a readiness check cannot be for a picture different from the current uploaded picture; and a filled PDF cannot faithfully represent a form state that has since been reset or edited.
3.5
Context
Calls to AI systems are often talked about in terms of their context. We let ctx ∈ Lang∗ range over messages available to the system at some point in the trace. More specifically, ctx is an applicationspecific abstraction of trace: ctx𝑡 ∈ Select𝑡 (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.
6
Alglave & Cousot
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 Src𝑡 constitute the Information State of an AI system: • Section 4.1 defines the universal knowledge base 𝐾𝑈 ,𝑡 : accepted domain knowledge. • The reference sources Src𝑡 consist of source pointers or resources: pages, files, tool results…. • Section 4.2 defines the source-derived knowledge base 𝐾𝑆,Src,𝑡 , computed from facts extracted from Src𝑡 : it may be wrong, incomplete, stale, or inconsistent. • Section 4.3 defines the AI system’s effective knowledge base 𝐾𝐸,ctx,𝑡 : what the system can use from the current context ctx, including mistaken, stale, compressed material. 𝐾𝐸,ctx,𝑡 is not what is in context; rather the context is an input to 𝐾𝐸,ctx,𝑡 . For Oma: ctx may contain messages describing the official guidance, picture-check result, and confirmation record, while Src contains e.g. passport-picture or form-validity rules.
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. 𝑈̄ . 4.1
Universal Knowledge Base The domain of the universal knowledge base 𝐾𝑈 ,𝑡 is a universe 𝑈̄ such that: • The elements of the universe 𝑈̄ encode facts, objects, and reasoning steps: token sequences, pictures, videos, recordings, theorems, proofs, laws, programs, events, permissions… One can read 𝑈̄ as many-sorted, or as a single encoded universe with tags for the different sorts of objects; • Without loss of generality, 𝑈̄ 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… For Oma: Elements of 𝑈̄ include picture facts, form field values, source claims, confirmation events, readiness facts, and claims about whether a given app action is allowed, as well as definition of the data appearing on a passport, database where this data is recorded, how to access that database, …
The Universal Knowledge Base w.r.t. a universe 𝑈̄ and a rule system 𝑅𝑡̄ over 𝑈̄ at a time 𝑡 consists of selected hypotheses 𝐻̄𝑡 ⊆ 𝑈̄ together with the rule system 𝑅𝑡̄ : 𝐾𝑈 ,𝑡 ≜ ⟨𝑈̄ , 𝐻̄𝑡 , 𝑅𝑡̄ , 𝑡⟩. For Oma: 𝐻̄𝑡 may include current domain facts such as the applicable passport renewal rules, the meaning of form fields, and the validity conditions for a submission, while 𝑅𝑡̄ contains rules for deriving claims such as whether a draft is complete, whether a picture satisfies the applicable requirements, and whether an application may be submitted.
4.2
Source-derived Knowledge Base
We assume that an AI system cannot always range over everything in 𝑈̄ . Instead, a system has a scope Scope ⊆ 𝑈̄ , 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 [26]. 4.2.1
Ignorance and Forgetfulness Abstractions.
Ignorance. The ignore abstraction ignores what falls outside this scope: ignore(𝑋 ) = 𝑋 ∩ Scope for 𝑋 ∈ ℘(𝑈̄ ). The same restriction applies to rules: ignore(𝑅𝑡̄ ) ≜ { 𝑃𝑐 ∈ 𝑅𝑡̄ | 𝑃 ⊆ Scope ∧𝑐 ∈ Scope }.
Ceci n’est pas une pipe
7
Thus ignore(𝑅𝑡̄ ) is sound but incomplete relative to 𝑅𝑡̄ : any proof in Scope is also a proof in 𝑈̄ , but some proofs in 𝑈̄ disappear because some facts, premises, or rules are outside the system’s scope. For Oma: Ignorance is exemplified by a system that does not encode every possible law, or institutional process that might not matter to passport renewal.
Forgetfulness. The forget abstraction formalises loss of distinctions inside the system’s scope. We write ≡𝑓 for the application-specific equivalence relation on Scope that identifies semantic objects the AI system’s representation cannot distinguish, and [𝑥]≡𝑓 for the equivalence class represented by 𝑥 . On sets, forget(𝑋 ) = {[𝑥]≡𝑓 ∣ 𝑥 ∈ 𝑋 }. On rules, forget(𝑅) ≜ {
{ [𝑝]≡𝑓 | 𝑝∈𝑃 }
abstract rules can no longer distinguish equivalent pieces of information.
[𝑐]≡𝑓
| 𝑃𝑐 ∈ 𝑅} , so
For Oma: Forgetting is exemplified by a system compressing a passport image. For Oma’s passport application, a full-resolution passport image, an OCR record, and a statement such as “old passport number was 𝑋 ” may be distinct in 𝑈̄ , but the app may represent all of them by the same object.
4.2.2 Source-derived Knowledge Base and its semantics. The reference sources Src𝑡 are not themselves facts: source-item facts 𝐹𝑆,Src,𝑡 ⊆ SourceItems (with SourceItems ≜ Scope/≡𝑓 ) are extracted from Src𝑡 . The corresponding rule system is 𝑅𝑆,𝑡 ≜ forget (ignore (𝑅𝑡̄ )). Thus the source-derived knowledge base is 𝐾𝑆,Src,𝑡 ≜ ⟨SourceItems, 𝐹𝑆,Src,𝑡 , 𝑅𝑆,𝑡 , 𝑡⟩. Its inference operator is Infer𝑅𝑆,𝑡 , and denotation𝑈 ∈ SourceItems → ℘(𝑈̄ ) defines the semantics of the source-derived knowledge base 𝐾𝑆,Src,𝑡 w.r.t. the universal knowledge base 𝐾𝑈 ,𝑡 . For Oma: A picture with infinite precision might be in 𝐾𝑈 ,𝑡 , and its grainy processed sibling in 𝐾𝑆,Src,𝑡 .
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 ctx ∈ Select𝑡 (trace), gathered e.g. from interactions with the world recorded in trace. For Oma: 𝑊 contains Oma, the phone, the old passport, the camera view, the doorbell, the draft form, the saved picture, and the government site. The interface observation covers things such as camera images, form text, retrieval results, and interruption notifications.
4.3.1 Effective knowledge base and its Semantics. We let 𝐾𝐸,ctx,𝑡 be the effective knowledge of an AI system: 𝐾𝐸,ctx,𝑡 ≜ ⟨Lang, 𝐹𝐸,ctx,𝑡 , 𝑅𝐸,ctx,𝑡 , 𝑡⟩. Recall that the context ctx is gathered by the orchestrator by interaction with users or external agents. The facts 𝐹𝐸,ctx,𝑡 ≜ {𝑚 ∣ 𝑚 ∈ ctx } are directly extracted from this context ctx. 4.3.2 Context is not Effective Knowledge. Recall that context ctx is an application-specific abstraction of the trace (which may include loss or extrapolation). Thus ctx lives in Lang: it is not itself a knowledge base, nor is it a subset of the effective knowledge 𝐾𝐸,ctx,𝑡 . 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 𝐾𝐸,ctx,𝑡 . For Oma: If the context says “Oma has not confirmed readiness,” the orchestrator may justify a source item 𝑠readinessNotAllowed even if that exact symbol does not occur in the context.
8
Alglave & Cousot
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 applicationspecific abstraction (including potential loss and extrapolation) available to the AI system for building 𝐾𝐸,ctx,𝑡 . Thus 𝐾𝐸,ctx,𝑡 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. For Oma: “Oma confirmed the current draft and no later edit invalidated it” is a trace property, not merely a context-message property.
4.4 Knowledge Base Statuses Justification of a claim by a knowledge base is only potential by default. Writing +, −, ±, and ? for the base justification statuses of Section 2, and ⊕ for the derived one-sided shorthand, we record what is justified by the Effective knowledge base 𝐾𝐸,ctx,𝑡 , the Source-derived knowledge base 𝐾𝑆,Src,𝑡 , and the Universal knowledge base 𝐾𝑈 ,𝑡 . To keep the selected knowledge base explicit, each status predicate takes it as a parameter (× ∈ {+, −, ±, ?}): Effective×,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx,𝑡 ) ≜ DenotesLang (𝑚, 𝑠) ∧ 𝐾𝐸,ctx,𝑡 ⊢×𝑡 𝑚 Source×,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ≜ 𝑠 ∈ SourceItems ∧ 𝐾𝑆,Src,𝑡 ⊢×𝑡 𝑠 Universal×,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ≜ 𝑐 ∈ 𝑈̄ ∧ 𝐾𝑈 ,𝑡 ⊢×𝑡 𝑐
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 𝐾𝑈 ,𝑡 is assumed given: in general 𝐾𝑈 ,𝑡 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 𝐾𝑈 ,𝑡 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, 𝐾𝑈 ,𝑡 may be precise enough to state obligations, but checking those obligations may still be undecidable, expensive, approximate, or domain-specific. For Oma: 𝐾𝑈 ,𝑡 is the current normative passport-renewal process: which UK or French renewal route applies, what the form fields mean, what picture conditions are required, and what authority is needed before the app may mark a draft ready or submit it. Official pages are Src𝑡 ; parsed guidance and OCR/MRZ output are 𝐹𝑆,Src,𝑡 ; their source-derived closure is 𝐾𝑆,Src,𝑡 .
Source evidence has a different status. A source pointer sp ∈ Src𝑡 , recorded in a trace witness field, can witness that the system retrieved or cited a source. It does not by itself show that the
Ceci n’est pas une pipe
9
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 𝐾𝑆,Src,𝑡 from Src𝑡 . Finally, even if a source item is present in the system’s effective knowledge 𝐾𝐸,ctx,𝑡 , 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 𝐾𝑆,Src,𝑡 , true in 𝐾𝑈 ,𝑡 , or authorised by the user. These limitations are not a reason to abandon the formalisation. They mark where the obligations sit. If 𝐾𝑈 ,𝑡 is unclear, an application written over 𝐾𝑈 ,𝑡 should explicitly disclaim that. If source material is stale or unofficial, the issue is in Src𝑡 . If extraction or interpretation is wrong, the issue is in 𝐾𝑆,Src,𝑡 . If the system relies on a compressed, inferred, or approximate item, the issue is in 𝐾𝐸,ctx,𝑡 . 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 𝐾𝐸,ctx,𝑡 over Lang records what the system is justified to use at time 𝑡 for the context ctx. For a message 𝑚 ∈ Lang, its being justified by the Effective knowledge base does not mean it is true. For Oma: 𝑠readinessChecksPassed being justified by 𝐾𝐸,ctx,𝑡 just means that this readiness-check result is considered usable for the current draft. It should not be justified by 𝐾𝐸,ctx,𝑡 if Oma edited a required field, replaced the picture, or if a later trace event otherwise invalidated the draft state.
For a message 𝑚 justified by 𝐾𝐸,ctx,𝑡 , the map CandidateClaims ∈ Lang → ℘(𝑈̄ ) records which claims 𝑚 might be standing for. We let 𝑠𝑚 be the unique source item 𝑠 s.t. DenotesLang (𝑚, 𝑠). Then: denotation𝑈 (𝑠𝑚 ), if 𝑠𝑚 is defined, CandidateClaims(𝑚) ≜ { ∅, otherwise. When 𝑠𝑚 is defined, the claims in CandidateClaims(𝑚) are the semantic claims associated with the source item 𝑠𝑚 . This may be a set with several elements because of the forgetfulness abstraction. If 𝑠𝑚 is undefined, 𝑚 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. For Oma: A priori CandidateClaims(𝑚ready ) might mean that the readiness checker returned normally, or that all required form fields were nonempty, or that the picture check and form check both passed for the current draft, or that the current draft satisfies the local readiness conditions for submission.
10
Alglave & Cousot
The definition of 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 𝑚, CandidateClaims(𝑚) needs to say which underlying claims 𝑚 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. For Oma: In the app, the denotation schema maps message 𝑚ready to a source item 𝑠readinessChecksPassed . We then look up the row for that source item 𝑠readinessChecksPassed ↦ {ReadinessChecksPassed(currentDraft)}. This only says that the app’s local readiness check passed for the current draft. Since the row does not contain, e.g. UserPermissionGiven(Submission), the orchestrator must not infer that permission from the readiness result. Thus permission can only come from an explicit separate message from Oma.
5.2
Asserted Claims
The map 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 Asserts𝐸,ctx,𝑡 (𝑚, 𝑐), s.t. Asserts𝐸,ctx,𝑡 (𝑚, 𝑐) ⇒ 𝑚 ∈ Lang ∧ 𝑐 ∈ CandidateClaims(𝑚). The asserted claims of 𝑚 are then: AssertedClaims𝐸,ctx,𝑡 (𝑚) ≜ { 𝑐 ∈ CandidateClaims(𝑚) ∣ 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚 ∧ Asserts𝐸,ctx,𝑡 (𝑚, 𝑐) }. Thus CandidateClaims(𝑚) records possible meanings, while AssertedClaims𝐸,ctx,𝑡 (𝑚) records the candidate claims that the system actually asks the user, caller, or downstream component to rely on. The positive effective-knowledge condition 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚 excludes messages that are refuted, contradictory, or unjustified in 𝐾𝐸,ctx,𝑡 . 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 SourceSupport𝑡 ⊆ SourceItems × 𝑈̄ and read SourceSupport𝑡 (𝑠, 𝑐) as: at time 𝑡 , source item 𝑠 supports the semantic claim 𝑐 . Source support is application-defined, but it must respect denotation: SourceSupport𝑡 (𝑠, 𝑐) ⇒ 𝑠 ∈ SourceItems ∧ 𝑐 ∈ denotation𝑈 (𝑠). For a message 𝑚 justified by 𝐾𝐸,ctx,𝑡 , i.e. 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚, the corresponding candidate claims are CandidateClaims(𝑚). This does not mean that those claims are justified by the source-derived knowledge base 𝐾𝑆,Src,𝑡 , let alone the universal knowledge base 𝐾𝑈 ,𝑡 . The predicate SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ) ≜ 𝑚 ∈ Lang ∧ 𝑐 ∈ CandidateClaims(𝑚)
∧ ∃𝑠 ∈ SourceItems . DenotesLang (𝑚, 𝑠) ∧ Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ SourceSupport𝑡 (𝑠, 𝑐). says that 𝑐 is definitely justified by the Universal Knowledge base, and that it is supported by a source item 𝑠 definitely justified by the Source-derived Knowledge base. For Oma: The claim that the draft satisfies 𝑐readinessChecksPassed = ReadinessChecksPassed(currentDraft) is supported only if the relevant passport rules are available as source-derived knowledge, the formcompleteness check and picture check apply to the current draft, Oma confirmed that draft.
5.4
Reliable Claims
SupportedClaim checks whether the candidate claim 𝑐 is justified by the universal and sourcederived knowledge bases. Reliability also requires that the message 𝑚 through which the system uses 𝑐 is justified by current effective knowledge and that 𝑐 is one of the asserted claims of 𝑚. With
Ceci n’est pas une pipe
11
ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ≜ 𝑚 ∈ Lang ∧ 𝑐 ∈ AssertedClaims𝐸,ctx,𝑡 (𝑚), the full reliability predicate is ReliableClaim𝑡 (𝑚, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚 ∧ SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ). Thus 𝐾𝐸,ctx,𝑡 appears in the judgment for what the system may use, while the support check is grounded in the source-derived and universal knowledge bases. For Oma: Pressing a button confirming readiness records event 𝑒ready ∈ trace with message 𝑚ready . Then:
𝑚ready denotationLang
𝑠readinessChecksPassed
𝑐readinessChecksPassed ∈CandidateClaims(𝑚ready ) SourceSupport𝑡 (𝑠readinessChecksPassed ,𝑐readinessChecksPassed ) Source+,𝑡 (𝑠readinessChecksPassed ;𝐾𝑆,Src,𝑡 )
𝑐readinessChecksPassed
Universal+,𝑡 (𝑐readinessChecksPassed ;𝐾𝑈 ,𝑡 )
SupportedClaim𝑡 (𝑚ready , 𝑐readinessChecksPassed ; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ) 𝑐readinessChecksPassed ∈AssertedClaims𝐸,ctx,𝑡 (𝑚ready ) 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚ready
ReliableClaim𝑡 (𝑚ready , 𝑐readinessChecksPassed ; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx) A string “result = passed” in the context window is not enough: context presence is input-level, 𝐾𝐸,ctx,𝑡 is effective-knowledge justification, and only ReliableClaim𝑡 justifies use.
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: RelianceFailure𝑡,ctx (𝑚, 𝑐) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐)∧¬ ReliableClaim𝑡 (𝑚, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , 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. For Oma: An unsupported assertion may be a claim that the passport picture rule allows something that the current official rule does not allow. An added hypothesis may be the system silently assuming that the old passport is still valid. A source-derived vs universal mismatch is an outdated web page that conflicts with the current official guidance. A useful output is therefore not only the generated answer, but also, e.g., the source pointer to the official rule against which the claim is checked.
Given a message 𝑚 ∈ Lang whose denotation is defined, let 𝑠 = denotationLang (𝑚) ∈ SourceItems. The claims to classify are AssertedClaims𝐸,ctx,𝑡 (𝑚), 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 Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) also holds, 𝐾𝑈 ,𝑡 refutes the claim: RefutedAssertion𝑡 (𝑚, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ).
12
Alglave & Cousot
• Unsupported Assertion. If Universal?,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) holds, the use is an unsupported assertion: UnsupportedAssertion𝑡 (𝑚, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ ∃𝑠 ∈ SourceItems . DenotesLang (𝑚, 𝑠)
∧ Effective⊕,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx,𝑡 ) ∧ Universal?,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ ¬ SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ). The unsupported claim may originate with Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ), or it may be invented by the AI system when Source±,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) or Source?,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) 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 𝑐 through a message 𝑚 when the corresponding source item 𝑠 is not one-sided and the universal status of 𝑐 is contradictory: Extrapolation𝑡 (𝑚, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ ∃𝑠 ∈ SourceItems . DenotesLang (𝑚, 𝑠)
∧ Effective⊕,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx,𝑡 ) ∧ ¬ Source⊕,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ). • Source-Derived vs Universal Mismatch. If a message 𝑚 denotes a source item 𝑠 justified by 𝐾𝑆,Src,𝑡 , and an asserted claim 𝑐 ∈ denotation𝑈 (𝑠) is contradictory in 𝐾𝑈 ,𝑡 , there is a mismatch: SourceUniversalMismatch𝑡 (𝑚, 𝑠, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠)
∧ 𝑐 ∈ denotation𝑈 (𝑠) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ). • Spurious Support. SpuriousSupport𝑡 (𝑚, 𝑠, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠) ∧ Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 )
∧ ¬Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) 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. SourceSupportGap𝑡 (𝑚, 𝑠, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠)
∧ Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ ¬SourceSupport𝑡 (𝑠, 𝑐)
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 𝑐 contradictory, the source item 𝑠 is definitely refuted: RefutedSourceContradictoryClaim𝑡 (𝑚, 𝑠, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠)
∧ Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ Source−,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 )
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. Theorem 1 (Exhaustiveness). If ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) and DenotesLang (𝑚, 𝑠), then it is the case that RelianceFailure𝑡,ctx (𝑚, 𝑐) holds if and only if at least one of the following holds: RefutedAssertion𝑡 (𝑚, 𝑐; ctx), Extrapolation𝑡 (𝑚, 𝑐; ctx),
UnsupportedAssertion𝑡 (𝑚, 𝑐; ctx),
SourceUniversalMismatch𝑡 (𝑚, 𝑠, 𝑐; ctx),
SpuriousSupport𝑡 (𝑚, 𝑠, 𝑐; ctx),
SourceSupportGap𝑡 (𝑚, 𝑠, 𝑐; ctx),
RefutedSourceContradictoryClaim𝑡 (𝑚, 𝑠, 𝑐; ctx).
Ceci n’est pas une pipe
6.2
13
History failure diagnostics
• Stale Source. This is a temporal instance of SourceUniversalMismatch, for which we need a notion of a source witness: an event present at time 𝑡0 that records a source pointer sp as provenance for an item 𝑠 . We assume the existence of an application-specific predicate ExtractedFrom, which records that event 𝑒 is the trace event whose extraction procedure produced source item 𝑠 from source pointer sp. We require this predicate to be well-typed: ExtractedFrom𝑡0 (𝑠, sp; 𝑒𝑠 ) ⇒ 𝑒𝑠 ∈ Ev ∧ 𝑠 ∈ SourceItems ∧ sp ∈ Src𝑡0
∧ sp ∈ 𝑒𝑠 .witness ∧ DenotesLang (𝑒𝑠 .message, 𝑠). Then we record provenance for an extracted source item: SourceWitness𝑡0 (sp, 𝑠; trace) ≜ ∃𝑒𝑠 ∈ trace≤𝑡0 . sp ∈ Src𝑡0 ∧ ExtractedFrom𝑡0 (𝑠, sp; 𝑒𝑠 ) ∧ 𝑠 ∈ 𝐹𝑆,Src,𝑡0 . A stale source error arises when a source witness comes from an older pointer at time 𝑡0 , and Universal+,𝑡0 (𝑐; 𝐾𝑈 ,𝑡0 ) is replaced at time 𝑡 : StaleSource𝑡 (𝑚, sp, 𝑠, 𝑐; ctx, trace) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠)
∧ 𝑐 ∈ denotation𝑈 (𝑠) ∧ ∃𝑡0 < 𝑡 . (SourceWitness𝑡0 (sp, 𝑠; trace) ∧ Universal+,𝑡0 (𝑐; 𝐾𝑈 ,𝑡0 )) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ (Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∨ Universal?,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∨ Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 )).
• Refuted Source. Such a source satisfies Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) while Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) holds: RefutedSource𝑡 (𝑚, 𝑠, 𝑐; ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ DenotesLang (𝑚, 𝑠)
∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ). This is stronger than lack of justification for claim 𝑐 : the universal knowledge base justifies ¬𝑐 . It is an AI system error when the system uses this claim, or when source knowledge is itself being presented as authority for 𝑐 ; 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 ℎ 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: DependsOn𝐸,ctx,𝑡 (𝑚, 𝑐, ℎ) ≜ ∃𝜋 ∈ UsedDerivations𝐸,ctx,𝑡 (𝑚, 𝑐) .
ℎ ∈ Premises(𝜋) ∧ 𝑐 ∈ Infer∗𝑅𝑡̄ (Premises(𝜋)) ∧ 𝑐 ∉ Infer∗𝑅𝑡̄ (Premises(𝜋) ∖ {ℎ}).
Here UsedDerivations𝐸,ctx,𝑡 (𝑚, 𝑐) is the set of derivation, explanation, or provenance records actually used by the system in asserting 𝑐 through 𝑚, and Premises(𝜋) is the set of semantic premises used by 𝜋 . Let ℛ𝑡,ctx ≜ { 𝑐 ∈ 𝑈̄ ∣ ∃𝑚𝑐 ∈ Lang . ReliableClaim𝑡 (𝑚𝑐 , 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx) }. An asserted claim 𝑐 in message 𝑚 depends on an added hypothesis when the system asserted 𝑐 , actually used ℎ, 𝑐 is justified if we add ℎ but not justified from currently reliable claims alone, ℎ itself has no reliable witnessing message 𝑚ℎ , and 𝑐 is not otherwise directly supported: AddedHypothesis𝑡 (ℎ, 𝑐; 𝑚, ctx) ≜ ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) ∧ ℎ ∈ 𝑈̄ ∧ DependsOn𝐸,ctx,𝑡 (𝑚, 𝑐, ℎ)
∧ ¬ ∃𝑚ℎ ∈ Lang . ReliableClaim𝑡 (𝑚ℎ , ℎ; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx) ∧ 𝑐 ∈ Infer∗𝑅𝑡̄ (ℛ𝑡,ctx ∪ {ℎ}) ∧ 𝑐 ∉ Infer∗𝑅𝑡̄ (ℛ𝑡,ctx ) ∧ ¬ SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ). • Unsupported Use. When does an unsupported claim enter the trace? If 𝑒 is a new event extending a trace trace at time 𝑡 , write trace′ = trace ⋅ 𝑒 . Let ctx𝑡 ∈ Select𝑡 (trace) and ctx𝑡+1 ∈
14
Alglave & Cousot
Select𝑡+1 (trace′ ) be the selected contexts before and after the extension. An unsupported use is a transition from ¬ Effective+,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx𝑡 ,𝑡 ) to Effective+,𝑡+1 (𝑚, 𝑠; 𝐾𝐸,ctx𝑡+1 ,𝑡+1 ) while the asserted claim 𝑐 still fails the support check: UnsupportedUse𝑡+1 (𝑒, 𝑚, 𝑠, 𝑐; trace, ctx𝑡 , ctx𝑡+1 ) ≜ trace′ = trace ⋅ 𝑒
∧ ctx𝑡 ∈ Select𝑡 (trace) ∧ ctx𝑡+1 ∈ Select𝑡+1 (trace′ ) ∧ 𝑒.message = 𝑚 ∧ DenotesLang (𝑚, 𝑠) ∧ ¬ Effective+,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx𝑡 ,𝑡 ) ∧ Effective+,𝑡+1 (𝑚, 𝑠; 𝐾𝐸,ctx𝑡+1 ,𝑡+1 ) ∧ ClaimUse𝐸,ctx𝑡+1 ,𝑡+1 (𝑚, 𝑐) ∧ ¬ SupportedClaim𝑡+1 (𝑚, 𝑐; 𝐾𝑈 ,𝑡+1 , 𝐾𝑆,Src,𝑡+1 ).
Theorem 2 (Trace Soundness). Each of StaleSource𝑡 (𝑚, sp, 𝑠, 𝑐; ctx, trace), RefutedSource𝑡 (𝑚, 𝑠, 𝑐; ctx), AddedHypothesis𝑡 (ℎ, 𝑐; 𝑚, ctx), and UnsupportedUse𝑡+1 (𝑒, 𝑚, 𝑠, 𝑐; trace, ctx𝑡 , ctx𝑡+1 ) implies, respectively, RelianceFailure𝑡,ctx (𝑚, 𝑐) or RelianceFailure𝑡+1,ctx𝑡+1 (𝑚, 𝑐). 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 𝑅𝑡̄ , 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 𝑅𝑡̄ . 7.1.1 Definition. A symbolic component uses a language ModLang that abstracts SourceItems (where SourceItems ≜ Scope/≡𝑓 ). Its intended semantics is semModLang ∈ ModLang → SourceItems. Conversely, statements in SourceItems must be approximated by ModLang: encodeModLang ∈ SourceItems → 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 Lang; otherwise the component needs communication encoders and decoders encModLang ∈ Lang → ℘(ModLang) and decModLang ∈ ModLang ∪ {⊥} → Lang. For Oma: ModLang may model rules for picture and form; encodeModLang encodes rules into checker syntax; semModLang gives the meaning of an encoded rule; encModLang turns a system message into checker inputs; and decModLang turns the checker result, failure, or timeout back into a system message.
For a black-box symbolic component, we can represent the inference engine as inferenceModLang ∈ ℘(℘(ModLang) × (ModLang ∪ {⊥})), where ⊥ represents timeout, failure, or absence of an answer. This relation abstracts search over forget(ignore(𝑅𝑡̄ )), but may omit rules or add incorrect ones. For Oma: inferenceModLang is the execution relation of a picture-rule checker, source status checker, or form validator, and ⊥ is timeout, failure, or no answer from that checker.
7.1.2 Scoped correctness. A symbolic component is correct within the system’s scope if each non⊥ result it returns corresponds, through semModLang , to a consequence of the scoped underlying rules:
Ceci n’est pas une pipe
15
∀𝐻ModLang ⊆ ModLang . ∀𝑐 ∈ ModLang . (⟨𝐻ModLang , 𝑐⟩ ∈ inferenceModLang ) ⇒ semModLang (𝑐) ∈ Infer∗𝑅𝑆,𝑡 ({semModLang (ℎ) ∣ ℎ ∈ 𝐻ModLang }). This is a scoped correctness condition, which must be stated relative to ⟨𝑈̄ , 𝑅𝑡̄ ⟩: forgetting can introduce abstract consequences that are not consequences of the ideal rule system. For Oma: Consider the picture part of Oma’s application. Rules distinguish observing a picture from {𝑐
} {𝑐pictureChecked }
checking it: 𝑅picture = { 𝑐 pictureObserved ,
𝑐pictureUsable
pictureCandidate
}. Thus an observed picture does not imply its usability. Sup-
pose a forgetfulness abstraction collapses 𝑐pictureCandidate ≡𝑓 𝑐pictureChecked because the orchestrator stores a coarse UI item e.g. “picture status present”, while 𝑐pictureObserved and 𝑐pictureUsable stay distinguished. The ab{[𝑐pictureObserved ]≡𝑓 } {[𝑐pictureChecked ]≡𝑓 }
stract rules are forget(𝑅picture ) = { [𝑐
pictureCandidate ]≡𝑓
, [𝑐
pictureUsable ]≡𝑓
}. Since [𝑐pictureCandidate ]≡𝑓 = [𝑐pictureChecked ]≡𝑓 ,
we have: [𝑐pictureObserved ]≡𝑓 ⇒ [𝑐pictureCandidate ]≡𝑓 = [𝑐pictureChecked ]≡𝑓 ⇒ [𝑐pictureUsable ]≡𝑓 . The abstract system has therefore erroneously justified that the picture is usable from a mere observation.
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 Lang. Large language models are neural components specialised to token sequences. Their inputs and outputs are messages in Lang, typically natural language or token sequences. 7.2.1 Definition. A neural component is a black box decode𝑁𝑁 ∘ 𝑁𝑁 ∘ encode𝑁𝑁 ∈ Lang → Lang, where encode𝑁𝑁 ∈ Lang → ℝ𝑛 , 𝑁𝑁 ∈ ℝ𝑛 → ℝ𝑚 , and decode𝑁𝑁 ∈ ℝ𝑚 → Lang define the encoder encode𝑁𝑁 , the neural network 𝑁𝑁 itself and the decoder decode𝑁𝑁 . The encoder encode𝑁𝑁 is the interface between communication-level inputs and the input layer of the neural network 𝑁𝑁 . 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 𝑁𝑁 can be decomposed into transformers between layers 𝑁𝑁 = 𝑁𝑁ℓ ∘ ⋯ ∘ 𝑁𝑁1 . The transformers 𝑁𝑁1 , …, 𝑁𝑁ℓ map vectors using weights, calls, and optimisation procedures such as backpropagation and gradient descent. 𝑁𝑁1 is the transformer of the input layer into the first hidden layer and is applied first. 𝑁𝑁ℓ is the transformer of the last hidden layer into the output layer. This final transformer 𝑁𝑁ℓ shapes the result for the task: classification, regression, sequence generation, or another result format. The decoder decode𝑁𝑁 translates the result vector back into a communication message in Lang. For Oma: A neural encoder may convert the candidate passport picture into vectors, the neural network may classify or extract information, and the decoder may return a label, field value, or message in 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 denotationLang , expansion by CandidateClaims, assertion selection by AssertedClaims𝐸,ctx,𝑡 , and the support checks in ReliableClaim𝑡 .
16
Alglave & Cousot
The reliability obligation on this output is not that every element of CandidateClaims(output) be reliable, but rather that every claim 𝑐 ∈ AssertedClaims𝐸,ctx,𝑡 (output) asserted by the output be reliable for the selected context ctx: ReliableClaim𝑡 (output, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , 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 [2, 75, 94]. For Oma: Validation may include adversarial picture tests, OCR checks for passport fields, and monitoring for cases where the image or source has drifted away from what the component was tested on.
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) [6]. 7.3.1 Definition. An agent service Serv is formalised by internal states StatesServ and a transition relation transServ ∈ ℘((StatesServ × Lang × Lang) × (StatesServ × Lang × Lang)). ′ , 𝑚′ , 𝑚′ ⟩⟩ ∈ trans A transition ⟨⟨𝑠Serv , 𝑚𝑎𝑖 , 𝑚𝑤 ⟩, ⟨𝑠Serv 𝑤 Serv means that the service is in state 𝑎𝑖 𝑠Serv , reads a communication message 𝑚𝑎𝑖 from the AI system, reads the observed world mes′ , returns a communication sage 𝑚𝑤 = observation(Serv, 𝑤), changes its internal state to 𝑠Serv ′ message 𝑚𝑎𝑖 to the AI system, and may request a world update represented by 𝑚𝑤′ , producing 𝑤 ′ = actuation(𝑤, 𝑚𝑤′ ). 7.3.2 Service Conformance. A conformance relation for a service Serv has the form transServ ⊆ SpecServ where SpecServ ∈ ℘((StatesServ × Lang × Lang) × (StatesServ × Lang × 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. For Oma: In the app, the camera, browser, document scanner, picture checker, form filler, retrieval service, and possible official web-service client are agent services. Each service has a bounded job. None of them should quietly become the source of truth for the whole task, and none of them should be able to perform a high-consequence action merely because a generated sentence made it sound plausible.
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).
Ceci n’est pas une pipe
7.4
17
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 Lang, records intermediate state, and handles observations or updates of the world. The user normally interacts with the orchestrator through prompts in 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 𝑊 be the world and let the components of an orchestrator be • Language Lang with denotationLang , CandidateClaims, observation, and actuation; • Symbolic components ⟨ModLang, encModLang , decModLang , inferenceModLang ⟩ ∈ Symbolic; • Neural components ⟨encode𝑁𝑁 , 𝑁𝑁 , decode𝑁𝑁 ⟩ ∈ Neural; • Agent services ⟨StatesServ , transServ ⟩ ∈ Services. An orchestrator has internal states 𝑠Orch ∈ StatesOrch . The orchestrator also records the states 𝑠Serv indexed by services Serv ∈ Services, although these states can only be read and modified by their services. It communicates with the components through messages in Lang and with the world through observation and actuation. Together these form a closed system, whose states are: ClosedSystemStates ≜ StatesOrch ×
∏ Serv∈Services
StatesServ × 𝑊 × Trace.
Its transition relation transOrch ∈ ℘((ClosedSystemStates × Lang) × 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. For Oma: These five cases may be (Symbolic:) run a picture-rule checker or form validator; (Neural:) ask the language model to produce the next message or plan fragment; (Service:) call the camera, or government server; (Internal:) pause, resume, update context, or decide the next control label; (World:) record that the doorbell rang, or the form changed elsewhere. ′ ′ , 𝑠⃗ ′ , 𝑤 ′ , trace′ ⟩, where 𝑠⃗ Let 𝑠Closed ≜ ⟨𝑠Orch , 𝑠⃗Serv , 𝑤, trace⟩ and 𝑠Closed ≜ ⟨𝑠Orch Serv is the family Serv of service states and trace is the event trace. For Comp ∈ {Symbolic, Neural, Service, Internal, World}, Comp the transition relations are transOrch ⊆ (ClosedSystemStates × Lang) × ClosedSystemStates. Comp
The orchestrator transition relation is their union: transOrch ≜ ⋃Comp transOrch . Thus each transition in transOrch satisfies at least one of the following clauses. The symbol 𝑚′ , when it appears ′ below, names a message produced inside the transition and recorded in 𝑠Closed or in the appended event; it is not a separate output of transOrch . • 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 𝑜⊥ ∈ Lang, and stipulate that observation(Serv, 𝑤) = 𝑜⊥ . For services that do not request a world update, we use a distinguished no-actuation message 𝑚⊥ ∈ Lang, and stipulate that actuation(𝑤, 𝑚⊥ ) = 𝑤 . Let NoActuation(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 repre′ sented by these no-op messages. Formally, if ⟨⟨𝑠Closed , 𝑚⟩, 𝑠Closed ⟩ ∈ transService Orch , then there exist Serv ∈ Services with transition structure ⟨StatesServ , transServ ⟩, an observation message 𝑜 ∈ Lang, a world-update message 𝑚𝑤′ ∈ Lang, and an event 𝑒 ′ ∈ Ev such that 𝑜 = observation(Serv, 𝑤),
18
Alglave & Cousot
′ (Serv), 𝑚′ , 𝑚′ ⟩⟩ ∈ trans ′ ′ ⟨⟨⃗𝑠Serv (Serv), 𝑚, 𝑜⟩, ⟨⃗𝑠Serv 𝑤 Serv , (NoActuation(Serv) ⇒ 𝑚𝑤 = 𝑚⊥ ), 𝑤 = ′ ′ actuation(𝑤, 𝑚𝑤 ), and 𝑠⃗Serv (OtherServ) = 𝑠⃗Serv (OtherServ) for all OtherServ ∈ Services ∖ {Serv}, 𝑒 ′ .kind = Service, 𝑒 ′ .message = 𝑚′ , and trace′ = trace ⋅ 𝑒 ′ . The service reads the communication message 𝑚, observes the world through observation, returns a message 𝑚′ recorded in ′ 𝑠Closed , and updates the world through 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 encModLang , receives a result which is decoded by decModLang into Lang. This message ′ ′ back is recorded by the orchestrator in its next state 𝑠Closed . Formally, if ⟨⟨𝑠Closed , 𝑚⟩, 𝑠Closed ⟩∈ Symbolic
transOrch , then there exist ⟨ModLang, encModLang , decModLang , inferenceModLang ⟩ ∈ Symbolic, a hypothesis set 𝐻 ⊆ ModLang, a result 𝑟 ∈ ModLang ∪ {⊥}, and an event 𝑒 ′ ∈ Ev such that ′ 𝐻 = encModLang (𝑚), ⟨𝐻 , 𝑟⟩ ∈ inferenceModLang , 𝑚′ = decModLang (𝑟), 𝑠⃗Serv = 𝑠⃗Serv , 𝑤 ′ = 𝑤 , ′ ′ ′ ′ ′ 𝑒 .kind = Symbolic, 𝑒 .message = 𝑚 , 𝑒 .observation = 𝑜⊥ , 𝑒 .actuation = 𝑚⊥ (the distinguished no-observation and no-actuation messages of the Service clause above), and trace′ = trace ⋅ 𝑒 ′ . ′ The orchestrator state changes from 𝑠Orch to 𝑠Orch to record the call and its result. • Neural: the orchestrator calls a neural component by sending a message 𝑚 ∈ Lang, receives a ′ generated message 𝑚′ , and records the step and its result 𝑚′ in its next state 𝑠Closed . Formally, Neural ′ if ⟨⟨𝑠Closed , 𝑚⟩, 𝑠Closed ⟩ ∈ transOrch , then there exists ⟨encode𝑁𝑁 , 𝑁𝑁 , decode𝑁𝑁 ⟩ ∈ Neural ′ and an event 𝑒 ′ ∈ Ev such that 𝑚′ = decode𝑁𝑁 (𝑁𝑁 (encode𝑁𝑁 (𝑚))), 𝑠⃗Serv = 𝑠⃗Serv , 𝑤 ′ = 𝑤 , ′ ′ ′ ′ ′ 𝑒 .kind = Neural, 𝑒 .message = 𝑚 , 𝑒 .observation = 𝑜⊥ , 𝑒 .actuation = 𝑚⊥ , and trace′ = trace ⋅ 𝑒 ′ . For a large language model LLM, 𝑚′ = decodeLLM (NN(encodeLLM (𝑚))) is the call to LLM on a context window, encodeLLM feeds the selected context window and decodeLLM 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 ′ ⟩ ∈ transInternal context, or choose the next control label. Formally, if ⟨⟨𝑠Closed , 𝑚⟩, 𝑠Closed Orch , then ′ ′ ′ ′ 𝑠⃗Serv = 𝑠⃗Serv , 𝑤 = 𝑤 , and trace = trace. The internal state change from 𝑠Orch to 𝑠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 𝑠Orch or in a later event, rather than as a separate output of transOrch . • 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 ⟨⟨𝑠Closed , 𝑚⟩, 𝑠Closed ⟩ ∈ transWorld Orch , then 𝑠Orch = 𝑠Orch , ′ ′ ′ 𝑠⃗Serv = 𝑠⃗Serv , trace = trace, since only the world changes from 𝑤 to 𝑤 . 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 𝐼 ∈ ℘(ClosedSystemStates) which must be proved to hold initially and remains true after each transition transOrch . Since transOrch 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 𝐸𝑛𝑣 ⊆ 𝑊 × 𝑊 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.
Ceci n’est pas une pipe
19 Information State Srct , KU,t KS,Src,t , KE,ctx ,t
evaluated w.r.t.
Claims denotationLang , CandidateClaims SupportedClaimt , ReliableClaimst
selects ctx/update Information State call/return
Compute Components Symbolic, Neural , Services
checked against
Specifications AllowedEventSpec worldmapSpec , interpSpec
Orchestrator States Orch , trans Orch messages/events World wt ∈ W
observation/actuation
Interface Lang, W, Ev, Trace
Fig. 1. An AI system
Variant functions can prove termination or progress of bounded phases. Recurrent obligations need temporal assumptions such as fairness or explicit scheduling. For Oma: An invariant may say that readiness is unreachable unless sources, picture and form are checked, and confirmation is present in the trace. The environment relation admits outside changes such as the doorbell ringing or the phone moving. Liveness may require the orchestrator eventually to save, ask Oma, refuse, or route to a clerk rather than remain silently stuck.
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 1 An AI system is ⟨Information State, Components, Orchestrator, Interface, Claims, Specifications⟩: • Information State ≜ ⟨Src𝑡 , 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝐸,ctx,𝑡 ⟩ is the information-state layer: the reference sources Src𝑡 , the universal knowledge base 𝐾𝑈 ,𝑡 , the source-derived knowledge 𝐾𝑆,Src,𝑡 , and the AI system’s effective working knowledge 𝐾𝐸,ctx,𝑡 . • Components ≜ ⟨Symbolic, Neural, Services⟩ is the components layer: Symbolic components, Neural components, and Services e.g. prompts, tools, sensors, browsers, APIs, or actuators. • Orchestrator ≜ ⟨StatesOrch , transOrch ⟩ is the orchestrator layer: the orchestrator states StatesOrch , including control state, selected context ctx, memory and trace pointers, routing information, and the transition relation transOrch that advances the closed system by calling components, services, updating internal state, observing world changes, or producing messages and world updates. • Interface ≜ ⟨Lang, 𝑊 , Ev, Trace, observation, actuation⟩ is the interface layer: the communication language Lang, the set 𝑊 ⊆ 𝑈̄ of possible world states, the event records Ev, the traces Trace = Ev∗ , the observation interface from the world into the system, and the actuation interface by which system messages may change the world. • The claims layer is: Claims ≜ ⟨denotationLang , CandidateClaims, Asserts𝐸,ctx,𝑡 , AssertedClaims𝐸,ctx,𝑡 , SourceSupport𝑡 , SupportedClaim𝑡 , ReliableClaim𝑡 , DependsOn𝐸,ctx,𝑡 ⟩.
It contains the maps, application-specific relations, and judgments that connect communicationlevel items to underlying semantic claims. Messages map to intended source items via denotationLang . CandidateClaims maps messages in Lang to candidate semantic meanings. Asserts𝐸,ctx,𝑡 selects which candidate claims are actually asserted, and SourceSupport𝑡 records which source items
20
Alglave & Cousot
support which semantic claims. The remaining judgments separate assertion, external support, reliability, and actual derivational dependence. • The specifications layer is: Specifications ≜ ⟨AllowedEventSpec , worldmapSpec , interpSpec , RequiresSpec , CurrentWitnessesOKSpec , AuthorityOKSpec , ActuationOKSpec ⟩. It says which observations, actions, and other candidate events are sound; the specificationrelative 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. For Oma: The AI system is the whole passport app: Information State contains sources and the three knowledge bases; Components contains checkers, neural models, and services; Orchestrator contains the orchestrator state and transition relation; Interface contains messages, world state, observations, updates, events, and trace; Claims contains denotation, candidate-claim, support, reliance, and dependence judgments; and Specifications contains the event specification, world and event semantic maps.
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 trace = 𝑒1 … 𝑒𝑛 ∈ Trace be the event trace so far, let 𝑤𝑡 ∈ 𝑊 be the current world state, and let 𝑒 ∈ Ev be the next event. A specification supplies: worldmapSpec ∶ 𝑊 ⇀ ℘(𝑈̄ ), interpSpec ∶ Ev ⇀ ℘(𝑈̄ ),
ActuationOKSpec ∶ Trace × 𝑊 × Ev × 𝑊 → {true, false},
RequiresSpec ∶ Trace × 𝑊 → ℘(𝑈̄ ),
AllowedEventSpec ∶ Trace × 𝑊 × Ev → {true, false}.
AuthorityOKSpec ∶ Trace × 𝑊 × Ev → {true, false},
CurrentWitnessesOKSpec ∶ Trace × 𝑊 × Ev → {true, false}. For a partial map 𝑓 ∶ 𝑋 ⇀ 𝑌 , write 𝑓 (𝑥) ↓ when 𝑓 (𝑥) is defined and 𝑓 (𝑥) ↑ when it is undefined; definedness does not require 𝑓 (𝑥) to be nonempty when 𝑌 is a powerset. Here worldmapSpec (𝑤) records the semantic facts about world state 𝑤 that matter to Spec, while interpSpec (𝑒) records the semantic content of event 𝑒 : what it claims, records, witnesses, authorizes, observes, or changes. The set RequiresSpec (trace, 𝑤𝑡 ) records the task-relevant semantic claims that Spec requires at the current trace and world state. The predicates CurrentWitnessesOKSpec , AuthorityOKSpec , and ActuationOKSpec record the remaining acceptance obligations checked by the safeguard: witness freshness, permission or delegation, and whether the candidate actuation from 𝑤𝑡 to 𝑤 ′ is permitted. The content of worldmapSpec is the reference against which an application instantiates RequiresSpec and ActuationOKSpec , which may consult it when relating required claims and permitted updates to the current and proposed world states. If worldmapSpec (𝑤𝑡 ) ↑, some prior interpSpec (𝑒𝑖 ) ↑, or interpSpec (𝑒) ↑, then 𝑒 is not checkable under Spec and is not valid; an implementation may reject, pause, or route to fallback. For Oma: worldmapSpec (𝑤) may contain the current form value and picture state; interpSpec (𝑒) may contain the claim that a source was checked, a checker returned a result, or Oma confirmed the draft.
Ceci n’est pas une pipe
21
AllowedEventSpec lists the constraints given by Spec. If 𝑒 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 𝑒 is performed by the system then the specification can require AllowedEventSpec (trace, 𝑤𝑡 , 𝑒). We write SystemControlled(𝑒) when 𝑒 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. For Oma: We give an example of specification implemented in our prototype using the cat language [4], and shown in appendix. A write event 𝑒 labelled CheckReady is allowed only if the trace contains the selected route, a successful picture-check witness, a form-complete witness, and Oma’s confirmation of the draft. Moreover, no invalidation may occur between those witnesses and the readiness event: editing the form, changing the picture, the route, or revoking confirmation makes the prior support stale. This catches readiness checks without a picture check, without form completion, without Oma’s current draft confirmation, or after an edit that invalidates the earlier confirmation.
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 𝑒 are reliable: ReliableAssertions𝑡,ctx (trace; 𝑒) ≜ |trace| = 𝑡 ∧ ctx ∈ Select𝑡 (trace)
∧ ∀𝑐 ∈ AssertedClaims𝐸,ctx,𝑡 (𝑒.message) . ReliableClaim𝑡 (𝑒.message, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx).
• 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 AllowedEventSpec : Validity𝑡,Spec (trace, 𝑤; 𝑒) ≜ |trace| = 𝑡 ∧ worldmapSpec (𝑤) ↓ ∧(∀𝑒𝑗 ∈ trace . interpSpec (𝑒𝑗 ) ↓)
∧ interpSpec (𝑒) ↓ ∧∀ctx ∈ Select𝑡 (trace) . ReliableAssertions𝑡,ctx (trace; 𝑒). • Interface Agreement. The event record must match what the observation and actuation interfaces actually did: InterfaceOK(Serv, 𝑒, 𝑤, 𝑤 ′ ) ≜ Serv ∈ Services ∧ (𝑒.observation = 𝑜⊥ ∨ 𝑒.observation = observation(Serv, 𝑤))
∧ ((𝑒.actuation = 𝑚⊥ ∧ 𝑤 ′ = 𝑤) ∨ actuation(𝑤, 𝑒.actuation) = 𝑤 ′ ).
Here Serv is the service whose observation interface is being checked, and 𝑜⊥ and 𝑚⊥ are the no-observation and no-actuation messages used by the service semantics. • Step Satisfies Interface. We define the derived step relation StepOrch (𝑠, 𝑠⃗, trace, 𝑤, 𝑒, 𝑠 ′ , 𝑠⃗′ , 𝑤 ′ )
≜ ∃𝑚 ∈ Lang . ⟨⟨⟨𝑠, 𝑠⃗, 𝑤, trace⟩, 𝑚⟩, ⟨𝑠 ′ , 𝑠⃗′ , 𝑤 ′ , trace ⋅ 𝑒⟩⟩ ∈ transOrch .
22
Alglave & Cousot
Now, this invariant says that the step taken satisfies the interface agreement: StepOK(StepOrch ) ≜ ∀𝑠, 𝑠⃗, 𝑠 ′ , 𝑠⃗′ , trace, 𝑤, 𝑤 ′ , 𝑒 . StepOrch (𝑠, 𝑠⃗, trace, 𝑤, 𝑒, 𝑠 ′ , 𝑠⃗′ , 𝑤 ′ ) ⇒ ∃Serv ∈ Services . InterfaceOK(Serv, 𝑒, 𝑤, 𝑤 ′ ). 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 𝑒 to the trace, it would be desirable for an orchestrator to run SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx). At a high-level, the safeguard either accepts the event 𝑒 or rejects it. Here we discuss the acceptance case, and rejection cases are discussed later in Section 9.3: • Acceptance. A result Accept(𝑒, 𝑤 ′ ) records 𝑒 and commits the world update 𝑤 ′ . We write: SafeguardAcceptSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) ≜ SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = Accept(𝑒, 𝑤 ′ ).
• Acceptance certificate. An acceptance result is not itself a proof that 𝑒 is allowed. The safeguard must establish a structured certificate. First, every claim required by Spec at the current trace and world must have a reliable message: RequiredClaimsOKSpec,𝑡,ctx (trace, 𝑤; 𝑒) ≜ |trace| = 𝑡 ∧ ctx ∈ Select𝑡 (trace)
∧ ∀𝑐 ∈ RequiresSpec (trace, 𝑤) . ∃𝑚𝑐 ∈ Lang . ReliableClaim𝑡 (𝑚𝑐 , 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx).
Validity ranges over every context in Select𝑡 (trace) since a later call may select differently from the same trace, whereas 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: CurrentWitnessesOK checks that required witnesses are present and not invalidated, AuthorityOK checks permission and delegation, and ActuationOK checks that the proposed world update is permitted. The complete acceptance certificate is: AcceptOKSpec,𝑡,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ) ≜ Validity𝑡,Spec (trace, 𝑤; 𝑒) ∧ RequiredClaimsOKSpec,𝑡,ctx (trace, 𝑤; 𝑒)
∧ CurrentWitnessesOKSpec (trace, 𝑤; 𝑒) ∧ AuthorityOKSpec (trace, 𝑤; 𝑒) ∧ ActuationOKSpec (trace, 𝑤; 𝑒, 𝑤 ′ ).
• 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: AcceptAdequateSpec ≜
∀trace, 𝑤, 𝑒, 𝑤 ′ , ctx . AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ) ⇒ AllowedEventSpec (trace, 𝑤, 𝑒). The implementation-level safeguard contract says that every accept result comes with such a certificate: SafeguardAcceptSoundSpec (SafeguardSpec ) ≜
∀trace, 𝑤, 𝑒, 𝑤 ′ , ctx . SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = Accept(𝑒, 𝑤 ′ ) ⇒ AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). • Valid step. A valid step is a system-controlled orchestrator step whose proposed event has been accepted by the safeguard: ValidStepSpec (StepOrch , SafeguardSpec , trace, 𝑤, 𝑤 ′ , 𝑒, ctx, 𝑠, 𝑠⃗, 𝑠 ′ , 𝑠⃗′ ) ≜ StepOrch (𝑠, 𝑠⃗, trace, 𝑤, 𝑒, 𝑠 ′ , 𝑠⃗′ , 𝑤 ′ ) ∧ SystemControlled(𝑒) ∧ SafeguardAcceptSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx).
Ceci n’est pas une pipe
23
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: Theorem 3 (Valid steps for accepted controlled transitions). For all trace, 𝑤 , 𝑤 ′ , 𝑒 , ctx, 𝑠 , 𝑠⃗, 𝑠 ′ , 𝑠⃗′ : ValidStepSpec (StepOrch , SafeguardSpec , trace, 𝑤, 𝑤 ′ , 𝑒, ctx, 𝑠, 𝑠⃗, 𝑠 ′ , 𝑠⃗′ )
∧ SafeguardAcceptSoundSpec (SafeguardSpec ) ∧ AcceptAdequateSpec ∧ StepOK(StepOrch ) ⇒ AllowedEventSpec (trace, 𝑤, 𝑒) ∧ ∃Serv ∈ Services . InterfaceOK(Serv, 𝑒, 𝑤, 𝑤 ′ ). For Oma: The theorem says the app cannot record “ready for submission” because the UI indicates thus. A readiness event cannot silently entail SubmitPassportApplication; submission requires its own authority event and its own transition. That gives Oma a trace where every accepted app action has current witnesses, the right authority, and a permitted actuation. For the event 𝑒.name = CheckReady, the relevant orchestrator transition is the transition that records 𝑒 in the trace and, if its transition safeguard returns Accept(𝑒, 𝑤 ′ ), updates the world state to say that the draft is ready. The safeguard must establish: • the trace before 𝑒 contains the selected renewal route; a successful picture-check witness for the current picture; a form-complete witness for the current form values; Oma’s confirmation of the current draft; • no later event in that same history invalidates those witnesses by editing the form, changing the picture, changing the route, or revoking confirmation; • every readiness claim asserted by 𝑒.message is reliable in the selected context; • the event record and world update are readiness-only: the event name is CheckReady, the authority field does not contain SubmissionPermit, the actuation is not a submission message, and 𝑤 ′ differs from 𝑤 only by marking the draft ready. If the safeguard accepts, is accept-sound, and its acceptance certificate is adequate for the specification, the theorem gives AllowedEventSpec (trace, 𝑤, 𝑒), i.e. readiness check event is allowed at that point of the trace and world state. Separately, the interface wrapper around observation and actuation must record what actually happened, giving ∃Serv ∈ Services . InterfaceOK(Serv, 𝑒, 𝑤, 𝑤 ′ ). A transition that records 𝑒.name = SubmitPassportApplication has a different safeguard. Before it can record 𝑒 , the event history must already contain a distinct event 𝑒𝑗 with s.t. 𝑗 ≤ |trace|, and 𝑒𝑗 .name = SubmissionPermit or a prior event whose 𝑒𝑗 .authority field records Oma’s permission to submit. The submit event’s 𝑒.actuation is then the submission message, and 𝑤 ′ = actuation(𝑤, 𝑒.actuation) is the world state after that submission. This keeps the readiness event and the submission event as separate trace events with separate authority requirements.
9.3
Rejection diagnostics
Safeguard rejection has several cases: for controlled-transition soundness, every rejected transition must identify a failed semantic obligation for 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 SafeguardAcceptSoundSpec , they define the implementation-level rejection contract. Definition 4. SafeguardSpec is reject-sound, written SafeguardRejectSoundSpec (SafeguardSpec ), when every rejection result satisfies the obligation of its constructor, universally quantified over trace, 𝑤 , 𝑒 , 𝑤 ′ , ctx, and the constructor payload; the formal rendition is in Appendix B: • RejectMissingClaim(𝑐) obliges Unjustifiability|trace|,ctx (𝑐; trace, 𝑤, Spec): Spec requires 𝑐 at (trace, 𝑤), 𝑐 is universally positive, and no current reliable message justifies relying on 𝑐 . • RejectRelianceFailure(𝑚, 𝑐, 𝑑) obliges
𝑚 = 𝑒.message ∧ RelianceFailure|trace|,ctx (𝑚, 𝑐) ∧ DiagnosticOK|trace|,ctx (𝑑; 𝑚, 𝑐, 𝑒, trace)
24
Alglave & Cousot
where DiagnosticOK means that 𝑑 names a specific reliance-failure case established by the direct or history-derived diagnostic predicates of Section 6. • RejectStaleWitness(𝑐, 𝑒𝑗 ) obliges StaleWitnessSpec (trace, 𝑤; 𝑒, 𝑐, 𝑒𝑗 ): some earlier trace event witnessed 𝑐 , the later event 𝑒𝑗 invalidated that witness under Spec, and no later event restored a current witness for 𝑐 . • RejectMissingAuthority(𝑎) obliges MissingAuthoritySpec (trace, 𝑤; 𝑒, 𝑎): Spec requires prior authority 𝑎 for 𝑒 at (trace, 𝑤), but no prior trace event is 𝑎, records 𝑎 in its authority field, or interprets as 𝑎. • RejectForbiddenActuation(𝑟) obliges ForbiddenActuationSpec (trace, 𝑤; 𝑒, 𝑤 ′ , 𝑟): 𝑟 = 𝑒.actuation, 𝑟 ≠ 𝑚⊥ , 𝑤 ′ = actuation(𝑤, 𝑟), and Spec does not permit that actuation for this event at (trace, 𝑤). Reject-soundness ties each rejection to a true failure statement. To conclude that a rejected transition refutes the acceptance certificate AcceptOK, the failure predicates must also refute the corresponding certificate predicates CurrentWitnessesOKSpec , AuthorityOKSpec , and ActuationOKSpec , which Spec otherwise leaves opaque. This is a coherence condition on Spec alone: Definition 5. Spec is diagnostically coherent when, for all trace, 𝑤 , 𝑒 , 𝑤 ′ , 𝑐 , 𝑒𝑗 , 𝑎, 𝑟 : SpecCoherentSpec ≜ (StaleWitnessSpec (trace, 𝑤; 𝑒, 𝑐, 𝑒𝑗 ) ⇒ ¬ CurrentWitnessesOKSpec (trace, 𝑤; 𝑒))
∧ (MissingAuthoritySpec (trace, 𝑤; 𝑒, 𝑎) ⇒ ¬ AuthorityOKSpec (trace, 𝑤; 𝑒)) ∧ (ForbiddenActuationSpec (trace, 𝑤; 𝑒, 𝑤 ′ , 𝑟) ⇒ ¬ ActuationOKSpec (trace, 𝑤; 𝑒, 𝑤 ′ )). Under these two assumptions, diagnostic adequacy is a genuine implication: every rejection refutes an actual conjunct of the acceptance certificate. Theorem 6 (Rejection Adequacy). Assume SafeguardRejectSoundSpec (SafeguardSpec ) as well as SpecCoherentSpec . Then for all trace, 𝑤 , 𝑒 , 𝑤 ′ , and every ctx ∈ Select|trace| (trace): SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) ∈ RejectSpec ⇒ ¬ AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). Together with acceptance soundness, a total safeguard then decides the certificate: Theorem 7 (Safeguard Decision). Assume additionally SafeguardAcceptSoundSpec (SafeguardSpec ) and that SafeguardSpec is total: every call returns Accept(𝑒, 𝑤 ′ ) or a value in RejectSpec . Then for all trace, 𝑤 , 𝑒 , 𝑤 ′ , and every ctx ∈ Select|trace| (trace): SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = Accept(𝑒, 𝑤 ′ ) ⟺ AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). For Oma: Rejection adequacy says that the rejection reason is not decorative. If the safeguard returns RejectMissingAuthority(𝑎), then authority 𝑎 really is required by Spec and really is absent from the prior trace. If it returns RejectRelianceFailure(𝑚, 𝑐, 𝑑) then 𝑚 really is the event message, 𝑐 really fails the reliable-claims test, and 𝑑 really matches one of the diagnostic predicates. If it returns RejectStaleWitness(𝑐, 𝑒𝑗 ), then 𝑒𝑗 really does invalidate the earlier witness for 𝑐 , with no later witness. And if the app’s safeguard is total, accept-sound, and reject-sound over a coherent specification, Oma is never blocked by a spurious rejection nor waved through without a certificate: the safeguard accepts exactly the certified transitions.
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 [25]; trivalent, epistemic, and Belnap–Dunn/FDE logics separate truth, falsity, uncertainty,
Ceci n’est pas une pipe
25
belief, knowledge, both, and neither [13, 33, 81, 110]; and denotational semantics gives mathematical meanings to computational expressions independently of implementation [86, 91]. 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 [38], with our treatment of messages as signs echoing Peirce’s semiotic epistemology and Frege’s distinction between expression, sense, and reference [37, 72]. Justification logic, truth maintenance, and belief revision make evidence, dependency, retraction, and theory change explicit [3, 7, 8, 29, 32]. 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 [19, 20, 41, 59, 67, 73]. Our records differ in requiring semantic support relative to 𝐾𝑆,Src,𝑡 and 𝐾𝑈 ,𝑡 , not lineage alone; evidence logic and attribution evaluation give the corresponding epistemic and empirical views of Asserts𝐸,ctx,𝑡 and SourceSupport𝑡 [18, 45, 79]. Prompt programming and prompt-containing software treat prompts as program-like artefacts with constraints, control flow, maintenance obligations, and tests [16, 44, 63]. 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 [9, 34, 40, 60, 74, 97, 101]. For us prompts constrain proof/search over 𝐾𝐸,ctx,𝑡 , whereas retrieval and citation mechanisms populate or test 𝐾𝑆,Src,𝑡 ; neither model fluency nor a source pointer alone establishes truth in 𝐾𝑈 ,𝑡 . 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 [2, 70, 94, 95]. 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 [42, 43, 57, 58, 102]. 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 [39, 50, 55, 61, 62, 65, 71, 82, 83, 92, 99, 105, 106, 109]. 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 domainspecific 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 schemaguided dialogue and MCP agent-tool protocols [24, 30, 84, 87, 98, 104, 108]. 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,
26
Alglave & Cousot
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 [12, 21, 28, 31, 54, 64, 66, 68, 69, 85]. Finally, control theory, runtime assurance, agent verification, and agent security provide languages for constraining behaviour over time [5, 10, 27, 35, 36, 47, 51–53, 56, 78, 80, 90, 100, 107]. Agent-security works treat the model as an untrusted component and enforce invariants through the surrounding system [11, 23, 87]. 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 𝐾𝑈 ,𝑡 , the sourcederived knowledge 𝐾𝑆,Src,𝑡 , and the AI system’s effective knowledge 𝐾𝐸,ctx,𝑡 . 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. The app uses our framework as an engineering discipline. A readiness check is not merely a green UI tick: it is a record of observations, witnesses, source support, and Oma’s confirmation. References [1] Peter Aczel. An introduction to inductive definitions. In John Barwise, editor, Handbook of Mathematical Logic, chapter 7, pages 739–782. North–Holland, Amsterdam, 1977. [2] Aws Albarghouthi. Introduction to neural network verification, 2021. https://arxiv.org/abs/2109.10317. [3] Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change: Partial meet contraction and revision functions. The Journal of Symbolic Logic, 50(2):510–530, 1985. [4] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, 2014. [5] Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In 18th European Control Conference, pages 3420–3431, 2019. [6] Anthropic. Model Context Protocol. https://modelcontextprotocol.io/, 2024. Open standard introduced on November 25, 2024. [7] Sergei N. Artemov. Explicit provability and constructive semantics. The Bulletin of Symbolic Logic, 7(1):1–36, 2001. [8] Sergei N. Artemov and Melvin Fitting. Justification Logic: Reasoning with Reasons, volume 216 of Cambridge Tracts in Mathematics. Cambridge University Press, 2019. [9] Akari Asai, Zeqiu Wu, Yizhong Wang, Avirup Sil, and Hannaneh Hajishirzi. Self-RAG: Learning to retrieve, generate, and critique through self-reflection, 2023. https://arxiv.org/abs/2310.11511. [10] Karl Johan Åström and Richard M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, 2008. https://fbsbook.org. [11] Mislav Balunovic, Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. AI agents with formal security guarantees. In ICML 2024 Workshop on Next Generation of AI Safety, 2024. [12] Moritz Y. Becker, Cédric Fournet, and Andrew D. Gordon. SecPAL: Design and semantics of a decentralized authorization language. Journal of Computer Security, 18(4):619–665, 2010. [13] Nuel D. Belnap. A useful four-valued logic. In J. Michael Dunn and George Epstein, editors, Modern Uses of Multiple-Valued Logic, pages 5–37. D. Reidel, Dordrecht, 1977.
Ceci n’est pas une pipe
27
[14] Emily M. Bender, Timnit Gebru, Angelina McMillan-Major, and Shmargaret Shmitchell. On the dangers of stochastic parrots: Can language models be too big? In Proceedings of the 2021 ACM Conference on Fairness, Accountability, and Transparency, pages 610–623, 2021. [15] Emily M. Bender and Alexander Koller. Climbing towards NLU: On meaning, form, and understanding in the age of data. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 5185–5198, 2020. [16] Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. Prompting is programming: A query language for large language models. Proc. ACM Program. Lang., 7(PLDI):1946–1969, 2023. [17] Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001. [18] Bernd Bohnet, Vinh Q. Tran, Pat Verga, Roee Aharoni, Daniel Andor, Livio Baldini Soares, Massimiliano Ciaramita, Jacob Eisenstein, Kuzman Ganchev, Jonathan Herzig, et al. Attributed question answering: Evaluation and modeling for attributed large language models. arXiv:2212.08037, 2022. [19] Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. Why and where: A characterization of data provenance. In Proceedings of the 8th International Conference on Database Theory (ICDT), volume 1973 of LNCS, pages 316–330. Springer, 2001. [20] James Cheney, Laura Chiticariu, and Wang-Chiew Tan. Provenance in databases: Why, how, and where. Foundations and Trends in Databases, 1(4):379–474, 2009. [21] Alessandro Chiesa and Eran Tromer. Proof-carrying data and hearsay arguments from signature cards. In Innovations in Computer Science, pages 310–331. Tsinghua University Press, 2010. [22] Noam Chomsky. Three models for the description of language. IRE Trans. Inf. Theory, 2(3):113–124, 1956. [23] Mihai Christodorescu, Earlence Fernandes, Ashish Hooda, Somesh Jha, Johann Rehberger, Kamalika Chaudhuri, Xiaohan Fu, Khawaja Shams, Guy Amir, Jihye Choi, Sarthak Choudhary, Nils Palumbo, Andrey Labunets, and Nishit V. Pandya. Agent security is a systems problem, 2026. [24] Manuel Costa, Boris Köpf, Aashish Kolluri, Andrew Paverd, Mark Russinovich, Ahmed Salem, Shruti Tople, Lukas Wutschitz, and Santiago Zanella-Béguelin. Securing AI agents with information-flow control, 2025. [25] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977. [26] Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth ACM Symposium on Principles of Programming Languages, pages 269–282, 1979. [27] Maxwell Crouse, Ibrahim Abdelaziz, Cristina Cornelio, Veronika Thost, Lingfei Wu, Kenneth D. Forbus, and Achille Fokoue. Formally specifying the high-level behavior of LLM-based agents, 2023. https://arxiv.org/abs/2310.08535. [28] Nicodemos Damianou, Naranker Dulay, Emil Lupu, and Morris Sloman. The ponder policy specification language. In Policies for Distributed Systems and Networks, volume 1995 of Lecture Notes in Computer Science, pages 18–38. Springer, 2001. [29] Johan de Kleer. An assumption-based TMS. Artificial Intelligence, 28(2):127–162, 1986. [30] Edoardo Debenedetti, Ilia Shumailov, Tianqi Fan, Jamie Hayes, Nicholas Carlini, Daniel Fabian, Christoph Kern, Chongyang Shi, Andreas Terzis, and Florian Tramèr. Defeating prompt injections by design, 2025. [31] John DeTreville. Binder, a logic-based security language. In 2002 IEEE Symposium on Security and Privacy, pages 105–113. IEEE Computer Society, 2002. [32] Jon Doyle. A truth maintenance system. Artificial Intelligence, 12(3):231–272, 1979. [33] J. Michael Dunn. Intuitive semantics for first-degree entailments and “coupled trees”. Philosophical Studies, 29(3):149–168, 1976. [34] Shahul Es, Jithin James, Luis Espinosa-Anke, and Steven Schockaert. RAGAS: Automated evaluation of retrieval augmented generation, 2023. https://arxiv.org/abs/2309.15217. [35] Eric Fang. AgentVerify: Compositional formal verification of AI agent safety properties via LTL model checking. Preprints.org, 2026. [36] Noe Y. Flandre, Alexander C. Nwala, and Philippe J. Giabbanelli. Composing verifiable conceptual models via building blocks: Towards design-time verification of agentic AI workflows, 2026. [37] Gottlob Frege. Über sinn und bedeutung. Zeitschrift für Philosophie und philosophische Kritik, 100:25–50, 1892. [38] A. Galton. Formal semantics: is it relevant to artificial intelligence? Artificial Intelligence Review, 2:151–165, 1988. [39] Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. PAL: Program-aided language models, 2022. https://arxiv.org/abs/2211.10435. [40] Tianyu Gao, Howard Yen, Jiatong Yu, and Danqi Chen. Enabling large language models to generate text with citations. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 2023. https://arxiv.org/abs/2305.14627.
28
Alglave & Cousot
[41] Deepak Garg, Limin Jia, and Anupam Datta. Policy auditing over incomplete logs: Theory, implementation and applications. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS), pages 151–162. ACM, 2011. [42] Fabian Gloeckle, Mantas Bakšys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, and Peter O’Hearn. WybeCoder: Verified imperative code generation, 2026. https://arxiv.org/abs/2603.29088. [43] Qiuhan Gu, Avaljot Singh, and Gagandeep Singh. SAIL: Sound abstract interpreters with LLMs. Proceedings of the ACM on Programming Languages, 10(PLDI), 2026. [44] Tommy Guy, Peli de Halleux, Reshabh K. Sharma, and Ben Zorn. Prompts are programs. SIGPLAN Blog, 2024. [45] Joseph Y. Halpern and Riccardo Pucella. A logic for reasoning about evidence. Journal of Artificial Intelligence Research, 26:1–34, 2006. [46] David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Cambridge University Press, 1928. [47] Kerianne L. Hobbs, Mark L. Mote, Matthew C. Abate, Samuel Coogan, and Eric M. Feron. Run time assurance for safety-critical systems: An introduction to safety filtering approaches for complex control systems. IEEE Control Systems Magazine, 43(2):28–65, 2023. [48] Aidan Hogan, Eva Blomqvist, and Stefan Dietze et al. Knowledge Graphs. Springer, 2022. [49] Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Ye Jin Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. ACM Computing Surveys, 55(12):1–38, 2023. [50] Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. SWE-bench: Can language models resolve real-world GitHub issues? In International Conference on Learning Representations, 2024. https://arxiv.org/abs/2310.06770. [51] Leslie Pack Kaelbling, Michael L. Littman, and Anthony R. Cassandra. Planning and acting in partially observable stochastic domains. Artificial Intelligence, 101(1–2):99–134, 1998. [52] Nafiseh Kahani, Masoud Barati, and Diana Addae. Runtime compliance verification for AI agents, 2026. [53] Rudolf E. Kalman. A new approach to linear filtering and prediction problems. Journal of Basic Engineering, 82(1):35– 45, 1960. [54] Parnian Shabani Kamran, Premkumar T. Devanbu, and Caleb Stanford. Vision paper: Proof-carrying code completions. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering Workshops, pages 35–42. ACM, 2024. [55] Ehud Karpas, Omri Abend, Yonatan Belinkov, Barak Lenz, Opher Lieber, Nir Ratner, Yoav Shoham, Hofit Bata, Yoav Levine, Kevin Leyton-Brown, Dor Muhlgay, Noam Rozen, Erez Schwartz, Gal Shachaf, Shai Shalev-Shwartz, Amnon Shashua, and Moshe Tenenholtz. MRKL systems: A modular, neuro-symbolic architecture that combines large language models, external knowledge sources and discrete reasoning, 2022. https://arxiv.org/abs/2205.00445. [56] Roham Koohestani. AgentGuard: Runtime verification of AI agents, 2025. Accepted at the Agentic Software Engineering workshop, ASE 2025. [57] Shuvendu K. Lahiri. Evaluating LLM-driven user-intent formalization for verification-aware languages. In Proceedings of the 24th Conference on Formal Methods in Computer Aided Design, 2024. [58] Shuvendu K. Lahiri. Intent formalization: A grand challenge for reliable coding in the age of AI agents, 2026. [59] Martin Leucker and Christian Schallhart. A brief account of runtime verification. Journal of Logic and Algebraic Programming, 78(5):293–303, 2009. [60] Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. Retrieval-augmented generation for knowledge-intensive NLP tasks. In Advances in Neural Information Processing Systems, volume 33, pages 9459– 9474, 2020. [61] Junjie Li, Xi Xiao, Yunbei Zhang, Chen Liu, Lin Zhao, Xiaoying Liao, Yingrui Ji, Janet Wang, Jianyang Gu, Yingqiang Ge, Weijie Xu, Xi Fang, Xiang Xu, Tianchen Zhao, Youngeun Kim, Tianyang Wang, Jihun Hamm, Smita Krishnaswamy, Jun Huan, and Chandan Reddy. Agent harness engineering: A survey, 2026. https://openreview.net/ forum?id=3hXEPbG0dh. [62] Minghao Li, Feifan Song, Bowen Yu, Haiyang Yu, Zhoujun Li, Fei Huang, and Yongbin Li. API-Bank: A benchmark for tool-augmented LLMs, 2023. https://arxiv.org/abs/2304.08244. [63] Jenny T. Liang, Melissa Lin, Nikitha Rao, and Brad A. Myers. Prompts are programs too! understanding how developers build software containing prompts. Proc. ACM Softw. Eng., 2(FSE):1591–1614, 2025. [64] Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run-time security policies. International Journal of Information Security, 4(1–2):2–16, 2005. [65] Xiao Liu, Hao Yu, Hanchen Zhang, Yifan Xu, Xuanyu Lei, Hanyu Lai, Yu Gu, Hangliang Ding, Kaiwen Men, Kejuan Yang, Shudan Zhang, Xiang Deng, Aohan Zeng, Zhengxiao Du, Chenhui Zhang, Sheng Shen, Tianjun Zhang, Yu Su, Huan Sun, Minlie Huang, Yuxiao Dong, and Jie Tang. AgentBench: Evaluating LLMs as agents, 2023. https://arxiv. org/abs/2308.03688.
Ceci n’est pas une pipe
29
[66] Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119–161, 2011. [67] Luc Moreau and Paolo Missier. PROV-DM: The PROV data model. W3C Recommendation, https://www.w3.org/TR/ prov-dm/, 2013. [68] George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119. ACM Press, 1997. [69] OASIS. eXtensible Access Control Markup Language (XACML) version 3.0. OASIS Standard, 2013. [70] Abhinandan Pal, Francesco Ranzato, Caterina Urban, and Marco Zanella. Abstract interpretation-based feature importance for support vector machines. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I, Lecture Notes in Computer Science, pages 27–49. Springer, 2024. [71] Shishir G. Patil, Tianjun Zhang, Xin Wang, and Joseph E. Gonzalez. Gorilla: Large language model connected with massive APIs, 2023. https://arxiv.org/abs/2305.15334. [72] Charles Sanders Peirce. Collected Papers of Charles Sanders Peirce. Harvard University Press, Cambridge, MA, 1931–1935. Edited by Charles Hartshorne and Paul Weiss. [73] Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. Functional programs that explain their work. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 365–376. ACM, 2012. [74] Fabio Petroni, Tim Rocktäschel, Sebastian Riedel, Patrick Lewis, Anton Bakhtin, Yuxiang Wu, and Alexander Miller. Language models as knowledge bases? In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP), pages 2463–2473. Association for Computational Linguistics, 2019. [75] Francesc Pifarre-Esquerda, Éric Goubault, and Sylvie Putot. Propagation of interval belief structures and imprecise copulas for neural network verification, 2026. [76] Wolfram Pohlers. Proof theory : an introduction. Springer, 1989. [77] Ali Rahimi and Benjamin Recht. Reflections on random kitchen sinks. NeurIPS Test of Time Award Talk, 2017. https://www.argmin.net/p/machine-learning-as-alchemy. [78] Peter J. Ramadge and W. Murray Wonham. Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization, 25(1):206–230, 1987. [79] Hannah Rashkin, Vitaly Nikolaev, Matthew Lamm, Lora Aroyo, Michael Collins, Dipanjan Das, Slav Petrov, Gaurav Singh Tomar, Iulia Turc, and David Reitter. Measuring attribution in natural language generation models. Computational Linguistics, 49(4), 2023. [80] James B. Rawlings, David Q. Mayne, and Moritz M. Diehl. Model Predictive Control: Theory, Computation, and Design. Nob Hill Publishing, 2 edition, 2017. https://sites.engineering.ucsb.edu/~jbraw/mpc/. [81] Rasmus Rendsvig, John Symons, and Yanjing Wang. Epistemic logic. In The Stanford Encyclopedia of Philosophy (Summer 2025 Edition), Edward N. Zalta and Uri Nodelman (eds.), 2025. https://plato.stanford.edu/archives/ sum2025/entries/logic-epistemic/. [82] Yangjun Ruan, Honghua Dong, Andrew Wang, Silviu Pitis, Yongchao Zhou, Jimmy Ba, Yann Dubois, Chris J. Maddison, and Tatsunori Hashimoto. Identifying the risks of LM agents with an LM-emulated sandbox, 2023. https://arxiv.org/abs/2309.15817. [83] Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Eric Hambro, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to use tools. In Advances in Neural Information Processing Systems, volume 36, 2023. https://arxiv.org/abs/2302.04761. [84] Pius Schlapbach. Formal semantics for agentic tool protocols, 2026. [85] Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30–50, 2000. [86] Dana S. Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG-6, Programming Research Group, Oxford University Computing Laboratory, 1971. [87] Tianneng Shi, Jingxuan He, Zhun Wang, Hongwei Li, Linyu Wu, Wenbo Guo, and Dawn Song. Progent: Securing AI agents with privilege control, 2025. [88] Joseph R. Shoenfield. Mathematical Logic. Taylor Francis, 2nd edition, 1967. [89] Abraham Silberschatz, Henry F. Korth, and S. Sudarshan. Database System Concepts. McGraw-Hill Education, New York, NY, 7th edition, 2020. [90] Eduardo D. Sontag. Mathematical Control Theory: Deterministic Finite Dimensional Systems. Springer, 2 edition, 1998. [91] Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13(1–2):11–49, 2000.
30
Alglave & Cousot
[92] Theodore R. Sumers, Shunyu Yao, Karthik Narasimhan, and Thomas L. Griffiths. Cognitive architectures for language agents, 2023. https://arxiv.org/abs/2309.02427. [93] Alfred Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific J. of Math., 5:285–310, 1955. [94] Caterina Urban and Antoine Miné. A review of formal methods applied to machine learning. CoRR, abs/2104.02466, 2021. [95] Caterina Urban, Pavle Subotic, and Filip Drobnjakovic. Static analysis by abstract interpretation against data leakage in machine learning. Sci. Comput. Program., 246:103338, 2025. [96] Dirk van Dalen. Logic and Structure. Springer, 2013. [97] Fei Wang, Xingchen Wan, Ruoxi Sun, Jiefeng Chen, and Sercan O. Arik. Astute RAG: Overcoming imperfect retrieval augmentation and knowledge conflicts for large language models. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 30553–30571. Association for Computational Linguistics, 2025. [98] Haoyu Wang, Christopher M. Poskitt, and Jun Sun. AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents, 2025. Accepted at ICSE 2026. [99] Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, Wayne Xin Zhao, Zhewei Wei, and Ji-Rong Wen. A survey on large language model based autonomous agents, 2023. https://arxiv.org/abs/2308.11432. [100] Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, and Tong Zhang. Lean4Agent: Formal modeling and verification for agent workflow and trajectory, 2026. [101] Yike Wang, Shangbin Feng, Heng Wang, Weijia Shi, Vidhisha Balachandran, Tianxing He, and Yulia Tsvetkov. Resolving knowledge conflicts in large language models. In First Conference on Language Modeling, 2024. [102] Ran Wei, Le Zhu, Haochi Wang, Jim Woodcock, Fang Yan, Simon Foster, and Xiangyang Ji. Formal-method-guided vibe coding: Closing the verification loop on AI-generated safety-critical software through model-driven engineering, 2026. [103] Joseph Weizenbaum. ELIZA—a computer program for the study of natural language communication between man and machine. Communications of the ACM, 9(1):36–45, 1966. [104] Yuhao Wu, Franziska Roesner, Tadayoshi Kohno, Ning Zhang, and Umar Iqbal. IsolateGPT: An execution isolation architecture for LLM-based agentic systems. In Proceedings of the Network and Distributed System Security Symposium, 2025. [105] John Yang, Carlos E. Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press. SWEagent: Agent-computer interfaces enable automated software engineering, 2024. https://arxiv.org/abs/2405.15793. [106] Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. ReAct: Synergizing reasoning and acting in language models. In International Conference on Learning Representations, 2023. https: //arxiv.org/abs/2210.03629. [107] Yedi Zhang, Yufan Cai, Xinyue Zuo, Xiaokun Luan, Kailong Wang, Zhe Hou, Yifan Zhang, Zhiyuan Wei, Meng Sun, Jun Sun, Jing Sun, and Jin Song Dong. The fusion of large language models and formal methods for trustworthy AI agents: A roadmap, 2024. https://arxiv.org/abs/2412.06512. [108] Peter Yong Zhong, Siyuan Chen, Ruiqi Wang, McKenna McCall, Ben L. Titzer, Heather Miller, and Phillip B. Gibbons. RTBAS: Defending LLM agents against prompt injection and privacy leakage, 2025. [109] Shuyan Zhou, Frank F. Xu, Hao Zhu, Xuhui Zhou, Robert Lo, Abishek Sridhar, Xianyi Cheng, Yonatan Bisk, Daniel Fried, Uri Alon, and Graham Neubig. WebArena: A realistic web environment for building autonomous agents, 2023. https://arxiv.org/abs/2307.13854. [110] Paul Égré and Lorenzo Rossi (eds.). Handbook of Trivalent Logics. MIT press, 2026 (to appear). https://mitpress.mit. edu/9780262054003/handbook-of-trivalent-logics/.
Ceci n’est pas une pipe
31
A Theorems and Proofs This appendix gives proof sketches for our theorems. A.1
Theorem 1: Exhaustiveness
PRoof of theoRem 1 on exhaustiveness. Fix 𝑠 such that DenotesLang (𝑚, 𝑠). (⇒) Suppose RelianceFailure𝑡,ctx (𝑚, 𝑐). By the definitions of RelianceFailure, ClaimUse, and AssertedClaims𝐸,ctx,𝑡 , we have ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐), 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚, and 𝑐 ∈ CandidateClaims(𝑚). Since the fixed predicate DenotesLang (𝑚, 𝑠) supplies the denotation conjunct and, by the four-status definitions and ⊕ status exclusivity, 𝐾𝐸,ctx,𝑡 ⊢+ 𝑡 𝑚 entails 𝐾𝐸,ctx,𝑡 ⊢𝑡 𝑚, we also have Effective⊕,𝑡 (𝑚, 𝑠; 𝐾𝐸,ctx,𝑡 ). Moreover, RelianceFailure gives ¬ ReliableClaim𝑡 (𝑚, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx), so the definition of ReliableClaim and the preceding facts give ¬ SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ). Because DenotesLang is functional and 𝑠 is the fixed denotation of 𝑚, this unsupported-claim fact is equivalently
¬(Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ SourceSupport𝑡 (𝑠, 𝑐)). Let us consider all possible cases Universal×,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) for × ∈ {+, −, ±, ?}. • If Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) then RefutedAssertion𝑡 (𝑚, 𝑐; ctx) follows directly from ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) and the definition of RefutedAssertion; • if Universal?,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) then UnsupportedAssertion𝑡 (𝑚, 𝑐; ctx) follows from the common claimuse, denotation, effective-one-sidedness, and unsupported-claim facts above, together with the definition of UnsupportedAssertion; • if Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) then again by case analysis: Source±,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∨ Source?,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ⇒ Extrapolation𝑡 (𝑚, 𝑐; ctx), Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ⇒ SourceUniversalMismatch𝑡 (𝑚, 𝑠, 𝑐; ctx), Source−,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ⇒ RefutedSourceContradictoryClaim𝑡 (𝑚, 𝑠, 𝑐; ctx).
• If Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) then ¬(Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ SourceSupport𝑡 (𝑠, 𝑐)) must hold. – Either ¬Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) gives SpuriousSupport𝑡 (𝑚, 𝑠, 𝑐; ctx), – or Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ ¬SourceSupport𝑡 (𝑠, 𝑐) gives SourceSupportGap𝑡 (𝑚, 𝑠, 𝑐; ctx). (⇐) The definition of the seven predicates implies ¬(Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ) ∧ SourceSupport𝑡 (𝑠, 𝑐)). The first four each force ¬Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ), for RefutedAssertion via status exclusivity. SpuriousSupport forces ¬Source+,𝑡 (𝑠; 𝐾𝑆,Src,𝑡 ); SourceSupportGap forces ¬SourceSupport𝑡 (𝑠, 𝑐). And finally RefutedSourceContradictoryClaim forces ¬Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ). □ A.2
Theorem 2: Trace soundness
PRoof of theoRem 2 on tRace soundness. In each case ClaimUse𝐸,ctx,⋅ (𝑚, 𝑐) is a literal conjunct, so by definition of RelianceFailure it suffices to show ¬ ReliableClaim⋅ (𝑚, 𝑐; … ), which by definition of ReliableClaim𝑡 follows from ¬ SupportedClaim⋅ (𝑚, 𝑐; 𝐾𝑈 ,⋅ , 𝐾𝑆,Src,⋅ ). • StaleSource. The final disjunct of the definition gives Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ), Universal?,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ), or Universal±,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ); each excludes Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) by status exclusivity (§2), so it is the case that SupportedClaim𝑡 (𝑚, 𝑐; … ) fails on its universal conjunct. • RefutedSource. Since the four base justification statuses are mutually exclusive by definition (§2), Universal−,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) excludes Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ), so SupportedClaim𝑡 (𝑚, 𝑐; … ) fails on its second conjunct. • AddedHypothesis. ¬ SupportedClaim𝑡 (𝑚, 𝑐; 𝐾𝑈 ,𝑡 , 𝐾𝑆,Src,𝑡 ) is a literal conjunct.
32
Alglave & Cousot
• UnsupportedUse. ¬ SupportedClaim𝑡+1 (𝑚, 𝑐; 𝐾𝑈 ,𝑡+1 , 𝐾𝑆,Src,𝑡+1 ) is a literal conjunct, taken at ctx𝑡+1 . □ A.3
Theorem 3: Valid steps for accepted controlled transitions
PRoof of theoRem 3 on Valid steps foR accepted contRolled tRansitions. From ValidStep we get the recorded orchestrator step and the accepted safeguard result. Accept-soundness gives AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). By AcceptAdequateSpec , this certificate entails AllowedEventSpec (trace, 𝑤, 𝑒). Instantiating StepOK with the same recorded step yields a service witness for the observation interface. □ A.4
Theorem 6: Rejection Adequacy
PRoof. Let 𝑡 = |trace| and res = SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) ∈ RejectSpec , and proceed by cases on the constructor of res; in each case we refute one conjunct of AcceptOKSpec,𝑡,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). If res = RejectMissingClaim(𝑐), reject-soundness gives Unjustifiability𝑡,ctx (𝑐; trace, 𝑤, Spec), whose conjuncts include 𝑐 ∈ RequiresSpec (trace, 𝑤) and the absence of any 𝑚𝑐 ∈ Lang with ReliableClaim𝑡 (𝑚𝑐 , 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx). Hence the universally quantified clause of the predicate RequiredClaimsOKSpec,𝑡,ctx (trace, 𝑤; 𝑒) fails at this 𝑐 , refuting the second conjunct of AcceptOK. If res = RejectRelianceFailure(𝑚, 𝑐, 𝑑), it is the case that reject-soundness gives 𝑚 = 𝑒.message as well as RelianceFailure𝑡,ctx (𝑚, 𝑐). By definition of RelianceFailure, ClaimUse𝐸,ctx,𝑡 (𝑚, 𝑐) holds, so 𝑐 ∈ AssertedClaims𝐸,ctx,𝑡 (𝑒.message), and ¬ ReliableClaim𝑡 (𝑚, 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx) holds. Since |trace| = 𝑡 and ctx ∈ Select𝑡 (trace) by hypothesis, the universally quantified clause of ReliableAssertions𝑡,ctx (trace; 𝑒) fails at this 𝑐 ; as ctx is a selected context, the final conjunct of Validity𝑡,Spec (trace, 𝑤; 𝑒) fails, refuting the first conjunct of AcceptOK. If res = RejectStaleWitness(𝑐, 𝑒𝑗 ), reject-soundness gives StaleWitnessSpec (trace, 𝑤; 𝑒, 𝑐, 𝑒𝑗 ), and diagnostic coherence gives ¬ CurrentWitnessesOKSpec (trace, 𝑤; 𝑒), refuting the third conjunct. The cases RejectMissingAuthority(𝑎) and RejectForbiddenActuation(𝑟) are identical, using the cases MissingAuthoritySpec ⇒ ¬ AuthorityOKSpec and ForbiddenActuationSpec ⇒ ¬ ActuationOKSpec to refute the fourth and fifth conjuncts respectively. □ A.5 Theorem 7: Safeguard Decision PRoof. Left to right is SafeguardAcceptSoundSpec (SafeguardSpec ). Right to left: suppose that it is the case that AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). By totality the safeguard returns Accept(𝑒, 𝑤 ′ ) or a value in RejectSpec ; the latter is impossible, since Theorem 6 would ensure that it is the case that ¬ AcceptOKSpec,|trace|,ctx (trace, 𝑤, 𝑒, 𝑤 ′ ). □ B 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 4) is then SafeguardRejectSoundSpec (SafeguardSpec ) ≜ the conjunction of the five constructor implications below, universally quantified over trace, 𝑤 , 𝑒 , 𝑤 ′ , ctx, and the respective payloads. The complete
Ceci n’est pas une pipe
33
rejection-result family is RejectSpec
B.1
∶∶= RejectMissingClaim(𝑐) ∣ RejectRelianceFailure(𝑚, 𝑐, 𝑑) ∣ RejectStaleWitness(𝑐, 𝑒𝑗 ) ∣ RejectMissingAuthority(𝑎) ∣ RejectForbiddenActuation(𝑟).
RejectMissingClaim Unjustifiability𝑡,ctx (𝑐; trace, 𝑤𝑡 , Spec) ≜
|trace| = 𝑡 ∧ ctx ∈ Select𝑡 (trace) ∧ 𝑐 ∈ RequiresSpec (trace, 𝑤𝑡 ) ∧ Universal+,𝑡 (𝑐; 𝐾𝑈 ,𝑡 ) ∧ ¬ ∃𝑚𝑐 ∈ Lang . ReliableClaim𝑡 (𝑚𝑐 , 𝑐; 𝐾𝐸,ctx,𝑡 , 𝐾𝑆,Src,𝑡 , 𝐾𝑈 ,𝑡 , ctx). SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = RejectMissingClaim(𝑐)
⇒ Unjustifiability|trace|,ctx (𝑐; trace, 𝑤, Spec). B.2
RejectRelianceFailure DiagnosticOK𝑡,ctx (𝑑; 𝑚, 𝑐, 𝑒, trace) ≜
(𝑑 = Extrapolation ∧ Extrapolation𝑡 (𝑚, 𝑐; ctx)) ∨ (𝑑 = RefutedAssertion ∧ RefutedAssertion𝑡 (𝑚, 𝑐; ctx)) ∨ (𝑑 = UnsupportedAssertion ∧ UnsupportedAssertion𝑡 (𝑚, 𝑐; ctx)) ∨ ∃𝑠 . (𝑑 = SourceUniversalMismatch(𝑠) ∧ SourceUniversalMismatch𝑡 (𝑚, 𝑠, 𝑐; ctx)) ∨ ∃𝑠 . (𝑑 = SpuriousSupport(𝑠) ∧ SpuriousSupport𝑡 (𝑚, 𝑠, 𝑐; ctx)) ∨ ∃𝑠 . (𝑑 = SourceSupportGap(𝑠) ∧ SourceSupportGap𝑡 (𝑚, 𝑠, 𝑐; ctx)) ∨ ∃𝑠 . (𝑑 = RefutedSourceContradictoryClaim(𝑠) ∧RefutedSourceContradictoryClaim𝑡 (𝑚, 𝑠, 𝑐; ctx)) ∨ ∃sp, 𝑠 . (𝑑 = StaleSource(sp, 𝑠) ∧ StaleSource𝑡 (𝑚, sp, 𝑠, 𝑐; ctx, trace)) ∨ ∃𝑠 . (𝑑 = RefutedSource(𝑠) ∧ RefutedSource𝑡 (𝑚, 𝑠, 𝑐; ctx)) ∨ ∃ℎ . (𝑑 = AddedHypothesis(ℎ) ∧ AddedHypothesis𝑡 (ℎ, 𝑐; 𝑚, ctx)) ∨ ∃𝑠, ctx𝑡+1 . (𝑑 = UnsupportedUse(𝑠) ∧ ctx𝑡+1 ∈ Select𝑡+1 (trace ⋅ 𝑒) ∧ UnsupportedUse𝑡+1 (𝑒, 𝑚, 𝑠, 𝑐; trace, ctx, ctx𝑡+1 )). SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = RejectRelianceFailure(𝑚, 𝑐, 𝑑)
⇒ 𝑚 = 𝑒.message ∧ RelianceFailure|trace|,ctx (𝑚, 𝑐) ∧ DiagnosticOK|trace|,ctx (𝑑; 𝑚, 𝑐, 𝑒, trace).
34
Alglave & Cousot
B.3
RejectStaleWitness
TraceWitnessSpec (𝑒𝑖 , 𝑒, 𝑐; trace) ≜
𝑒𝑖 ∈ trace ∧ interpSpec (𝑒𝑖 ) ↓ ∧𝑐 ∈ interpSpec (𝑒𝑖 ) ∧ (𝑒𝑖 ∈ 𝑒.witness ∨ ∃𝐼 ⊆ [1, |trace|] . 𝐼 ∈ 𝑒.witness ∧ ∃𝑘 ∈ 𝐼 . 𝑒𝑖 = trace[𝑘] ∨ ∃𝑡0 , sp, 𝑠 . sp ∈ 𝑒.witness ∧ SourceWitness𝑡0 (sp, 𝑠; trace) ∧ ExtractedFrom𝑡0 (𝑠, sp; 𝑒𝑖 )). StaleWitnessSpec (trace, 𝑤; 𝑒, 𝑐, 𝑒𝑗 ) ≜ worldmapSpec (𝑤) ↓
∧ (∀𝑒𝑘 ∈ trace . interpSpec (𝑒𝑘 ) ↓) ∧ interpSpec (𝑒) ↓ ∧ ∃𝑖, 𝑗 ∈ [1, |trace|] . 𝑖 < 𝑗 ∧ trace[𝑗] = 𝑒𝑗 ∧ TraceWitnessSpec (trace[𝑖], 𝑒, 𝑐; trace) ∧ a witness-invalidation clause of Spec classifies 𝑒𝑗 as invalidating trace[𝑖] for 𝑐 at (trace, 𝑤)
∧ ¬ ∃ℓ ∈ [𝑗 + 1, |trace|] . TraceWitnessSpec (trace[ℓ], 𝑒, 𝑐; trace) ∧ Spec classifies trace[ℓ] as a current witness for 𝑐. (SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = RejectStaleWitness(𝑐, 𝑒𝑗 )) ⇒ StaleWitnessSpec (trace, 𝑤; 𝑒, 𝑐, 𝑒𝑗 ). B.4
RejectMissingAuthority MissingAuthoritySpec (trace, 𝑤; 𝑒, 𝑎) ≜ worldmapSpec (𝑤) ↓
∧ (∀𝑒𝑗 ∈ trace . interpSpec (𝑒𝑗 ) ↓) ∧ interpSpec (𝑒) ↓ ∧ Spec requires prior authority 𝑎 for 𝑒 at (trace, 𝑤) ∧ ¬ ∃𝑗 ∈ [1, |trace|] . (trace[𝑗] = 𝑎 ∨ 𝑎 ∈ trace[𝑗].authority ∨ 𝑎 ∈ interpSpec (trace[𝑗])). SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = RejectMissingAuthority(𝑎)
⇒ MissingAuthoritySpec (trace, 𝑤; 𝑒, 𝑎). B.5
RejectForbiddenActuation ForbiddenActuationSpec (trace, 𝑤; 𝑒, 𝑤 ′ , 𝑟) ≜ worldmapSpec (𝑤) ↓
∧ (∀𝑒𝑗 ∈ trace . interpSpec (𝑒𝑗 ) ↓) ∧ interpSpec (𝑒) ↓ ∧𝑟 = 𝑒.actuation ∧ 𝑟 ≠ 𝑚⊥ ∧ actuation(𝑤, 𝑟) = 𝑤 ′ ∧ no actuation clause of Spec allows the tuple (trace, 𝑤, 𝑒.name, 𝑒.kind, 𝑒.resource, 𝑒.authority, 𝑒.witness, 𝑒.actuation, 𝑟).
Ceci n’est pas une pipe
(SafeguardSpec (trace, 𝑤, 𝑒, 𝑤 ′ , ctx) = RejectForbiddenActuation(𝑟)) ⇒ ForbiddenActuationSpec (trace, 𝑤; 𝑒, 𝑤 ′ , 𝑟).
35
36
C
Alglave & Cousot
Example implementation of a specification written in cat [4]
(* Readiness for submission. *) let s_before = po let E_ready = E_appAgent & E_write & E_checkReady let E_filled = E_checkForm let s_readiness_route = [E_ukRenewalPicked | E_frRenewalPicked] ; feeds_into ; [E_ready] let s_readiness_picture = [E_checkPicture] ; was_checked_before ; [E_ready] let s_readiness_form = [E_filled] ; was_checked_before ; [E_ready] let s_readiness_confirmation = [E_confirmDraft] ; permits ; [E_ready] let s_readiness_stale = [E_formEditInvalidatedConfirmation] ; invalidates ; [E_ready] let s_readiness_support = s_readiness_route | s_readiness_picture | s_readiness_form | s_readiness_confirmation empty E_ready \ range(s_readiness_route) as s_readiness_requires_route empty E_ready \ range(s_readiness_picture) as s_readiness_requires_picture empty E_ready \ range(s_readiness_form) as s_readiness_requires_form empty E_ready \ range(s_readiness_confirmation) as s_readiness_requires_confirmation empty s_readiness_support \ s_before as s_readiness_support_must_precede_ready empty s_readiness_stale & s_before as s_readiness_requires_current_form_state empty ((invalidates ; s_readiness_support) & s_before) as s_readiness_support_not_invalidated