Agents as Software: A Programming Languages Agenda for Agent Reliability

1 Introduction

• Agents’ behavior is distributed across prompts, tools, memories, policies, plans, traces, and orchestration logic, leaving their programming model implicit and only partially specified.The paper argues that conventional testing and debugging are inadequate for this setting.Source: §1 · p. 1
• Specifications can express familiar software properties and agent-specific concerns over event logs, state, permissions, information flow, tool preconditions, belief updates, and resource use.Examples include authorization, grounded belief, stale evidence, tool-use justification, and recoverability after failure.Source: §1 · p. 1
• Static analysis can check prompts, plans, tool schemas, memory policies, and configurations before deployment for ambiguous obligations, invalid flows, and premature reachability of high-impact actions.Runtime monitoring can track goals, outputs, evidence, permissions, obligations, and constraints to check grounded actions, valid beliefs, authorization, and trace properties.Source: §1 · p. 1
• Execution traces can inform improved specifications, workflow repairs, tool-use optimization, and agent evolution as environments change.The proposed reliability process spans checks before execution, monitoring during execution, and improvement afterward; its goal is governability, not determinism.Source: §1 · p. 2
• The agenda must account for agents revising their own artifacts, predicates with nondeterministic interpretations, and runs that admit multiple abstractions whose monitors may disagree.The paper also surveys specifications and program analysis as the following sections’ topics.Source: §1 · p. 2

Specifications for AI Agents

• Agent specifications combine an abstract computational model, a compositional logic for properties, and domain-specific functions and predicates.The section treats risks such as memory mishandling, permission violations, leaked secrets, type errors, and functional incorrectness as computational problems.Source: §2 · p. 2

Formalizing Specifications

• Event logs offer an action-based abstraction suited to open-ended, concurrent, delegated workflows, while state-based invariants may be difficult to identify for dynamic executions.The event vocabulary determines which executions are indistinguishable; the designer chooses which events to log, and the abstraction must be defined carefully because delegation can yield different abstract traces with different specification outcomes.Source: §2 · pp. 2–3

Limits of Specifications

• Event-log specifications inherit abstraction incompleteness, and the essay leaves more involved security-oriented abstraction and specification mechanisms unexplored.A password leak can evade an email-focused specification; default-restrictive models and capability permissions can limit unmodeled actions, while not all harms are readily expressible as formal specifications.Source: §2 · pp. 2–4

Agent Specifications

• Resource- and permission-based specifications are a particularly immediate challenge because coordination and delegation require tracking permission provenance across unbounded traces.The section highlights reasoning about whether an agent instance may access or modify a resource or call a tool.Source: §2 · p. 4

Knowledge and Belief

• Knowledge and belief specifications can require actions to follow observable evidence, reject beliefs contradicted by later evidence, or ensure mutual knowledge before coordinated commitment.Grounded-belief checks can be monitored dynamically against facts derivable from the current trace prefix.Source: §2 · p. 4

Natural-Language Theories

• A formal account of natural-language theories remains underdeveloped, including how learned predicates relate through implication, incompatibility, and revision.The section notes that a general framework integrating reasoning mechanisms over fallible learned predicates is lacking, while predicate meanings can depend on context.Source: §2 · pp. 4–6
• The proposed direction is to develop reusable mechanisms for defining predicate signatures, relations among predicates, and algorithms for reasoning over such theories.The authors compare this goal to designing type systems that package reasoning patterns into higher-level categories and algorithms.Source: §2 · p. 6

The Role of Language Design

• Prompt- and agent-programming languages could integrate types, permissions, and tests into workflows, reducing the burden of checking some properties during execution.This is presented as a correct-by-construction approach to reliability.Source: §2 · p. 6

3.1 Static Analysis

• Static analysis checks prompts, tool schemas, policies, memory, and workflows before deployment for unclear obligations, invalid data flows, and unsafe action reachability.It examines whether configurations make reliable execution possible, rather than predicting an exact execution path.Source: §3.1 · pp. 6–7
• Prompts are checkable interfaces, while tool and workflow validation checks action schemas, data dependencies, and whether high-impact actions become reachable only after required evidence.Checks include missing or contradictory prompt obligations, schema-conformant outputs, grounded arguments, and required confirmation or authorization.Source: §3.1 · pp. 6–7

3.2 Dynamic Analysis

• Dynamic analysis monitors execution prefixes, maintaining runtime state for established facts, their provenance, active constraints, and unresolved obligations.The state can track evidence separately from task progress and resource use.Source: §3.2 · pp. 7–8
• Runtime checks require current evidence and correctly ordered events before actions, while trace-wide invariants catch violations such as cumulative spending beyond a budget.Evidence can become stale or be invalidated; temporal guards can require prior confirmation before a high-impact action.Source: §3.2 · pp. 9–10
• After a violation, monitoring can block an action, request evidence, refresh state, or replan when recovery remains possible; repeated failures can inform revised specifications.Irreversible actions may instead require aborting, escalating, or restarting; mined specifications are candidates for review, not ground truth.Source: Figure 2 · p. 8, §3.2 · p. 10

• The essay proposes specifications over formal models of agent executions and static and dynamic enforcement methods, as a starting point for a broader reliability agenda.Source: §4 · p. 10