# Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

arXiv: https://arxiv.org/abs/2605.20923 · HTML: https://mlsanity.com/paper/2605.20923/

## Key facts

- Cited by 1 papers 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.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 18 of 18)

- [AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents](https://mlsanity.com/paper/2503.18666/) (2025)
- [Enforcing Temporal Constraints for LLM Agents](https://mlsanity.com/paper/2512.23738/) (2025)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [A Trace-Based Assurance Framework for Agentic AI Orchestration: Contracts, Testing, and Governance](https://mlsanity.com/paper/2603.18096/) (2026)
- [HasChor: Functional Choreographic Programming for All (Functional Pearl)](https://mlsanity.com/paper/2303.00924/) (2023)
- [Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems](https://mlsanity.com/paper/2605.16198/) (2026)
- [Pirouette: Higher-Order Typed Functional Choreographies](https://mlsanity.com/paper/2111.03484/) (2021)
- [Pact: A Choreographic Language for Agentic Ecosystems](https://mlsanity.com/paper/2605.03143/) (2026)
- [From Clarity to Efficiency for Distributed Algorithms](https://mlsanity.com/paper/1412.8461/) (2014)
- [Dynamic Choreographies: Theory And Implementation](https://mlsanity.com/paper/1611.09067/) (2016)
- [Gossiping in Message-Passing Systems](https://mlsanity.com/paper/1802.08641/) (2018)
- [On the Monitorability of Session Types, in Theory and Practice (Extended Version)](https://mlsanity.com/paper/2105.06291/) (2021)
- [Monitoring Blackbox Implementations of Multiparty Session Protocols](https://mlsanity.com/paper/2306.04204/) (2023)
- [Sound Concurrent Traces for Online Monitoring Technical Report](https://mlsanity.com/paper/2402.18391/) (2024)
- [Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages](https://mlsanity.com/paper/2405.11308/) (2024)
- [A Note on Runtime Verification of Concurrent Systems](https://mlsanity.com/paper/2507.04830/) (2025)
- [Runtime Verification of Interactions Using Automata](https://mlsanity.com/paper/2511.00531/) (2025)
- [Provable Coordination for LLM Agents via Message Sequence Charts](https://mlsanity.com/paper/2604.17612/) (2026)

## Built on by (most cited first, 1 of 1)

- [SoK: Formal Methods for Fact-Checking and Information Integrity](https://mlsanity.com/paper/2609.23239/) (2026)

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