Pith. sign in

REVIEW 3 major objections 6 minor 110 references

Ceci n'est pas une pipe: AI systems as semantic abstractions

T0 review · 3 major / 6 minor · reviewed 2026-07-13 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read An AI system's output is an engineered representation, not the fact it appears to describe, and is reliable only when justified across accepted domain knowledge, reference sources, and what the system can currently use, plus explicit author

desk verdict Solid formal stack for AI reliability with real theorems; the maps that ground it are left to applications, so the force is definitional rather than automatic. read the letter →

arxiv 2607.09489 v1 pith:YW3MGT4E submitted 2026-07-10 cs.AI cs.PL

Jade Alglave , Patrick Cousot This is my paper · ORCID
classification cs.AIcs.PL
keywords AIsystemssemanticabstractionsknowledgebasesreliableclaimshallucinationdiagnosticsagentorchestrationeventtracestransitionsafeguards
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper treats AI systems as engineered semantic abstractions rather than magic or oracles: a generated answer, citation, tool call, or world-changing action is a message whose meaning must be checked, not a fact in itself. The authors introduce three knowledge layers—what accepted domain knowledge justifies, what reference sources say, and what the system can currently use from context—and define when a claim asserted through a message is reliable. That layering yields precise diagnostics for common failures such as unsupported assertions, extrapolation, stale or refuted sources, source-versus-knowledge mismatches, added hypotheses, and unsupported use. For agents that observe or change the world, controlled steps must also pass a safeguard that checks current witnesses, authority, and permitted actuation. The point is a usable vocabulary for specifying and auditing systems whose consequential outputs must rest on reliable claims and explicit authority rather than fluent text.

What carries the argument

The Information State—universal knowledge base K_U,t, source-derived knowledge K_S,Src,t, and effective knowledge K_E,ctx,t—together with the reliability predicate ReliableClaim_t (and the related diagnostics and transition safeguard). It separates denotation, candidate claims, asserted claims, supported claims, and reliable claims so failures and allowed actuations can be stated and checked.

What would settle it

Implement the proposed safeguard and event specification on a passport-renewal (or similar) agent: if a readiness or submission step can still be accepted after a form edit invalidates witnesses or without user confirmation, while the diagnostics report no failure, the soundness claims fail.

Watch

Extended reading notes

Core claim

An AI system's output is not the object it appears to describe but an engineered representation. A claim asserted through a message is reliable only when the message is justified by the system's effective knowledge, the claim is supported by both source-derived knowledge and universal domain knowledge, and—for system-controlled world updates—a safeguard has accepted the event after checking current witnesses, authority, and permitted actuation.

Load-bearing premise

The framework needs a usable statement of accepted domain knowledge against which claims can be judged supported, refuted, or unknown; if that knowledge cannot be fixed for a domain, the external reliability judgments lose their anchor.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper proposes a semantic framework that treats AI systems as engineered abstractions rather than oracles. It distinguishes three knowledge layers—universal domain knowledge K_U,t, source-derived knowledge K_S,Src,t, and effective working knowledge K_E,ctx,t—together with traces, authority, and world interfaces. Messages are mapped through denotation, candidate claims, asserted claims, source support, and a reliability predicate ReliableClaim_t. From these definitions the authors derive a taxonomy of reliance and history failures (extrapolation, unsupported assertion, stale source, added hypothesis, etc.) and a transition-safeguard model for controlled actuations. Theorems 1–3 and 6–7 (with appendix proof sketches) establish exhaustiveness of the reliance diagnostics, trace soundness of history failures, and relative soundness/decision properties of accept/reject safeguards. A passport-renewal prototype is used as a running example.

Significance. If the framework is adopted, it supplies a precise vocabulary for obligations that are usually left informal: when a citation, tool result, or world-changing action may be relied on, and which layer failed when it may not. The separation of K_U, K_S, and K_E, the witness/authority fields on events, and the AcceptOK certificate are useful engineering targets for agent harnesses and runtime monitors. Credit is due for the explicit failure taxonomy, the exhaustiveness and safeguard theorems with proof sketches, and the concrete cat-language readiness specification in Appendix C. The contribution is definitional and relative rather than an absolute decision procedure for natural-language domains; its value is as a specification and audit discipline, not as a free-standing factuality oracle.

