Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
On the map: LLM agents and tool use → Software engineering coding agents
Abstract (arXiv)
We study runtime monitoring for distributed LLM-agent workflows. In an asynchronous execution, a decision can only depend on events that are causally visible to the lifeline that makes it: an event that appears earlier in some log may still be unknown locally. We extend the ZipperGen agent-workflow framework with Causal Past Logic (CPL), an adaptation of PT-DTL to guards in if-constructs and while loops. In addition to standard past-time modalities such as previous and since, a guard can inspect the latest causally visible event of another lifeline and selected variables stored there. The owner evaluates the guard online to select the next branch or loop step. We adapt the knowledge-vector monitor to ZipperGen and prove that the locally computed monitor value coincides with the denotational semantics of the guard at the current event.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. Builds on 18 of its 68 references that are in the map. First posted on arXiv 20 May 2026.
Builds on
18 of 68 references.
References · 18
- 2025AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agentscited by 223
- 2025Enforcing Temporal Constraints for LLM Agentscited by 34
- 2025RvLLM: LLM Runtime Verification with Domain Knowledgecited by 17
- 2026A Trace-Based Assurance Framework for Agentic AI Orchestration: Contracts, Testing, and Governancecited by 8
- 2023HasChor: Functional Choreographic Programming for All (Functional Pearl)cited by 3
- 2026Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systemscited by 3
- 2021Pirouette: Higher-Order Typed Functional Choreographiescited by 2
- 2026Pact: A Choreographic Language for Agentic Ecosystemscited by 2
- 2014From Clarity to Efficiency for Distributed Algorithmscited by 1
- 2016Dynamic Choreographies: Theory And Implementationcited by 1
- 2018Gossiping in Message-Passing Systemscited by 1
- 2021On the Monitorability of Session Types, in Theory and Practice (Extended Version)cited by 1
6 more
- 2023Monitoring Blackbox Implementations of Multiparty Session Protocolscited by 1
- 2024Sound Concurrent Traces for Online Monitoring Technical Reportcited by 1
- 2024Propositional dynamic logic and asynchronous cascade decompositions for regular trace languagescited by 1
- 2025A Note on Runtime Verification of Concurrent Systemscited by 1
- 2025Runtime Verification of Interactions Using Automatacited by 1
- 2026Provable Coordination for LLM Agents via Message Sequence Chartscited by 1
Built on by
Citing papers per year: 2026: 1.
1 paper.
Similar, not cited
Close in wording, no citation either way
- 2026From Agent Loops to Structured Graphs:A Scheduler-Theoretic Framework for LLM Agent Execution
- 2026Symbolic Temporal Supervision of LLM Agents Using Contracts
- 2025The Dual-State Architecture for Reliable LLM Agents
- 2026Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
- 2026VineLM: Trie-Based Fine-Grained Control for Agentic Workflows
- 2026When Agentic Executions Fail: Detecting and Localizing Runtime Faults from Telemetry
- 2026From Static Templates to Dynamic Runtime Graphs: A Survey of Workflow Optimization for LLM Agents
- 2026Formal Verification of Agentic Systems over Operational Data