One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AI
Agentic AI pipelines interleave LLM decisions, state changes, tool calls, and cross-agent delegation, so a single monitoring formalism cannot cover every boundary. This paper proposes AgenticRV, an architecture that separates execution-boundary adapters from monitors via canonical events, per-monitor projections and abstractions, and a policy layer that arbitrates normalized verdicts. Its core contribution is an interoperability contract with formal conditions for when observations suffice, when monitors can be replaced without changing decisions, and when blocking actually prevents effects.
The paper offers a clean, modular runtime-verification architecture and honestly scopes its claims to interface integration rather than end-to-end agent safety. However, the empirical evaluation is thin—only tens of controlled decisions and a handful of anecdotal LLM runs—so the practical assurance story remains largely theoretical. The prevention guarantee is structurally sound but hinges on strong serialisation and faithful-adapter assumptions that are easy to violate in real deployments.
The separation of concerns between adapters, canonical events, per-monitor projections, and normalized verdicts is well designed and clearly formalized. Definition 3 formalizes property-sufficient observation ($\forall\tau,\tau^{\prime}\in H:\mathit{obs}_{m}(\tau)=\mathit{obs}_{m}(\tau^{\prime})\Rightarrow b(\tau)=b(\tau^{\prime})$), giving a crisp information-theoretic condition that every plug-in monitor must respect. Proposition 2 shows that replacing a monitor preserves the system reaction as long as normalized control metadata is unchanged, which legitimately decouples the policy from any monitor's internal semantics. The controlled ablations in Table 2 and the cross-adapter scope experiment in Table 3 are carefully constructed and directly support the paper's central thesis that different monitors observe different things and must be combined.
The evaluation scale is far too small to support safety claims outside the laboratory: 34 controlled tool decisions, 24 cross-boundary reporting decisions, and exactly four LLM-driven witnesses. The authors candidly admit this limitation, but it leaves the architecture's robustness under realistic concurrency, noisy models, and long traces unexamined. Proposition 3's conditional prevention argument requires serialised check-and-release, comprehensive boundary coverage, and perfectly faithful adapter enforcement; the paper notes these are "limited to the instrumented boundaries," yet many agent effects (unwrapped calls, internal state merges, remote-agent internals) simply fall outside them. The architecture also demands manual configuration of projection, abstraction, trusted propositions, and scope bindings, with no automated derivation or task isolation.
The evidence supports integration correctness and interface separation, but it does not compare AgenticRV against existing guardrail or enforcement frameworks such as AgentSpec or NeMo Guardrails on any shared benchmark. The paper fairly states that its results "concern interface integration and conditional enforcement, rather than comparative end-to-end agent safety," yet without empirical comparison the practical advantage of formalism agnosticism over a unified DSL remains unquantified. The ablation in Table 2 is strong evidence for joint monitoring, but it is deterministic and uses hand-crafted paths rather than realistic agent tasks.
The Python implementation is open-source with exact version pins and commit-level supplements, and the microbenchmarks report specific hardware and software environments. These details should allow independent reproduction of the measured overheads and the controlled test paths. However, reproducing the assurance claims for a new application requires substantial manual work: the architecture does not automate projection, abstraction, trusted-proposition validation, or policy selection, and the scope configuration for interleaved tasks is left to the deployer. The differential checks enumerate only traces of length at most four, so they do not close the verification gap for the unbounded case.
Agentic AI systems combine model decisions, mutable state, tool calls, and delegation to external agents. Monitoring them requires observations from different execution boundaries, while prevention requires control before an operation produces its effect. We present AgenticRV, a runtime-verification architecture that separates these boundaries from the monitoring formalism. Adapters emit canonical events; each monitor receives its own projection and abstraction; and a decision policy uses normalised verdicts to select a reaction supported by the responsible adapter. We formalise when observations suffice, monitor replacement preserves decisions, and blocking prevents unsafe effects. We also distinguish rejected attempts from completed effects, avoiding the assumption that a blocked request must leave every monitor in a permanent violation state. The Python implementation supports LangGraph, MCP, and A2A. A controlled LangGraph experiment combines an external Reelay temporal monitor with a programmatic report monitor; ablations show why both are needed for the selected requirements. Differential checks and cross-adapter tests provide further integration evidence. An LLM-driven incident-response example illustrates the same enforcement path, while existing microbenchmarks isolate framework costs. The results support reuse of monitoring methods at explicit control boundaries, subject to the stated observation and deployment assumptions.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.