Paper deep dive
Agents as Software: A Programming Languages Agenda for Agent Reliability
Shraddha Barke, Adithya Murali
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 9/29/2026, 1:20:50 PM
Summary
This paper proposes a programming systems perspective to improve the reliability of AI agents by treating them as programmable artifacts. It argues that agent behavior, distributed across prompts, tools, and memories, should be specified, analyzed, and monitored using formal methods. The authors outline a framework involving abstract models (event logs or state), logics for specifications (permission, belief, temporal), and atomic predicates, supported by static analysis, runtime monitoring, and post-execution repair.
Entities (9)
Relation Signals (7)
Shraddha Barke â affiliatedwith â Microsoft Research
confidence 99% ¡ Shraddha Barke Microsoft Research Redmond, USA
Adithya Murali â affiliatedwith â University of Wisconsin-Madison
confidence 99% ¡ Adithya Murali University of Wisconsin-Madison Madison, USA
Programming Systems Perspective â aimstoimprove â Agent Reliability
confidence 95% ¡ This essay argues that a programming-systems perspective offers a natural lens for making agents reliable.
AI Agents â modeledas â Programmable Artifacts
confidence 95% ¡ We recast agents as programmable artifacts whose behavior can be specified over traces and state
Static Analysis â analyzes â Prompts
confidence 90% ¡ Static analysis techniques treat prompts, plans, tool schemas... as analyzable objects before deployment
Runtime Monitoring â checks â execution traces
confidence 90% ¡ Dynamic analysis complements these checks by tracking what actually happens during execution... a runtime monitor can check whether actions are grounded
Event Logs â usedfor â Specification Verification
confidence 85% ¡ We propose that agentic executions can be abstracted into a log of âeventsâ... specifications are stated in some logic
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:AI agents increasingly resemble software systems: they call tools, remember facts, follow policies, delegate work, and take actions with real consequences. % Yet the ``program'' of an agent is scattered across prompts, tools, memories, workflows, and execution traces, making its behavior difficult to inspect through ordinary testing and debugging alone. % This essay argues that a programming-systems perspective offers a natural lens for making agents reliable. % We recast agents as programmable artifacts whose behavior can be specified over traces and state, checked before deployment, monitored during execution, and improved from observed failures. % The goal is not to make probabilistic agents behave like deterministic programs, but to give them enough structure that their behavior can be reasoned about, controlled, and repaired.
Tags
Links
- Source: https://arxiv.org/abs/2609.32198v1
- Canonical: https://arxiv.org/abs/2609.32198v1
Trouble viewing inline? Open PDF directly â
Full Text
64,527 characters extracted from source content.
Expand or collapse full text
Agents as Software: A Programming Languages Agenda for Agent Reliability Shraddha Barke Microsoft Research Redmond, USA sbarke@microsoft.com Adithya Murali University of Wisconsin-Madison Madison, USA adithyamurali@cs.wisc.edu Abstract AI agents increasingly resemble software systems: they call tools, remember facts, follow policies, delegate work, and take actions with real consequences. Yet the âprogramâ of an agent is scattered across prompts, tools, memories, work- flows, and execution traces, making its behavior difficult to inspect through ordinary testing and debugging alone. This essay argues that a programming-systems perspective offers a natural lens for making agents reliable. We recast agents as programmable artifacts whose behavior can be specified over traces and state, checked before deployment, monitored during execution, and improved from observed failures. The goal is not to make probabilistic agents behave like determin- istic programs, but to give them enough structure that their behavior can be reasoned about, controlled, and repaired. CCS Concepts:⢠Software and its engineeringâFor- mal methods;⢠Computing methodologiesâIntelligent agents. Keywords: agent reliability, specifications, logics for agents, static and dynamic analysis, agent verification ACM Reference Format: Shraddha Barke and Adithya Murali. 2026. Agents as Software: A Programming Languages Agenda for Agent Reliability. In Proceed- ings of the 2026 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward! â26), October 4â9, 2026, Oakland, CA, USA. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3840586.3843744 1 Introduction AI agents are emerging as the next major abstraction in soft- ware engineering: systems capable of reasoning over natural language and acting through software interfaces. Agents can be viewed as probabilistic microservices: modular enti- ties that perform specialized tasks, but with underspecified constraints and inherent randomness. Unlike deterministic This work is licensed under a Creative Commons Attribution 4.0 Interna- tional License. Onward! â26, Oakland, CA, USA Š 2026 Copyright held by the owner/author(s). ACM ISBN 979-8-4007-2934-8/2026/10 https://doi.org/10.1145/3840586.3843744 software systems, agents operate in dynamic, uncertain en- vironments, interpreting ambiguous user intent while taking actions that may have real-world side effects. From a pro- gramming languages perspective, the central shift is that the agentâs âprogramâ is no longer contained in a single body of source code. Its behavior is distributed across prompts, tools, memories, policies, plans, traces, and orchestration logic. Agents are therefore programmable systems, but their pro- gramming model is implicit, probabilistic, and only partially specified. This makes conventional testing and debugging inadequate. Ensuring the correctness and reliability of such systems therefore demands a new discipline for specifying, analyz- ing, monitoring, and improving agent behavior. This pa- per argues for a programming languages view of AI agents. Rather than treating agents as opaque wrappers around lan- guage models, we view them as software artifacts whose distributed behavior can be studied using the tools of pro- gramming languages, formal methods, runtime verification, and neuro-symbolic reasoning. This view starts with defining specifications for agents. Specifications can describe what counts as valid behavior over event logs, state abstractions, permissions, information flow, tool preconditions, belief up- dates, and resource usage. They can express familiar software properties, such as type correctness, resource discipline, and authorization, while also capturing agent-specific concerns such as grounded belief, stale evidence, tool-use justification, and recoverability after failure. Of course, specifications must also be connected to analy- ses that operate before, during, and after execution. Static analysis techniques treat prompts, plans, tool schemas, mem- ory policies, and configuration artifacts as analyzable objects before deployment, checking whether the agent is struc- turally capable of reliable behavior. This includes checking for ambiguous obligations, invalid data and tool flows, and high-impact actions that become reachable before their re- quired evidence has been established. Dynamic analysis complements these checks by tracking what actually happens during execution. By maintaining an evolving state of goals, tool outputs, evidence, permis- sions, obligations, and constraints, a runtime monitor can check whether actions are grounded, beliefs remain valid, irreversible operations are authorized, and global trace prop- erties continue to hold. Finally, execution traces can become arXiv:2609.32198v1 [cs.PL] 26 Sep 2026 Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali material for learning better specifications, repairing work- flows, optimizing tool use, and evolving agents as their en- vironments change. In this sense, agent reliability is not a single verification problem, but an ongoing systems problem: how to design agents that can be checked before execution, monitored during execution, and improved after execution. The goal is not to eliminate the probabilistic nature of agents, but to make their behavior more explicit, inspectable, and governable. Determinism is not the goal: sampling is an im- plementation mechanism, in the way a thread scheduler or a garbage collector is, and software has long presented pre- dictable interfaces over such mechanisms by constraining what they are allowed to do rather than by making them deterministic. Much of what follows is not agent-specific: these ideas are well established in programming languages and systems re- search, and should be adapted rather than reinvented. Three assumptions, however, do not carry over cleanly. First, the artifact being analyzed is not necessarily fixed before exe- cution: an agent may revise its memory, plans, instructions, or generated code in ways that alter its subsequent behav- ior. Second, atomic predicates need not have deterministic interpretations: whether food is rotten, for example, may be decided by a fallible model rather than a fixed procedure. Third, an execution need not admit a canonical abstraction: the same run may be projected into several event logs, and monitors over those logs may disagree on whether the spec- ification was violated. The rest of this paper develops this perspective. Section 2 discusses specifications for AI agents, including abstract mod- els of agentic computation, logics for stating agent proper- ties, domain-specific predicates expressed through natural language or neuro-symbolic mechanisms, and the role of language design in making such specifications easier to en- force. Section 3 then turns to static and dynamic analysis, showing how prompts, tools, memory, retrieval, and execu- tion traces can be checked for reliability properties. Figure 1 summarizes how the pieces fit together. 2 Specifications for AI Agents A science of reliability must start with a discussion of risks, and the specifications that we can enforce to mitigate them: What do we want to prevent agentic systems from doing? How do we formulate good behavior? In this section, we will essentially stay close to the classi- cal programming languages understanding of bad behavior in software: memory mishandling, permission violations, leaked secrets, inputs/outputs of the wrong type, functional incorrectness, etc, which can be defined as computational problems. There is a significant body of literature on "harms" that AI systems can perpetuate that is centered more on hu- manistic and social concerns [27,41,48]. While some of these harms may be expressible as formal specifications (e.g., pri- vacy or fairness), this is not true in general (e.g., preventing generation of graphic images, whatever that may mean in a specific cultural context). Additionally, we will dedicate our discussion to the problem of stating formal specifications and leave the discussion of how they may be enforced to later sections. We conceive the science of specifications for agents as con- sisting of three pieces: (1) an abstract model that formalizes agentic computation, (2) a compositional logic that specifies the family of properties we wish to state â such that the formulas in the logic can be interpreted over the chosen ab- stract model, and (3) a set of atomic functions and predicates that encapsulate useful aspects of the domain at hand and over which the specification formulas will be written. Formalizing Specifications. The first step towards for- malizing specifications is to define a formal computational model of agents. One can then use various logics, languages, and calculi to express specifications over the abstract model. We observe that agentic frameworks are closer to systems software, since their computation is often best understood as an open-ended process consisting of individual atomic steps. Agentic frameworks also feature complex concurrency, delegation protocols, and reactivity in their design, which reinforces the aptness of this comparison. In this spirit, we propose that agentic executions can be abstracted into a log of âeventsâ. The vocabulary of the events tracked in the agentsâ computation provides a specific abstraction, since two agents that are indistinguishable at the level of a par- ticular event vocabulary would satisfy the same properties. Therefore, the choice of what events must be logged can be left up to the designer of the verification infrastructure (human or otherwise). In this essay, we do not take a position on specific mod- eling choices, such as choosing between action-based and state-based formalisms [16,17,23,32]. At the time of writing this essay, popular discussions on agent reliability tend to exemplify specifications that are more naturally stated over state-like abstractions, e.g., permission tokens for access- ing files, resource invariants (like number of sub-agents al- lowed), or well-typed-ness of values. State-based formalisms like TLA+ [23,24] also offer robust tool support for work- ing with such specifications, and can therefore be a more attractive choice if applicable. However, it may be difficult to commit to purely state-based formalisms for dynamic agents, since agents can decompose tasks in different ways and may not admit a single cohesive abstract state that captures an agentâs execution. For example, consider a code agent that spawns sub-agents to refactor related functionality in a code repository into one or more functions. The sub-agents may traverse and modify the repository in different orders, mak- ing it difficult to identify a single abstract state invariant that should hold across all intermediate executions. In contrast, Agents as Software: A Programming Languages Agenda for Agent ReliabilityOnward! â26, October 4â9, 2026, Oakland, CA, USA The agentâs âprogramâ System prompt & task instructions Tool schemas & contracts Memory & retrieval policy Permissions & capabilities Orchestration & delegation Formal layer (§2) Abstraction mechanism concrete executionâŚâevent log itself a formal object Abstract model events, state, resources, threads Logic LTL, epistemic, permission, provenance, hyperproperties Atoms arithmetic, types, and natural-language predicates Analyses (§3) Before: static analysis Is the configuration capable of reliable behavior? Ambiguous obligations, unguarded high-impact actions, unsatisfiable dataflow. During: runtime monitoring Is this action justified by the trace prefix? Evidence, freshness, temporal guards, global invariants. After: mining & repair What did the failures reveal that the specification did not say? Candidate guards and invariants. abstract check against feedback: mined specifications, repaired prompts, tightened contracts Figure 1. The programming-systems view of an agent. The agentâs âprogramâ (left) is distributed across artifacts in different languages, some of which are written during execution. An abstraction mechanism lifts concrete executions into event traces, over which specifications are stated in some logic and vocabulary of atoms (middle). Analyses (right) consume these before, during, and after execution, and what they observe is fed back into the artifacts. modeling the changes as an event log where agents com- mit changes they make to the log, respecting function call order or other hierarchies in the code can be more useful. Action-based formalisms can therefore offer better support for stating and composing higher-level coordination specifi- cations for complex agent workflows. Unsurprisingly, some emerging works on agentic specifi- cations advocate for adopting an event-based abstraction of execution behavior [22,47]. Many of these works predom- inantly focus on violations involving improper actions in certain states/environments (e.g., improper tool use) [19,22, 30,35,47], and agents are therefore modeled as executing a sequence of well-defined (and often predefined) actions. They then utilize the boundaries between LLMs and tools or initial/terminal points to define events, e.g., after an action has been completed by an agent, or when a tool communi- cates a result. There is a richer space of modeling choices for such ab- stractions. For instance, one can model tools and the re- sources at an agentâs disposal and define stringent interfaces between different agents and tools. One can explicitly model memory and have a vocabulary over memory stores and ac- cesses performed by agents, or model the environment and use vocabulary over the environmentâs responses. Another natural extension is to have a formal model that distinguishes sub-agents with their own virtual âthreadâ. One interesting realization of this model is to require certain events to be committed to a concrete log, potentially in the middle of an agentâs execution. A subtlety that can arise with event-based abstractionsâ as opposed to formalisms that only model agent-tool-human boundariesâ is that we are no longer guaranteed that a given concrete trace can only be mapped on to a single abstract trace. For example, consider an abstraction that records an acquire(agent_id,í)and arelease(agent_id,í)for a resource í, with the specification being that a resource cannot be ac- quired twice without being released in the middle. Now con- sider a trace where an agent delegates a sub-agent to operate on a resource it acquired. Depending on how the trace is abstracted, one may record the release of the resource by the parent agent either before the sub-agent begins or after the sub-agentâs execution has finished. Not only are these distinct abstractions, but one of them satisfies the specifi- cation while the other does not! Therefore, the abstraction mechanism for lifting real executions to abstract traces must be carefully defined (and treated as a formal object in its own right) when working with richer abstract models. Finally, we observe that an event log-based view is only an abstraction and inherits the weaknesses of incompleteness that plagues any abstraction mechanism. For example, given a vocabulary consisting of sending and receiving emails, an agent may respect the specification âread email from ABCâ send response to ABC if ABC is not a no-reply addressâ by behaving as follows: âread emailâleak passwordâsend emailâ. The password leak will not be detected by a mech- anism enforcing the given specification. This is obviously because we havenât even modeled that leaking passwords is bad. One can mitigate such issues to some extent by using other specification frameworks that attempt to model the en- vironment explicitly and prevent certain actions outright, or using a default-restrictive as opposed to a default-permissive modelâ meaning that any actions beyond benign ones must Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali be modeled explicitly to be allowed. An interesting spin on this approach is the idea of âcapability permissionsâ, which are permission resources that allow an agent to only ex- hibit certain classes of capabilities. For instance, in the above example, one can say that no actions beyond reading and responding to emails are allowed. A system enforcing such a specification can then flag the password leak as being outside the scope of capabilities allowed for the agent. More gener- ally, a security-oriented treatment of agentic reliability may need to consider more involved abstraction and specification mechanisms. We do not investigate this further in this essay. Logics for Agentic Specifications. Once we fix an ab- stract model, we can express specifications as logical formu- las that are evaluated over the model. There are abundantly many choices here. In our view, the key concerns are not raw expressiveness or elegance from a purely specification per- spective: anyone who simply wants to convey a property can do so in plain English, and if someone knows how a property can be checked they can simply encode that check directly as a program over the model. Instead, the considerations are more about the algorithmic toolkit associated with the logics. Different logics vary in their support for automated deduc- tion, the complexity of deciding whether a property holds, and the extent to which specifications can be composed. We discuss some techniques for static and dynamic analysis for various classes of properties in later sections. Table 1 illustrates an assortment of properties that one may wish to employ for describing reliable behavior in agents. Many of these are of course familiar to readers acquainted with verification and testing of systems software. Among these, the class of resource and permission-based specifi- cations appears to be the most interesting and immediate challenge to tackle. Since agents require complex coordina- tion and utilize dynamic delegation to divide tasks, reasoning about whether an individual agent instance has permission to access/modify a resource or call a tool, and in particular being able to maintain such reasoning across an unbounded trace by monitoring provenance of permission tokens ap- pears to be a challenging and useful problem for coordinating agents at scale. An interesting class of properties that is less explored in contemporary literature is knowledge and belief logics. One of the most attractive aspects of learning-based systems is their ability to act under incomplete information based on learned knowledge of the domain, and therefore one of the risks is that an agent acts on knowledge it does not actually have, or on beliefs that may be contradicted by subsequent evidence. This class of specifications is slightly different from the kinds of permission specifications discussed above. Rather, they pertain to whether the agent knew or justifiably believed something at a particular point. We showcase sev- eral interesting variations on such specifications in Table 1. The simplest example is a grounded-belief specification, which asks that any belief acted upon must be derivable from the agentâs observable history (whether that means the con- text, the memory, or perhaps tool outputs) and blocking ac- tions which cannot be justified in this manner. As we discuss later under evidence-grounded tool use in Section 3.2, this kind of specification can be monitored dynamically by check- ing whether a proposed action is justified by facts derivable from the current trace prefix. A revision-consistent speci- fication requires the agent not to act on a belief once later evidence in the same trace has contradicted it. This blocks the failure mode where an agent latches onto an early con- clusion and ignores subsequent evidence. A coordination specification, in the multi-agent setting, asks that two agents not jointly commit to a plan unless each knows the plan and each knows the other knows it, blocking handoff failures where a planner and an executor disconnect. Each of these scenarios corresponds to concrete logics studied in the litera- ture. Utilizing the language of knowledge and belief within a formal system to reason about agentsâ actions is a promising avenue for future work. Atoms. The final piece in writing specifications is the set of atomic concepts, such as functions and predicates, that are determined by the domain of interest. On one end, one can use standard mathematical and logical domains: integers or reals with arithmetic operators, sets and maps, booleans, and so on. On the other end, we can simply choose to express atomic concepts in natural language, e.g. âbusy intersectionâ, which can be used to specify safe behavior of an autonomous vehicle, or ârotten foodâ, which can be used in the context of a cooking agent. Recent work in this area allows users to specify a gen- eral set of predicates in natural language and automates checking them either by prompting LLMs to evaluate these predicates on traces in a wholesale manner, or by asking LLMs to write Boolean programs (derived from the modelsâ internal knowledge about the domain) which implement the predicate [18,47]. An interesting middle ground here has been explored by prior work on neuro-symbolic pro- gramming where neural âmodulesâ capturing e.g., whether an image is that of a cat, are composed with programmatic or logical combinators [2,28,29,33,43]. Such frameworks offer the ability to enforce type systems on expressions in the language, learning distribution-specific semantics, and differentiable reasoning. However, what remains underdeveloped is a formal ac- count of natural-language theories: collections of predicates specified in natural language, evaluated by learned models, and connected by explicit relations such as implication, in- compatibility, and revision. This problem has clear predeces- sors. Cyc encoded commonsense knowledge as axioms [25]; ontology engineering developed shared vocabularies [14]; Agents as Software: A Programming Languages Agenda for Agent ReliabilityOnward! â26, October 4â9, 2026, Oakland, CA, USA Table 1. An example set of agent specifications, varied by specification purpose and type of logic that may be used to express the property. The Usage column notes whether these properties are typically found in a survey of related work on agent reliability (R), were not found in related work by the authors verbatim but are essentially natural extensions of those currently used (B as in Boundary), or are speculated by the authors (S). Spec exampleProperty kindLogicUsage Tool inputs/outputs must satisfy the given pre/post- condition Interface correctnessFOLR EveryAcquire(r)must have a matching Release(r) later before another Acquire(r) Resource well-formednessRegexes over trace vocabularyR Cannot issuedelete_resource(r)without prior Owns(agent, r) in session Action admissibilityLTLR Order retrieval must be preceded by an authentica- tion of the corresponding customer Action admissibilityLTLR confirmation_token argument equals token from prior request_confirmation; not reused Input integrity (freshness / use-once) Session typesR Capabilities held by subagentâcapabilities held by parent at spawn Permission disciplinePermission LogicsR No use of a capability after its Revoke eventPermission disciplineLTLR NoSend_external(m)wheremderives from a confidential-labeled source Information-flow (label- based) Information flow types/logicsR Output independent of content from demarcated potential junk source Counterfactual prop- erty/Hyperproperty HyperLTL or similar logicsB No tool invocation with arguments derived from untrusted data without calling validate Value provenanceFOL/Gradual Types/Provenance LogicsB Every output supported by a corresponding appro- priate Source Output faithfulness (anti- hallucination) Provenance logicsB Tool call expenditures within remaining budgetQuantitative Trace logics with counting/Arithmetic constraints R Probability of reaching unsafe state ⤠íQuantitative + SafetyPCTL / probabilistic LTLR Secret input and observable output share ⤠í bitsQuantitativeFOL with ArithmeticB Every irreversible action (e.g., tool call) is derivable from the action set of an Authorized_Plan(p) Plan-coherence/ provenanceLTL + Provenance/Permission logicsB Before any irreversible action, the agentâs belief in the justification for the action is derivable from prior plans in the trace Beliefs and JustificationEpistemic logicsB/S No subagent acting for userí˘reads data labeled for user í˘ â˛ â í˘ Data security/Access man- agement FOL/Permission logicsB Subagents spawned in disjoint scopes do not share resources Access managementResource logics e.g., separation logicB/S Events measured over user-level time (e.g., must produce result within wall-clock í seconds) Realtime propertiesTimed logicsB An agent does not continue to hold a belief after it has seen evidence to contradict the belief Belief consistencyDynamic Epistemic logicsS Cooperating subagents must have mutual knowl- edge of a shared plan Multi-agent coordinationEpistemic logics over multiple partiesS description logics identified decidable fragments [3]; the Se- mantic Web extended these ideas to the open web [38]; Wiki- data curated knowledge at scale [46]; and Wikifunctions now pursues their composable-function counterpart [13]. These efforts provide much of the representational machinery we need. New work should therefore reuse existing formalisms and vocabularies. Language models change the economics: predicates are now cheap to evaluate but difficult to trust. There are three aspects of such theories that remain to be developed. First, one can investigate different kinds of natu- ral language theories and how they may be formalized. For example, consider a predicatebusy_intersection(ííí). This predicate has a highly contextual interpretation: what it means for an intersection to be busy during work traffic is not the same as what it means at 2 a.m., and the meaning may also differ depending on whether the intersection is in a large city or a small town. One way to formalize such a predicate is to treat its meaning as context-dependent rather than fixed. For instance,busy_intersectionmay be interpreted proba- bilistically, together with a complement predicatenot_busy, so that their probabilities sum to one. Alternatively, its se- mantics may be expressed in terms of confidence, possibility, or defeasible rules that can be revised when new evidence becomes available. We are not aware of a general framework Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali that integrates these reasoning mechanisms over fallible learned predicates. Another aspect of these natural language theories is how various predicates may be related to each other, including any (hard or soft) entailments between them [8]. For ex- ample, one would presumably wantbusy_intersectionto en- tailyield_before_turn, or wantrotten_foodto be incompat- ible withsafe_to_eat. This is also the point where mecha- nisms whose combinators are fixed a prioriâincluding logic programmingâcan find limitations, since there are innumer- able ways to restate the same concept and natural language predicates can be related to each other in tricky ways. We also know of no work that provides a well-considered formal footing for recording these entailments. Finally, developing standalone solvers for interesting and useful natural theories that can also be combined into larger reasoning mechanisms is an area that is completely unexplored. The ideal goal here is to develop abstract mechanisms for designing natural language theories with associated recipes for defining the collection of predicate signatures involved, the kinds of entailments or other relationships between them, and algorithms that can perform reasoning modulo these theories. We imagine this line of research to be similar to designing type systems, where related reasoning patterns are abstracted into higher level logical categories with associated reasoning algorithms. A careful study of natural language theories is thus fertile ground for future work and would greatly benefit the science of agent reliability. We conclude this section with a brief note on designing languages for reliable agent engineering. The Role of Language Design. Many specifications de- scribed above can be thought of as enforcing certain disci- plines in agentic execution at an algorithmic level, in the sense that the specifications can already be stated at the level of the vocabulary of the task and/or agent orchestra- tion. Therefore, it is useful to explore prompt- and agent- programming languages that provide rich interfaces for inte- grating data types, permissions, and other reliability artifacts, such as test cases, into the specification of agent workflows. Designing such languages, as with traditional programming languages, can reduce the burden of checking for certain properties during execution. This is essentially the âcorrect- by-constructionâ position on engineering reliability. The technical questions in this area arise at two levels. First, there are higher-level choices about the harnesses within which agents are deployed: whether agents are treated as relatively free actors, or whether they are only used to generate code that ultimately acts on their behalf after be- ing subjected to formal verification [30,35]. Second, there are design choices about the language abstractions used to write agents themselves: differing in the styles of traditional programming languages they choose to adopt or extend, their support for control flow, parallelization, or exposure to lower-level systems knobs for controlling LLMs (like con- text window, temperature, low-level prompting or decoding strategies) within the language, and their use of different constraint mechanisms for eliciting specific outputs from language models [1, 6, 12, 21, 31, 44, 51]. 3 Program Analysis for Agent Reliability The previous section described how agent behavior can be specified over abstract models, logics, and domain-specific predicates. We now ask how such specifications can be used to improve reliability. We separate analysis along the execu- tion boundary: static and dynamic analysis. Together, these analyses support reliability before and during execution, while traces provide feedback for improving future agent behavior. 3.1 Static Analysis Static analysis checks the artifacts that exist before an agent runs: prompts, tool schemas, policies, memory and retrieval configurations, and workflow structure. Its goal is to identify configurations that permit unreliable behavior before they are deployed [4, 9, 34, 39]. Agent Configurations as Static Artifacts. Static anal- ysis for agents provides a way to reason about whether an agent is configured to behave reliably before it is executed. Unlike a conventional single-program artifact, agentic be- havior is distributed across prompts, tool schemas, policies, memory, and orchestration logic. Static analysis treats these configuration artifacts as the objects to be checked. The goal is not to predict the agentâs exact execution path, but to check whether the system has been set up in a way that makes reliable execution more likely: are the instructions clear, are tool preconditions stated, are dangerous actions properly guarded, are data dependencies satisfiable, and can the available tools support the intended workflow? A prompt, a tool schema, a retrieval policy, or a memory rule may each appear individually harmless, but their interaction can also cause failures. For example, a prompt may instruct the agent to issue refunds, while the available tools do not expose whether a returned item has actually been received. Simi- larly, a workflow may require user confirmation before an irreversible action, but the prompt may never state when such confirmation is required. Static analysis makes these gaps visible before the agent is deployed. Prompts as Interfaces. Prompts are the most visible con- figuration artifact in an agentic system, but they should not be treated as isolated text. A prompt functions like an inter- face between the task, the model, the available tools, and the surrounding control policy. Static analysis of prompts should therefore ask whether the prompt states the obliga- tions needed for reliable execution: which instructions are trusted, when the agent should ask for clarification, when it Agents as Software: A Programming Languages Agenda for Agent ReliabilityOnward! â26, October 4â9, 2026, Oakland, CA, USA should call a tool, when it should stop or escalate, whether irreversible actions require confirmation, and what output format downstream components expect [36, 40, 52]. This makes prompt analysis less about stylistic prompt engineering and more about making prompts checkable. Am- biguous directives such as âresolve the issueâ or âfetch rel- evant dataâ are risky because they leave critical decisions underspecified: what evidence is sufficient, which tools may be used, what constraints must be preserved, and what ac- tions require approval. A static checker can flag missing placeholders, contradictory prompt sections, underspeci- fied escalation rules, and outputs that do not conform to the JSON schema, DSL, or intermediate representation ex- pected by downstream components. In this sense, prompts become closer to executable interfaces: they expose obliga- tions that can be checked against tools, policies, and work- flows. This mirrors a familiar pattern from program synthe- sis and compiler analysis, where partial programs, sketches, specifications, and intermediate representations are analyzed before execution to rule out ill-formed or unsafe comple- tions [15, 42]. Tool and Workflow Validation. Prompts describe what the agent should do, while tool schemas and tool-use work- flows describe what actions are available and when those actions are valid. Here, a tool-use workflow means the in- tended structure of an agent task: which tools may be called, what facts must be established before each call, and which actions require confirmation or authorization. The goal of static analysis would be to check whether this structure is possible and safe before the agent runs [49]. We illustrate the main checks using a refund or exchange workflow. An agent should not be able to callissue_refundmerely because the user requested a refund; the workflow should es- tablish that the order exists, the item is eligible, the return has been received, the refund amount is valid, and any required confirmation has been obtained. Ensuring this involves three related checks: local action validity, dataflow validity, and workflow reachability. The first check is local action validity. At the simplest level, the tool call proposed by the model must have the right âshapeâ: a valid tool name, required arguments, and schema-conformant values. A more com- plex requirement would be similar to refinement types [45], which can go beyond shape, e.g.,amount > 0andamount <= order_total(order_id). More advanced checks could involve looking at effects: reading a state or constructing an internal plan vs. mutating an account, contacting a user, deleting data, or moving money [35]. The second check is dataflow validity. Tool arguments should be grounded in information that the agent actually has access to: user input, prior tool responses, retrieved docu- ments, or authorized memory. A checker can flag unresolved references, hallucinated identifiers, missing dependencies, and outputs that do not match the schema expected by later steps. For example, anexchange_delivered_order_items call should be traceable to a priorget_order_detailscall that established the relevant order, items, delivery status, and available replacement options. Similarly, the analyzer can detect redundant or conflicting actions, such as workflows that make bothreturn_itemandexchange_itemreachable for the same item without a disambiguating condition. The third check is workflow reachability. A locally valid action may still be unsafe if it becomes reachable too early. For example,issue_refundmay have a validorder_idand a validamount, but it should not be reachable until the work- flow has established that the order exists, the return has been received, and the refund amount is allowed. An abstract- interpretation view is useful here: the analyzer can over- approximate possible agent states and flag paths where a high-impact action is reachable before its required evidence is available. The warning is not that a particular execution has failed, but that the configuration permits a bad execution. 3.2 Dynamic Analysis As AI agents become increasingly complex, weaving user inputs, prompts, tools, models, and memory in nontrivial ways, their reliability hinges on reasoning about behavior during execution. Static analysis alone is insufficient in these dynamic environments. Tool outputs are observed incremen- tally, user constraints may be clarified over multiple turns, memory and retrieved context may conflict with fresh obser- vations, and the external environment may change while the agent is acting. Dynamic analysis therefore complements static analysis by treating execution as an evolving semantic object, in the spirit of runtime verification, where properties are checked over observed executions [5,26]. At each step, a runtime monitor reasons over the current trace prefix: the user inputs, model decisions, tool calls, tool responses, confir- mations, retrieved evidence, and memory accesses observed so far. This prefix induces the monitorâs view of the task state and determines which actions are justified. We explain these ideas primarily through tool calls, but the same view extends to retrieval, memory, confirmations, delegation, and environment observations [37, 50]. The rest of this section decomposes dynamic analysis into a sequence of prefix-based validation questions. First, what state should the runtime monitor maintain from the execu- tion prefix? Given that state, when is a proposed tool call justified? Which observations still count as valid evidence? What obligations must be discharged before high-impact actions? What properties must hold across the accumulated trace? And when a violation occurs, can the execution still be recovered? Trace Semantics: What State Does a Runtime Monitor Maintain? Dynamic analysis runs while the agent executes a task and interacts with its environment. Its central object Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali Agent Execution Trace Step 1 tool_call(get_order_details, id: 4821) PASS Step 2 tool_call(check_return_policy, order: 4821) PASS Step 3 tool_call(issue_refund, order: 4821, amount: 127) Required: return_status == "received" Actual: return_status == "not_shipped" BLOCKED Step 4 (re-plan) tool_call(request_return_confirmation, order: 4821) SAFE re-plan Monitor State (after Step 2) Established facts: user_authenticated = true order_exists(4821) = true return_status = "not_shipped" Pending obligations: verify_return_receipt BEFORE issue_refund Precondition check for issue_refund: REQUIRED: return_status == "received" ACTUAL: return_status == "not_shipped" VERDICT: BLOCK. Obligation not discharged. Key insight. The monitor maintains a compact representation of the trace prefix: facts established so far, their provenance, constraints still in force, and unresolved obligations. For high-impact actions, the trace must show that required guards have been discharged in order; not merely that the relevant facts are present in the state. Figure 2. Runtime monitor example. The agent attempts to issue a refund (Step 3), but the monitor blocks the action because the required temporal guardverify_return_receipthas not been discharged. The agent then re-plans by first checking whether the return has been received. is not an isolated tool call, but the trace prefix that pre- cedes it. At any point in execution, this prefix contains the user constraints, tool responses, retrieved evidence, commit- ments, permissions, consumed resources, and failed actions observed so far. Together with the agentâs policies and tool contracts, this prefix determines what the agent is justified in believing and which actions it may safely take next. The runtime state is a compact representation of this pre- fix. It records the facts established so far, their provenance, the constraints still in force, and the obligations that remain unresolved. This state is updated as the agent receives user inputs, observes tool responses, retrieves evidence, makes commitments, or consumes resources. A concrete implemen- tation may separate evidence tracking from task tracking: one component records tool responses, retrieved evidence, memory entries, and provenance, while another tracks goals, constraints, subgoals, task progress, and resource use. These components enable the agent to reason about its current state and make informed decisions based on evolving context. This abstraction is necessary whenever correctness de- pends on runtime conditions. For example, in a retail task involving several purchases, the monitor may need to track the cumulative amount spent across tool invocations to en- sure that the agent remains within the userâs budget. Once the runtime monitor has constructed this state, the next ques- tion is whether a proposed tool call is justified by it [4, 47]. Evidence-Grounded Tool Use: When Is a Tool Call Jus- tified? Runtime state becomes useful when the agent is about to act. At that point, the monitor must decide whether the proposed tool call is justified by the execution prefix. Correctness is not limited to whether an individual tool call is well-formed. A tool invocation may satisfy its schema and still be unwarranted by the trace. Dynamic analysis checks whether each action is supported by the facts avail- able at that point in the execution, not merely whether the call conforms to a schema [19,47]. For example, an exchange_delivered_order_itemscall may contain all re- quired arguments but still be invalid if the agent has not established that the item was delivered, that the replacement satisfies the userâs constraints, and that the user has con- firmed the exchange. These requirements are not merely syntactic properties of the call. They are semantic dependen- cies on prior events in the trace. Similarly, if a user asks for a product with âclicky switches,â the agent must verify that a prior response has establishedswitch_type = clicky. The relevant question is not whether the agent mentioned clicky switches, but whether the trace contains trusted evidence for that claim. Dynamic analysis therefore asks whether the Agents as Software: A Programming Languages Agenda for Agent ReliabilityOnward! â26, October 4â9, 2026, Oakland, CA, USA Table 2. Analysis techniques for agent reliability, organized by phase. Static analysis checks agent configurations before execution; dynamic analysis monitors behavior during execution. Phase Analysis TechniqueWhat It ChecksArtifact / Object Static Analysis Prompt testing and analysisAre task obligations explicit? Does the prompt specify when to call tools, stop, escalate, or ask for confirmation? Prompt text Tool contract validationAre tool preconditions, effects, and required evi- dence explicit? Are high-impact actions guarded? Tool schemas Cross-artifact consistencyCan individually safe artifacts compose into un- safe behavior? Do the prompt, tools, and policies fit together, or do they create gaps where the agent can take an unsafe action? PromptĂ ToolsĂ Policy Information-flow analysisCan untrusted information influence sensitive actions without validation? Dataflow across artifacts Abstract interpretationCan an unsafe action become reachable before its required evidence, authorization, or confirmation is established? Abstract agent state Dynamic Analysis Runtime state trackingWhat facts, permissions, constraints, obligations, and provenance are established by the current execution prefix? Execution prefix Evidence-grounded checking Before a tool call, are its preconditions justified by observed evidence in the current trace state? Tool call vs. trace evidence Temporal guard checkingHave required guards been discharged in the right order? For example, authenticateâvali- dateâ confirmâ commit. Ordering over trace events Global invariant checkingDo accumulated actions over the trace sat- isfy global properties such as budgets, resource bounds, authorization, and information-flow re- strictions? Full trace preconditions of the proposed action are derivable from the current runtime state. Provenance and Freshness: Which Observations Still Count? Evidence-grounded tool use assumes that the facts in runtime state are still usable when the agent acts. This assumption can fail. Facts in an agent trace have provenance and lifetime: they come from particular sources, are observed at particular times, and may be weakened or invalidated by later events. The monitor must therefore decide whether those facts still count as valid evidence. An order retrieved early in the session may change before the agent acts on it; a memory entry may be overridden by a fresh user instruction; a retrieved document may conflict with a tool response; and a failed API call may invalidate a candidate plan. Runtime state must therefore track where a fact came from, when it was observed, and whether later events have weakened or in- validated it. For example, a calendar agent may check a userâs availability early in a conversation. If it schedules a meeting much later, the earlier availability result may no longer be re- liable. The monitor should require a fresh availability check before creating the event. Thus, dynamic analysis must treat trace observations as time-scoped evidence. Temporal Guards: What Must Happen Before High- Impact Actions? Some action preconditions are temporal: they require particular events to occur before an action is allowed. For high-impact actions with potential side ef- fects, it is not enough for the relevant facts to be present in the runtime state. The trace must also show that required guards have been discharged in the right order. These guards capture familiar ordering requirements: authenticate before account changes, validate recipients before sending confi- dential information, check availability before scheduling meetings, run tests before committing code, and obtain con- firmation before submitting an exchange. For example, an exchange_delivered_order_itemscall should not be al- lowed merely because the item is eligible and the replace- ment is valid. The trace must also contain a prior confirma- tion event, such asconfirm_exchange, before the exchange is committed. The monitor treats confirmation as a pend- ing obligation until a matchingconfirm_exchangeevent appears in the trace. Temporal guards capture ordering con- straints over individual actions, but some correctness condi- tions are not tied to a single guard. They must be checked over the accumulated trace as a whole. Global Trace Properties: What Must Hold Across the Execution? Temporal guards capture ordering constraints around individual actions, but some correctness conditions only make sense over the accumulated trace. A sequence of locally valid actions may still violate a global property. For Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali example, an agent may make several purchases that indi- vidually satisfy the tool schema but collectively exceed the userâs budget; schedule meetings that are each valid in isola- tion but overlap in time; or pass private information through a sequence of steps that eventually exposes it to an unau- thorized recipient. Dynamic analysis therefore maintains invariants over the evolving trace state, such as budget lim- its, resource bounds, compatibility constraints, authorization requirements, and information-flow restrictions. When these properties can be encoded symbolically, SMT-style checks can be used to test whether the current state remains con- sistent with the accumulated constraints [11]. For instance, a shopping agent may add items one at a time, each satis- fying the userâs local preferences, while the running total eventually exceeds the userâs budget. The runtime state must therefore maintain the accumulated cost and reject any next purchase that violates the budget constraint. Recoverability and Feedback: What Happens After a Violation? A runtime violation need not mean that the exe- cution has failed outright. Some violations are wrong turns: the agent relied on stale data, skipped a confirmation, chose an incompatible item, or followed a plan invalidated by a failed tool call. In these cases, the monitor can still steer the execution back onto a valid path by blocking the next action, asking for missing evidence, refreshing state, or triggering replanning. Other violations cross a point of no return. Once an email has been sent, an order submitted, private informa- tion disclosed, or a destructive operation committed, later steps cannot simply repair the trace. This distinction matters because recoverable violations call for repair or replanning, while unrecoverable violations call for aborting, escalating, or restarting. Violations are also useful beyond the current execution. Repeated failures show where the agentâs specifi- cation is incomplete. A missing confirmation check, a stale memory lookup, or an unsafe path to a high-impact tool is not just an execution error; it is evidence that the prompt, tool interface or memory policy failed to encode a needed constraint. In this way, runtime feedback can support spec- ification mining: successful executions, failed traces, doc- umentation, and human feedback can be used to propose candidate preconditions, temporal guards, data dependen- cies, and invariants for a domain. These mined specifications are not ground truth, but they provide candidates that can be reviewed and promoted into prompts, tool contracts, runtime monitors, and regression tests. Runtime monitoring, recov- ery, and specification revision together form a feedback loop related to the MonitorâAnalyzeâPlanâExecute over Knowl- edge (MAPE-K) architecture from autonomic computing [20] and its broader development in self-adaptive systems [7,10]. In our setting, the knowledge component includes an incom- plete specification that may itself be revised in response to observed failures. 4 Conclusion In this essay, we argued for the conception of AI agents as software systems from a programming languages perspec- tive: structured, composable units with clear functional roles that can be analyzed, tested, and verified. We then described an agenda involving the expression of clear specifications written over well-defined formal models of agentic execu- tions and involving new and complex specification logics. We further described a variety of static and dynamic enforce- ment methodologies for various classes of specifications, and discussed the nuances involved in designing such algorithms. Our hope is that this essay acts as a sound starting point for the community to develop a rich agenda on reliability for AI agents. References [1]Soufiane Amini, Yassine Benajiba, Cesare Bernardis, Paul Cayet, Hassan Chafi, Abderrahim Fathan, Louis Faucon, Damien Hilloulin, Sungpack Hong, Ingo Kossyk, Tran Minh Son Le, Rhicheek Pa- tra, Sujith Ravi, Jonas Schweizer, Jyotika Singh, Shailender Singh, Weiyi Sun, Kartik Talamadupula, and Jerry Xu. 2025. Open Agent Specification (Agent Spec): A Unified Representation for AI Agents. arXiv:2510.04173 [cs.AI] https://arxiv.org/abs/2510.04173 [2]Saeed Amizadeh, Hamid Palangi, Oleksandr Polozov, Yichen Huang, and Kazuhito Koishida. 2020. Neuro-symbolic visual reasoning: disen- tangling "visual" from "reasoning". In Proceedings of the 37th Interna- tional Conference on Machine Learning (ICMLâ20). JMLR.org, Article 27, 12 pages. [3] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider (Eds.). 2003. The Description Logic Hand- book: Theory, Implementation and Applications. Cambridge University Press, Cambridge, UK. doi:10.1017/CBO9780511711787 [4] Shraddha Barke, Arnav Goyal, Alind Khare, Avaljot Singh, Suman Nath, and Chetan Bansal. 2026. AgentRx: Diagnosing AI Agent Failures from Execution Trajectories. (2026). doi:10.48550/arXiv.2602.02475 [5]Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Run- time verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20, 4 (2011), 1â64. doi:10.1145/ 2000799.2000800 [6] Luca Beurer-Kellner, Marc Fischer, and Martin Vechev. 2023. Prompting Is Programming: A Query Language for Large Language Models. Proc. ACM Program. Lang. 7, PLDI, Article 186 (June 2023), 24 pages. doi:10. 1145/3591300 [7] Yuriy Brun, Giovanna Di Marzo Serugendo, Cristina Gacek, Holger Giese, Holger M. Kienle, Marin Litoiu, Hausi A. MĂźller, Mauro Pezzè, and Mary Shaw. 2009. Engineering Self-Adaptive Systems through Feedback Loops. In Software Engineering for Self-Adaptive Systems, Betty H. C. Cheng, RogĂŠrio de Lemos, Holger Giese, Paola Inverardi, and Jeff Magee (Eds.). Lecture Notes in Computer Science, Vol. 5525. Springer, 48â70. doi:10.1007/978-3-642-02161-9_3 [8] Qiaochu Chen, Arko Banerjee, ĂaÄatay Demiralp, Greg Durrett, and IĹÄąl Dillig. 2023. Data Extraction via Semantic Regular Expression Synthesis. Proc. ACM Program. Lang. 7, OOPSLA2, Article 287 (Oct. 2023), 30 pages. doi:10.1145/3622863 [9]Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT- SIGPLAN Symposium on Principles of Programming Languages. ACM, 238â252. doi:10.1145/512950.512973 [10]RogĂŠrio de Lemos, Holger Giese, Hausi A. MĂźller, Mary Shaw, et al. 2013. Software Engineering for Self-Adaptive Systems: A Second Agents as Software: A Programming Languages Agenda for Agent ReliabilityOnward! â26, October 4â9, 2026, Oakland, CA, USA Research Roadmap. In Software Engineering for Self-Adaptive Systems I. Lecture Notes in Computer Science, Vol. 7475. Springer, 1â32. doi:10. 1007/978-3-642-35813-5_1 [11]Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Con- struction and Analysis of Systems. Springer, 337â340. doi:10.1007/978- 3-540-78800-3_24 [12]Honghua Dong, Qidong Su, Yubo Gao, Zhaoyu Li, Yangjun Ruan, Gennady Pekhimenko, Chris J Maddison, and Xujie Si. 2024. APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts. arXiv preprint arXiv:2406.13161 (2024). doi:10.48550/arXiv.2406.13161 [13]Michael Falk. 2026. Wikilambda the Ultimate: The Wikimedia Foun- dationâs Search for the Perfect Language. AI & Society (2026). doi:10.1007/s00146-026-02899-w [14]Thomas R. Gruber. 1995. Toward Principles for the Design of Ontolo- gies Used for Knowledge Sharing. International Journal of Human- Computer Studies 43, 5â6 (1995), 907â928. doi:10.1006/ijhc.1995.1081 [15]Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis. Foundations and Trends in Programming Languages 4, 1â2 (2017), 1â119. doi:10.1561/2500000010 [16]C.A.R. Hoare. 1985. Communicating Sequential Processes. Prentice Hall. http://w.usingcsp.com/cspbook.pdf [17]C. A. R. Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978), 666â677. doi:10.1145/359576.359585 [18]Tzu-Heng Huang, Catherine Cao, Vaishnavi Bhargava, and Frederic Sala. 2024. The ALCHEmist: automated labeling 500x CHEaper than LLM data annotators. In Proceedings of the 38th International Conference on Neural Information Processing Systems (Vancouver, BC, Canada) (NIPS â24). Curran Associates Inc., Red Hook, NY, USA, Article 2003, 25 pages. doi:10.48550/arXiv.2407.11004 [19]Adharsh Kamath, Sishen Zhang, Calvin Xu, Shubham Ugare, Gagan- deep Singh, and Sasa Misailovic. 2025. Enforcing temporal constraints for llm agents. (2025). doi:10.48550/arXiv.2512.23738 [20]Jeffrey O. Kephart and David M. Chess. 2003. The Vision of Auto- nomic Computing. Computer 36, 1 (2003), 41â50. doi:10.1109/MC.2003. 1160055 [21]Omar Khattab, Arnav Singhvi, Paridhi Maheshwari, Zhiyuan Zhang, Keshav Santhanam, Sri Vardhamanan, Saiful Haq, Ashutosh Sharma, Thomas T. Joshi, Hanna Moazam, Heather Miller, Matei Zaharia, and Christopher Potts. 2024. DSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines. The Twelfth International Confer- ence on Learning Representations. [22]Roham Koohestani. 2025. AgentGuard: Runtime Verification of AI Agents. In 2025 40th IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW) (Seoul, Korea, Republic of ). IEEE Press, 74â77. doi:10.1109/ASEW67777.2025.00023 [23]Leslie Lamport. 1994. The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 3 (May 1994), 872â923. doi:10.1145/177492. 177726 [24]Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., USA. [25]Douglas B. Lenat. 1995. CYC: A Large-Scale Investment in Knowledge Infrastructure. Commun. ACM 38, 11 (1995), 32â38. doi:10.1145/219717. 219745 [26] Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. The journal of logic and algebraic programming 78, 5 (2009), 293â303. doi:10.1016/j.jlap.2008.08.004 [27]Megan Li, Wendy Bickersteth, Ningjing Tang, Lorrie Cranor, Jason Hong, Hong Shen, and Hoda Heidari. 2025. A Closer Look at the Existing Risks of Generative AI: Mapping the Who, What, and How of Real-World Incidents. Proceedings of the AAAI/ACM Conference on AI, Ethics, and Society 8, 2 (Oct. 2025), 1561â1573. doi:10.1609/aies.v8i2. 36655 [28]Ziyang Li, Jiani Huang, and Mayur Naik. 2023. Scallop: A Language for Neurosymbolic Programming. Proc. ACM Program. Lang. 7, PLDI, Article 166 (June 2023), 25 pages. doi:10.1145/3591280 [29]Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. 2018. DeepProbLog: neural probabilistic logic programming. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (MontrĂŠal, Canada) (NIPSâ18). Curran Associates Inc., Red Hook, NY, USA, 3753â3763. [30]Erik Meijer. 2025. Guardians of the Agents. Commun. ACM 69, 1 (Dec. 2025), 46â52. doi:10.1145/3777544 [31]Microsoft. 2025. GenAIScript: Generative AI Scripting. Website. https: //microsoft.github.io/genaiscript/ Accessed on 01-09-2025. [32]R. Milner. 1999. Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge, UK. [33]Adithya Murali, Atharva Sehgal, Paul Krogmeier, and P. Madhusudan. 2022. Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, Luc De Raedt (Ed.). International Joint Conferences on Artificial Intelligence Organization, 3358â3365. doi:10.24963/ijcai.2022/466 Main Track. [34]Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Prin- ciples of Program Analysis. Springer. doi:10.1007/978-3-662-03811-6 [35]Martin Odersky, Yaoyu Zhao, Yichen Xu, Oliver BraÄevac, and Cao Nguyen Pham. 2026. Tracking Capabilities for Safer Agents. arXiv:2603.00991 [cs.AI] https://arxiv.org/abs/2603.00991 [36]Dhia Elhaq Rzig, Dhruba Jyoti Paul, Kaiser Pister, Jordan Henkel, and Foyzul Hassan. 2025. An Empirically-grounded tool for Automatic Prompt Linting and Repair: A Case Study on Bias, Vulnerability, and Optimization in Developer Prompts. arXiv preprint arXiv:2501.12521 (2025). doi:10.48550/arXiv.2501.12521 [37]Timo Schick, Jane Dwivedi-Yu, Roberto DessĂŹ, Roberta Raileanu, Maria Lomeli, Eric Hambro, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. 2023. Toolformer: Language models can teach themselves to use tools. Advances in neural information processing systems 36 (2023), 68539â68551. doi:10.48550/arXiv.2302.04761 [38]Nigel Shadbolt, Tim Berners-Lee, and Wendy Hall. 2006. The Semantic Web Revisited. IEEE Intelligent Systems 21, 3 (2006), 96â101. doi:10. 1109/MIS.2006.62 [39] Reshabh K Sharma, Shraddha Barke, and Benjamin Zorn. 2026. Willful Disobedience: Automatically Detecting Failures in Agentic Traces. In Proceedings of the ACM Conference on AI and Agentic Systems (CAIS â26). Association for Computing Machinery, New York, NY, USA, 584â596. doi:10.1145/3786335.3813153 [40]Reshabh K Sharma, Jonathan De Halleux, Shraddha Barke, Dan Gross- man, and Benjamin Zorn. 2025. Promptpex: Automatic test generation for language model prompts. (2025). doi:10.48550/arXiv.2503.05070 [41]Renee Shelby, Shalaleh Rismani, Kathryn Henne, AJung Moon, Negar Rostamzadeh, Paul Nicholas, NâMah Yilla-Akbari, Jess Gallegos, An- drew Smart, Emilio Garcia, and Gurleen Virk. 2023. Sociotechnical Harms of Algorithmic Systems: Scoping a Taxonomy for Harm Reduc- tion. In Proceedings of the 2023 AAAI/ACM Conference on AI, Ethics, and Society (MontrĂŠal, QC, Canada) (AIES â23). Association for Computing Machinery, New York, NY, USA, 723â741. doi:10.1145/3600211.3604673 [42]Armando Solar-Lezama, Rodric Rabbah, Rastislav BodĂk, and Kemal EbcioÄlu. 2005. Programming by sketching for bit-streaming programs. In Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation. 281â294. doi:10.1145/1065010. 1065045 [43]DĂdac SurĂs, Sachit Menon, and Carl Vondrick. 2023. ViperGPT: Vi- sual Inference via Python Execution for Reasoning. In 2023 IEEE/CVF International Conference on Computer Vision (ICCV). 11854â11864. doi:10.1109/ICCV51070.2023.01092 Onward! â26, October 4â9, 2026, Oakland, CA, USAShraddha Barke and Adithya Murali [44]Mandana Vaziri, Louis Mandel, Claudio Spiess, and Martin Hirzel. 2024.PDL: A Declarative Prompt Programming Language. arXiv:2410.19135 [cs.AI] https://arxiv.org/abs/2410.19135 [45]Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional program- ming. 269â282. doi:10.1145/2628136.2628161 [46]Denny VrandeÄiÄ and Markus KrĂśtzsch. 2014. Wikidata: A Free Collaborative Knowledgebase. Commun. ACM 57, 10 (2014), 78â85. doi:10.1145/2629489 [47] Haoyu Wang, Christopher M. Poskitt, and Jun Sun. 2025. AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents. arXiv:2503.18666 [cs.AI] https://arxiv.org/abs/2503.18666 [48]Laura Weidinger, Maribeth Rauh, Nahema Marchal, Arianna Manzini, Lisa Anne Hendricks, Juan Mateos-Garcia, Stevie Bergman, Jackie Kay, Conor Griffin, Ben Bariach, Iason Gabriel, Verena Rieser, and William Isaac. 2023. Sociotechnical Safety Evaluation of Generative AI Systems. arXiv:2310.11986 [cs.AI] https://arxiv.org/abs/2310.11986 [49]Melwin Xavier, Melveena Jolly, Midhun Xavier, et al.2026. Agentproof: Static Verification of Agent Workflow Graphs. (2026). doi:10.48550/ arXiv.2603.20356 [50]Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. 2022. React: Synergizing reasoning and acting in language models. arXiv preprint arXiv:2210.03629 (2022). doi:10.48550/arXiv.2210.03629 [51]Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Chuyue Sun, Jeff Huang, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark Barrett, and Ying Sheng. 2024. SGLang: Efficient Execution of Structured Language Model Programs. arXiv preprint arXiv:2312.07104 (2024). https://arxiv.org/abs/2312.07104 [52]Kaijie Zhu, Jindong Wang, Jiaheng Zhou, Zichen Wang, Hao Chen, Yidong Wang, Linyi Yang, Wei Ye, Yue Zhang, Neil Gong, et al.2023. Promptrobust: Towards evaluating the robustness of large language models on adversarial prompts. In Proceedings of the 1st ACM workshop on large AI systems and models with privacy and safety analysis. 57â68. doi:10.1145/3689217.3690621 Received 2026-05-15; accepted 2026-06-28