major comments (3)
  1. Sections 3.2 and 5.1–5.3 leave denotationLang, CandidateClaims, Asserts_E,ctx,t, and SourceSupport_t as unconstrained application maps, and Section 4.5 notes that K_U,t may be unavailable for natural language. Theorems 1–3 and 6–7 then establish only relative exhaustiveness/soundness with respect to those maps. The abstract and conclusion still prescribe that outputs and actuations “must be justified by reliable claims.” Without minimal non-vacuity or soundness obligations on the maps (e.g., that SourceSupport_t respects denotation_U and that Asserts cannot invent claims outside CandidateClaims beyond what is already stated), ReliableClaim_t can be instantiated so that almost any fluent message is reliable or almost none is. The central normative claim therefore needs either (i) explicit soundness/non-vacuity conditions on a correct instantiation, or (ii) a clearer scoping statement that
  2. Section 9 defines SafeguardAcceptSoundSpec, AcceptAdequateSpec, SafeguardRejectSoundSpec, and SpecCoherentSpec as assumptions on the implementation and on Spec; Theorems 3, 6, and 7 then derive AllowedEventSpec and certificate decision from those assumptions. The manuscript should state more prominently (near the theorem statements and in the conclusion) that these are conditional results: they do not construct a safeguard or prove that a given orchestrator meets AcceptOK, they only show that any safeguard meeting the contracts decides the certificate and that accepted steps are allowed. As written, a reader can over-read the theorems as establishing end-to-end controlled-transition soundness for deployed agents.
  3. Section 7.1.2’s picture-checker example correctly shows that forgetfulness can introduce abstract consequences not justified by the ideal rules (observed picture ⇒ usable). The system-level soundness story in Sections 8–9 relies on ReliableClaim and event specifications to block such errors, but the paper never states a global soundness theorem relating an AI system (as an abstraction of an ideal semantic system, per the introduction) to the ideal system under stated conditions on ignore/forget and on the application maps. Either supply such a theorem (even a schematic one) or explicitly limit the claim to local certificate soundness of controlled steps, so the “AI systems as semantic abstractions” framing is not stronger than what is proved.
minor comments (6)
  1. The running Oma/passport example is helpful but often repeats the same readiness narrative; a short table mapping each failure predicate of Section 6 to one concrete passport-app scenario would make the taxonomy easier to use.
  2. Figure 1 is described in the text but the relationships among Information State, Claims, Specifications, and Orchestrator would benefit from a one-sentence caption stating what is checked versus what is selected.
  3. Notation for time indices and context selection (t vs |trace|, ctx ∈ Select_t(trace)) is dense; a small notation table early in Section 4 would reduce load.
  4. The prototype is said to be available on request; for a journal version, a public artifact or appendix walkthrough showing at least one RejectRelianceFailure / RejectStaleWitness path on a real trace would strengthen credibility without requiring a large empirical study.
  5. Related work is broad and useful; a tighter comparison paragraph against runtime-enforcement / proof-carrying-agent lines (AgentSpec, Progent, CaMeL, edit automata) stating what is new in the three-layer knowledge split versus policy languages alone would help placement.
  6. Minor typos and style: “Paraconsistentjustification” spacing (Section 2); occasional long sentences in Sections 4.5 and 9.2 could be split for readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: a definitional semantics framework whose theorems are consequences of independently layered predicates, not fitted or self-forced predictions.

full rationale

This paper is a formal framework paper, not an empirical or predictive derivation. It introduces three knowledge bases (K_U,t, K_S,Src,t, K_E,ctx,t), maps from messages to candidate/asserted claims, and predicates ReliableClaim, SupportedClaim, and a family of failure diagnostics, then proves definitional consequences: exhaustiveness of the reliance-failure taxonomy (Thm 1), that history failures imply reliance failures (Thm 2), and soundness/adequacy of transition safeguards relative to those definitions (Thms 3, 6–7). None of these steps fit parameters to data, rename a target quantity as a prediction, or import a uniqueness theorem from the authors that forbids alternatives. Self-citations (cat language [4]; abstract interpretation [25,26]) supply modeling tools and an example specification language; they are not load-bearing uniqueness claims that force the central reliability criterion. Application-defined maps (denotationLang, CandidateClaims, SourceSupport, etc.) being left open is a vacuity/correctness concern about external force of the framework, not circularity of the derivation chain. Score 0 with empty steps is the honest finding.

Assumptions & free parameters 0 free parameters · 6 assumptions · 4 invented entities

The paper is a definitional formal-methods framework. It rests on standard lattice/fix-system mathematics, domain assumptions about how AI systems are structured (orchestrator, services, traces), and several invented semantic objects (three knowledge bases, reliability predicates, safeguard certificates) introduced to state the claims. There are no fitted free parameters. Invented entities are mathematical constructs with no independent empirical handle outside applications that instantiate them.

assumptions (6)
  • standard math Tarski least fixed points exist for ⊆-monotone inference operators Infer_R, so Infer*_R(B) is well-defined (Section 2).
    Used to define justification and closure of knowledge bases.
  • standard math Ignorance and forgetfulness form Galois-style abstractions (ignore = intersect Scope; forget = quotient by ≡_f) yielding scoped rule systems R_S,t (Section 4.2).
    Standard abstract-interpretation setup; soundness/incompleteness relative to Ū follows from the abstractions.
  • domain assumption An AI system can be decomposed into Information State, Symbolic/Neural/Services components, Orchestrator, Interface, Claims, and Specifications communicating through Lang (Sections 1, 7–8).
    Architectural modeling choice that all later transition and safeguard definitions presuppose.
  • domain assumption For a given application, denotationLang, CandidateClaims, Asserts_E,ctx,t, SourceSupport_t, worldmapSpec, interpSpec, RequiresSpec, and AllowedEventSpec can be fixed well enough to check events (Sections 3–5, 8.2).
    These maps are explicitly application-defined; the framework’s checks are only as good as those instantiations.
  • domain assumption A universal knowledge base K_U,t of accepted domain facts and rules exists (or applications explicitly disclaim when it does not) (Sections 4.1, 4.5).
    External anchor for Universal± statuses and SupportedClaim; paper acknowledges NL domains may lack a clean K_U,t.
  • ad hoc to paper Four base justification statuses (+, −, ±, ?) are mutually exclusive and exhaustive for each claim relative to a knowledge base (Section 2).
    Paraconsistent status algebra tailored for the failure taxonomy; standard in multi-valued logics but chosen here as the paper’s status lattice.
invented entities (4)
  • Triple knowledge state (K_U,t, K_S,Src,t, K_E,ctx,t) plus Src_t
    purpose: Separate domain truth, source-derived content, and what the system may currently use.
    Core modeling invention; no independent evidence outside applications that instantiate the three bases.
  • ReliableClaim / SupportedClaim / AssertedClaims pipeline
    purpose: Define when a message-asserted claim may be relied on.
    Definitional construct used by all failure diagnostics and safeguards.
  • Transition safeguard AcceptOK / RejectSpec certificates
    purpose: Gate system-controlled events on reliability, witnesses, authority, and actuation permission.
    Operational contract invented for controlled-transition soundness theorems.
  • Reliance-failure and history-failure diagnostic predicates (Extrapolation, StaleSource, AddedHypothesis, etc.)
    purpose: Taxonomize common AI failures as layer mismatches.
    Named failure modes are paper-defined; exhaustiveness is relative to those definitions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Ceci n'est pas une pipe: AI systems as semantic abstractions." pith.science (2026). https://pith.science/paper/YW3MGT4E

@misc{pith2026260709489,
  author       = {Pith},
  title        = {Pith review of: Ceci n'est pas une pipe: AI systems as semantic abstractions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YW3MGT4E}},
  note         = {Machine review of arXiv:2607.09489}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.09489 by the authors.

Figure 1
Figure 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. … view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

110 extracted references · 22 linked inside Pith

  1. [1]

    An introduction to inductive definitions

    Peter Aczel. An introduction to inductive definitions. In John Barwise, editor,Handbookof MathematicalLogic, chapter 7, pages 739–782. North–Holland, Amsterdam, 1977

    1977

  2. [2]

    Introduction to neural network verification, 2021.https://arxiv.org/abs/2109.10317

    Aws Albarghouthi. Introduction to neural network verification, 2021.https://arxiv.org/abs/2109.10317

    arXiv 2021

  3. [3]

    Alchourrón, Peter Gärdenfors, and David Makinson

    Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change: Partial meet contrac- tion and revision functions.TheJournalof SymbolicLogic, 50(2):510–530, 1985

    1985

  4. [4]

    Herding cats: Modelling, simulation, testing, and data mining for weak memory

    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

    2014

  5. [5]

    Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada

    Aaron D. Ames, Samuel Coogan, Magnus Egerstedt, Gennaro Notomista, Koushil Sreenath, and Paulo Tabuada. Control barrier functions: Theory and applications. In18thEuropeanControlConference, pages 3420–3431, 2019

    2019

  6. [6]

    Model Context Protocol.https://modelcontextprotocol.io/, 2024

    Anthropic. Model Context Protocol.https://modelcontextprotocol.io/, 2024. Open standard introduced on November 25, 2024

    2024

  7. [7]

    Sergei N. Artemov. Explicit provability and constructive semantics.TheBulletinof SymbolicLogic, 7(1):1–36, 2001

    2001

  8. [8]

    Artemov and Melvin Fitting.JustificationLogic:ReasoningwithReasons, volume 216 ofCambridgeTracts in Mathematics

    Sergei N. Artemov and Melvin Fitting.JustificationLogic:ReasoningwithReasons, volume 216 ofCambridgeTracts in Mathematics. Cambridge University Press, 2019

    2019

Show all 110 references
  1. [9]

    Self-RAG: Learning to retrieve, generate, and critique through self-reflection, 2023.https://arxiv.org/abs/2310.11511

    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

    2023 arXiv

  2. [10]

    Murray.FeedbackSystems:An Introductionfor ScientistsandEngineers

    Karl Johan Åström and Richard M. Murray.FeedbackSystems:An Introductionfor ScientistsandEngineers. Prince- ton University Press, 2008.https://fbsbook.org

    2008

  3. [11]

    AI agents with formal security guarantees

    Mislav Balunovic, Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. AI agents with formal security guarantees. In ICML 2024 Workshopon NextGenerationof AI Safety, 2024

    2024

  4. [12]

    Becker, Cédric Fournet, and Andrew D

    Moritz Y. Becker, Cédric Fournet, and Andrew D. Gordon. SecPAL: Design and semantics of a decentralized autho- rization language.Journalof ComputerSecurity, 18(4):619–665, 2010

    2010

  5. [13]

    Nuel D. Belnap. A useful four-valued logic. In J. Michael Dunn and George Epstein, editors,Modern Uses of Multiple-ValuedLogic, pages 5–37. D. Reidel, Dordrecht, 1977. Ceci n’est pas une pipe 27

    1977

  6. [14]

    Bender, Timnit Gebru, Angelina McMillan-Major, and Shmargaret Shmitchell

    Emily M. Bender, Timnit Gebru, Angelina McMillan-Major, and Shmargaret Shmitchell. On the dangers of stochastic parrots: Can language models be too big? InProceedingsof the2021 ACM Conferenceon Fairness,Accountability, andTransparency, pages 610–623, 2021

    2021

  7. [15]

    Bender and Alexander Koller

    Emily M. Bender and Alexander Koller. Climbing towards NLU: On meaning, form, and understanding in the age of data. InProceedingsof the58thAnnualMeetingof theAssociationfor ComputationalLinguistics, pages 5185–5198, 2020

    2020

  8. [16]

    Prompting is programming: A query language for large language models.Proc

    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

    1946

  9. [17]

    Cambridge University Press, 2001

    Patrick Blackburn, Maarten de Rijke, and Yde Venema.ModalLogic. Cambridge University Press, 2001

    2001

  10. [18]

    Tran, Pat Verga, Roee Aharoni, Daniel Andor, Livio Baldini Soares, Massimiliano Ciaramita, Jacob Eisenstein, Kuzman Ganchev, Jonathan Herzig, et al

    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.08...

    2022 arXiv

  11. [19]

    Why and where: A characterization of data provenance

    Peter Buneman, Sanjeev Khanna, and Wang-Chiew Tan. Why and where: A characterization of data provenance. In Proceedingsof the8thInternationalConferenceon DatabaseTheory(ICDT), volume 1973 ofLNCS, pages 316–330. Springer, 2001

    1973

  12. [20]

    Provenance in databases: Why, how, and where.Foundations andTrendsin Databases, 1(4):379–474, 2009

    James Cheney, Laura Chiticariu, and Wang-Chiew Tan. Provenance in databases: Why, how, and where.Foundations andTrendsin Databases, 1(4):379–474, 2009

    2009

  13. [21]

    Proof-carrying data and hearsay arguments from signature cards

    Alessandro Chiesa and Eran Tromer. Proof-carrying data and hearsay arguments from signature cards. In Innovationsin ComputerScience, pages 310–331. Tsinghua University Press, 2010

    2010

  14. [22]

    Three models for the description of language.IRE Trans.Inf

    Noam Chomsky. Three models for the description of language.IRE Trans.Inf. Theory, 2(3):113–124, 1956

    1956

  15. [23]

    Mihai Christodorescu, Earlence Fernandes, Ashish Hooda, Somesh Jha, Johann Rehberger, Kamalika Chaudhuri, Xi- aohan Fu, Khawaja Shams, Guy Amir, Jihye Choi, Sarthak Choudhary, Nils Palumbo, Andrey Labunets, and Nishit V. Pandya. Agent security is a systems problem, 2026

    2026

  16. [24]

    Securing AI agents with information-flow control, 2025

    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

    2025

  17. [25]

    Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InConferenceRecord of theFourthACM Symposium on Principles of Programming Languages, pages 238–252, 1977

    1977

  18. [26]

    Systematic design of program analysis frameworks

    Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. InConferenceRecord of theSixthACM Symposium on Principlesof Programming Languages, pages 269–282, 1979

    1979

  19. [27]

    Forbus, and Achille Fokoue

    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

    2023 arXiv

  20. [28]

    The ponder policy specification language

    Nicodemos Damianou, Naranker Dulay, Emil Lupu, and Morris Sloman. The ponder policy specification language. In Policiesfor DistributedSystemsandNetworks, volume 1995 ofLectureNotesin ComputerScience, pages 18–38. Springer, 2001

    1995

  21. [29]

    An assumption-based TMS.ArtificialIntelligence, 28(2):127–162, 1986

    Johan de Kleer. An assumption-based TMS.ArtificialIntelligence, 28(2):127–162, 1986

    1986

  22. [30]

    Defeating prompt injections by design, 2025

    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

    2025

  23. [31]

    Binder, a logic-based security language

    John DeTreville. Binder, a logic-based security language. In2002 IEEE Symposium on SecurityandPrivacy, pages 105–113. IEEE Computer Society, 2002

    2002

  24. [32]

    A truth maintenance system.ArtificialIntelligence, 12(3):231–272, 1979

    Jon Doyle. A truth maintenance system.ArtificialIntelligence, 12(3):231–272, 1979

    1979

  25. [33]

    coupled trees

    J. Michael Dunn. Intuitive semantics for first-degree entailments and “coupled trees”.PhilosophicalStudies, 29(3):149–168, 1976

    1976

  26. [34]

    RAGAS: Automated evaluation of retrieval augmented generation, 2023.https://arxiv.org/abs/2309.15217

    Shahul Es, Jithin James, Luis Espinosa-Anke, and Steven Schockaert. RAGAS: Automated evaluation of retrieval augmented generation, 2023.https://arxiv.org/abs/2309.15217

    2023 arXiv

  27. [35]

    AgentVerify: Compositional formal verification of AI agent safety properties via LTL model checking

    Eric Fang. AgentVerify: Compositional formal verification of AI agent safety properties via LTL model checking. Preprints.org, 2026

    2026

  28. [36]

    Flandre, Alexander C

    Noe Y. Flandre, Alexander C. Nwala, and Philippe J. Giabbanelli. Composing verifiable conceptual models via build- ing blocks: Towards design-time verification of agentic AI workflows, 2026

    2026

  29. [37]

    Über sinn und bedeutung.Zeitschriftfür PhilosophieundphilosophischeKritik, 100:25–50, 1892

    Gottlob Frege. Über sinn und bedeutung.Zeitschriftfür PhilosophieundphilosophischeKritik, 100:25–50, 1892

  30. [38]

    A. Galton. Formal semantics: is it relevant to artificial intelligence?ArtificialIntelligenceReview, 2:151–165, 1988

    1988

  31. [39]

    PAL: Program-aided language models, 2022.https://arxiv.org/abs/2211.10435

    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

    2022 arXiv

  32. [40]

    Enabling large language models to generate text with citations

    Tianyu Gao, Howard Yen, Jiatong Yu, and Danqi Chen. Enabling large language models to generate text with citations. In Proceedingsof the2023 Conferenceon Empirical Methodsin NaturalLanguageProcessing, 2023. https://arxiv.org/abs/2305.14627. 28 Alglave & Cousot

    2023 arXiv

  33. [41]

    Policy auditing over incomplete logs: Theory, implementation and applications

    Deepak Garg, Limin Jia, and Anupam Datta. Policy auditing over incomplete logs: Theory, implementation and applications. InProceedingsof the18thACM ConferenceonComputerandCommunicationsSecurity(CCS), pages 151–162. ACM, 2011

    2011

  34. [42]

    Holden, Gabriel Synnaeve, and Peter O’Hearn

    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

    2026 arXiv

  35. [43]

    SAIL: Sound abstract interpreters with LLMs.Proceedingsof the ACM on Programming Languages, 10(PLDI), 2026

    Qiuhan Gu, Avaljot Singh, and Gagandeep Singh. SAIL: Sound abstract interpreters with LLMs.Proceedingsof the ACM on Programming Languages, 10(PLDI), 2026

    2026

  36. [44]

    Sharma, and Ben Zorn

    Tommy Guy, Peli de Halleux, Reshabh K. Sharma, and Ben Zorn. Prompts are programs. SIGPLAN Blog, 2024

    2024

  37. [45]

    Halpern and Riccardo Pucella

    Joseph Y. Halpern and Riccardo Pucella. A logic for reasoning about evidence.Journalof ArtificialIntelligence Research, 26:1–34, 2006

    2006

  38. [46]

    Cambridge University Press, 1928

    David Hilbert and Wilhelm Ackermann.Grundzüge der theoretischen Logik. Cambridge University Press, 1928

    1928

  39. [47]

    Hobbs, Mark L

    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 SystemsMagazine, 43(2):28–65, 2023

    2023

  40. [48]

    Springer, 2022

    Aidan Hogan, Eva Blomqvist, and Stefan Dietze et al.KnowledgeGraphs. Springer, 2022

    2022

  41. [49]

    Survey of hallucination in natural language generation.ACM ComputingSurveys, 55(12):1–38, 2023

    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 ComputingSurveys, 55(12):1–38, 2023

    2023

  42. [50]

    Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan

    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? InInternationalConferenceon Learning Representations, 2024.https://arxiv.org/abs/2310.06770

    2024 arXiv

  43. [51]

    Littman, and Anthony R

    Leslie Pack Kaelbling, Michael L. Littman, and Anthony R. Cassandra. Planning and acting in partially observable stochastic domains.ArtificialIntelligence, 101(1–2):99–134, 1998

    1998

  44. [52]

    Runtime compliance verification for AI agents, 2026

    Nafiseh Kahani, Masoud Barati, and Diana Addae. Runtime compliance verification for AI agents, 2026

    2026

  45. [53]

    Rudolf E. Kalman. A new approach to linear filtering and prediction problems.JournalofBasicEngineering, 82(1):35– 45, 1960

    1960

  46. [54]

    Devanbu, and Caleb Stanford

    Parnian Shabani Kamran, Premkumar T. Devanbu, and Caleb Stanford. Vision paper: Proof-carrying code com- pletions. In Proceedingsof the39thIEEE/ACM InternationalConferenceon AutomatedSoftwareEngineering Workshops, pages 35–42. ACM, 2024

    2024

  47. [55]

    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

    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, ne...

    2022 arXiv

  48. [56]

    AgentGuard: Runtime verification of AI agents, 2025

    Roham Koohestani. AgentGuard: Runtime verification of AI agents, 2025. Accepted at the Agentic Software Engi- neering workshop, ASE 2025

    2025

  49. [57]

    Shuvendu K. Lahiri. Evaluating LLM-driven user-intent formalization for verification-aware languages. In Proceedingsof the24thConferenceon FormalMethodsin ComputerAidedDesign, 2024

    2024

  50. [58]

    Shuvendu K. Lahiri. Intent formalization: A grand challenge for reliable coding in the age of AI agents, 2026

    2026

  51. [59]

    A brief account of runtime verification.Journalof Logic andAlgebraic Programming, 78(5):293–303, 2009

    Martin Leucker and Christian Schallhart. A brief account of runtime verification.Journalof Logic andAlgebraic Programming, 78(5):293–303, 2009

    2009

  52. [60]

    Retrieval-augmented generation for knowledge-intensive NLP tasks

    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. InAdvancesin NeuralIn...

    2020

  53. [61]

    Agent harness engineering: A survey, 2026

    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 Krish- naswamy, Jun Huan, and Chandan Reddy. Agent harness engine...

    2026

  54. [62]

    API-Bank: A benchmark for tool-augmented LLMs, 2023.https://arxiv.org/abs/2304.08244

    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

    2023 arXiv

  55. [63]

    Liang, Melissa Lin, Nikitha Rao, and Brad A

    Jenny T. Liang, Melissa Lin, Nikitha Rao, and Brad A. Myers. Prompts are programs too! understanding how devel- opers build software containing prompts.Proc. ACM Softw.Eng., 2(FSE):1591–1614, 2025

    2025

  56. [64]

    Edit automata: Enforcement mechanisms for run-time security policies

    Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run-time security policies. InternationalJournalof InformationSecurity, 4(1–2):2–16, 2005

    2005

  57. [65]

    AgentBench: Evaluating LLMs as agents, 2023.https://arxiv

    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:...

    2023 arXiv

  58. [66]

    McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer

    Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms.ComputerScience Review, 5(2):119–161, 2011

    2011

  59. [67]

    PROV-DM: The PROV data model

    Luc Moreau and Paolo Missier. PROV-DM: The PROV data model. W3C Recommendation,https://www.w3.org/TR/ prov-dm/, 2013

    2013

  60. [68]

    George C. Necula. Proof-carrying code. In Proceedingsof the24th ACM SIGPLAN-SIGACT Symposium on Principlesof Programming Languages, pages 106–119. ACM Press, 1997

    1997

  61. [69]

    eXtensible Access Control Markup Language (XACML) version 3.0

    OASIS. eXtensible Access Control Markup Language (XACML) version 3.0. OASIS Standard, 2013

    2013

  62. [70]

    Abstract interpretation-based feature im- portance for support vector machines

    Abhinandan Pal, Francesco Ranzato, Caterina Urban, and Marco Zanella. Abstract interpretation-based feature im- portance for support vector machines. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors,Verification, Model Checking, and AbstractInterpretation- 25th Inte...

    2024

  63. [71]

    Patil, Tianjun Zhang, Xin Wang, and Joseph E

    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

    2023 arXiv

  64. [72]

    Harvard University Press, Cambridge, MA, 1931–1935

    Charles Sanders Peirce.CollectedPapers of CharlesSandersPeirce. Harvard University Press, Cambridge, MA, 1931–1935. Edited by Charles Hartshorne and Paul Weiss

    1931

  65. [73]

    Acar, James Cheney, and Paul Blain Levy

    Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. Functional programs that explain their work. In Proceedingsofthe17thACM SIGPLAN InternationalConferenceonFunctionalProgramming (ICFP), pages 365–376. ACM, 2012

    2012

  66. [74]

    Fabio Petroni, Tim Rocktäschel, Sebastian Riedel, Patrick Lewis, Anton Bakhtin, Yuxiang Wu, and Alexander Miller. Language models as knowledge bases? InProceedingsof the2019 Conferenceon EmpiricalMethodsin Natural LanguageProcessingandthe9thInternationalJointConferenceonNatura...

    2019

  67. [75]

    Propagation of interval belief structures and imprecise copulas for neural network verification, 2026

    Francesc Pifarre-Esquerda, Éric Goubault, and Sylvie Putot. Propagation of interval belief structures and imprecise copulas for neural network verification, 2026

    2026

  68. [76]

    Springer, 1989

    Wolfram Pohlers.Proof theory: anintroduction. Springer, 1989

    1989

  69. [77]

    Reflections on random kitchen sinks

    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

    2017

  70. [78]

    Ramadge and W

    Peter J. Ramadge and W. Murray Wonham. Supervisory control of a class of discrete event processes.SIAM Journal on ControlandOptimization, 25(1):206–230, 1987

    1987

  71. [79]

    Measuring attribution in natural language generation models

    Hannah Rashkin, Vitaly Nikolaev, Matthew Lamm, Lora Aroyo, Michael Collins, Dipanjan Das, Slav Petrov, Gau- rav Singh Tomar, Iulia Turc, and David Reitter. Measuring attribution in natural language generation models. ComputationalLinguistics, 49(4), 2023

    2023

  72. [80]

    Rawlings, David Q

    James B. Rawlings, David Q. Mayne, and Moritz M. Diehl. ModelPredictiveControl:Theory,Computation,and Design. Nob Hill Publishing, 2 edition, 2017.https://sites.engineering.ucsb.edu/~jbraw/mpc/

    2017

  73. [81]

    Epistemic logic

    Rasmus Rendsvig, John Symons, and Yanjing Wang. Epistemic logic. InTheStanfordEncyclopediaof Philosophy (Summer 2025 Edition),Edward N. Zaltaand Uri Nodelman (eds.), 2025. https://plato.stanford.edu/archives/ sum2025/entries/logic-epistemic/

    2025

  74. [82]

    Maddison, and Tatsunori Hashimoto

    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

    2023 arXiv

  75. [83]

    Toolformer: Language models can teach themselves to use tools

    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. InAdvances in NeuralInformationProcessingSystems, volume 36, 2023. ht...

    2023 arXiv

  76. [84]

    Formal semantics for agentic tool protocols, 2026

    Pius Schlapbach. Formal semantics for agentic tool protocols, 2026

    2026

  77. [85]

    Schneider

    Fred B. Schneider. Enforceable security policies.ACM TransactionsonInformationandSystemSecurity, 3(1):30–50, 2000

    2000

  78. [86]

    Scott and Christopher Strachey

    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

    1971

  79. [87]

    Progent: Securing AI agents with privilege control, 2025

    Tianneng Shi, Jingxuan He, Zhun Wang, Hongwei Li, Linyu Wu, Wenbo Guo, and Dawn Song. Progent: Securing AI agents with privilege control, 2025

    2025

  80. [88]

    Shoenfield.MathematicalLogic

    Joseph R. Shoenfield.MathematicalLogic. Taylor Francis, 2nd edition, 1967

    1967

  81. [89]

    Korth, and S

    Abraham Silberschatz, Henry F. Korth, and S. Sudarshan.DatabaseSystemConcepts. McGraw-Hill Education, New York, NY, 7th edition, 2020

    2020

  82. [90]

    Sontag.MathematicalControlTheory:DeterministicFiniteDimensionalSystems

    Eduardo D. Sontag.MathematicalControlTheory:DeterministicFiniteDimensionalSystems. Springer, 2 edition, 1998

    1998

  83. [91]

    Fundamental concepts in programming languages.Higher-OrderandSymbolicComputation, 13(1–2):11–49, 2000

    Christopher Strachey. Fundamental concepts in programming languages.Higher-OrderandSymbolicComputation, 13(1–2):11–49, 2000. 30 Alglave & Cousot

    2000

  84. [92]

    Sumers, Shunyu Yao, Karthik Narasimhan, and Thomas L

    Theodore R. Sumers, Shunyu Yao, Karthik Narasimhan, and Thomas L. Griffiths. Cognitive architectures for language agents, 2023.https://arxiv.org/abs/2309.02427

    2023 arXiv

  85. [93]

    A lattice theoretical fixpoint theorem and its applications.PacificJ

    Alfred Tarski. A lattice theoretical fixpoint theorem and its applications.PacificJ. of Math., 5:285–310, 1955

    1955

  86. [94]

    A review of formal methods applied to machine learning.CoRR, abs/2104.02466, 2021

    Caterina Urban and Antoine Miné. A review of formal methods applied to machine learning.CoRR, abs/2104.02466, 2021

    2021 arXiv

  87. [95]

    Static analysis by abstract interpretation against data leakage in machine learning.Sci

    Caterina Urban, Pavle Subotic, and Filip Drobnjakovic. Static analysis by abstract interpretation against data leakage in machine learning.Sci. Comput. Program., 246:103338, 2025

    2025

  88. [96]

    Springer, 2013

    Dirk van Dalen.LogicandStructure. Springer, 2013

    2013

  89. [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. InProceedingsof the63rd AnnualMeetingof theAssociationfor ComputationalLinguistics(Volume1: Long Pape...

    2025

  90. [98]

    Poskitt, and Jun Sun

    Haoyu Wang, Christopher M. Poskitt, and Jun Sun. AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents, 2025. Accepted at ICSE 2026

    2025

  91. [99]

    A survey on large language model based autonomous agents, 2023.https://arxiv.org/abs/2308.11432

    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

    2023 arXiv

  92. [100]

    Lean4Agent: Formal modeling and verification for agent workflow and trajectory, 2026

    Ruida Wang, Jerry Huang, Pengcheng Wang, Xuanqing Liu, Luyang Kong, and Tong Zhang. Lean4Agent: Formal modeling and verification for agent workflow and trajectory, 2026

    2026

  93. [101]

    Re- solving knowledge conflicts in large language models

    Yike Wang, Shangbin Feng, Heng Wang, Weijia Shi, Vidhisha Balachandran, Tianxing He, and Yulia Tsvetkov. Re- solving knowledge conflicts in large language models. InFirstConferenceon LanguageModeling, 2024

    2024

  94. [102]

    Formal-method-guided vibe coding: Closing the verification loop on AI-generated safety-critical software through model-driven engineer- ing, 2026

    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 engineer- ing, 2026

    2026

  95. [103]

    ELIZA—a computer program for the study of natural language communication between man and machine.Communicationsof theACM, 9(1):36–45, 1966

    Joseph Weizenbaum. ELIZA—a computer program for the study of natural language communication between man and machine.Communicationsof theACM, 9(1):36–45, 1966

    1966

  96. [104]

    IsolateGPT: An execution isola- tion architecture for LLM-based agentic systems

    Yuhao Wu, Franziska Roesner, Tadayoshi Kohno, Ning Zhang, and Umar Iqbal. IsolateGPT: An execution isola- tion architecture for LLM-based agentic systems. InProceedingsof theNetworkandDistributedSystem Security Symposium, 2025

    2025

  97. [105]

    Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press

    John Yang, Carlos E. Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press. SWE- agent: Agent-computer interfaces enable automated software engineering, 2024.https://arxiv.org/abs/2405.15793

    2024 arXiv

  98. [106]

    ReAct: Synergizing reasoning and acting in language models

    Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. ReAct: Synergizing reasoning and acting in language models. InInternationalConferenceon LearningRepresentations, 2023.https: //arxiv.org/abs/2210.03629

    2023 arXiv

  99. [107]

    The fusion of large language models and formal methods for trustworthy AI agents: A roadmap, 2024.https://arxiv.org/abs/2412.06512

    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

    2024 arXiv

  100. [108]

    Titzer, Heather Miller, and Phillip B

    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

    2025

  101. [109]

    Xu, Hao Zhu, Xuhui Zhou, Robert Lo, Abishek Sridhar, Xianyi Cheng, Yonatan Bisk, Daniel Fried, Uri Alon, and Graham Neubig

    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

    2023 arXiv

  102. [110]

    MIT press, 2026 (to appear).https://mitpress.mit

    Paul Égré and Lorenzo Rossi (eds.).Handbookof TrivalentLogics. 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...

    2026

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.