Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Benedikt Bollig

cs.LO May 20, 2026 · v2 cs.AI cs.PL

Read PDF arXiv abstract Code

TL;DR

MSCs, Causal Past Logic semantics, the knowledge-vector monitor, and its correctness theorem are mechanized in Lean 4 without sorry.

Abstract

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.

Problem

In asynchronous distributed LLM-agent workflows, a lifeline's decision can only depend on events causally visible to it. Workflow guards therefore need a logic and a monitor that respect this causal visibility.

Approach

The ZipperGen choreographic agent-workflow framework is extended with Causal Past Logic (CPL), an adaptation of PT-DTL interpreted over valued message sequence charts. CPL supports previous/since operators and inspection of the latest causally visible event of another lifeline and its variables. A knowledge-vector monitor using vector clocks and latest-value views is adapted to ZipperGen. Its correctness with respect to the denotational semantics is proved and mechanized in Lean 4.

Results

The locally computed monitor value is proven to coincide with the guard's semantics at the current event, and the Lean development kernel-checks without sorry or custom axioms. A Python prototype shows sub-millisecond to few-millisecond per-event overhead on the benchmarks.

Workload	ℓ	Atoms n	Vars k	Local (ms)	Send (ms)	Msg data (KB)
Code review	4	–	1	0.047	0.069	1.2
Scaling Ψ	32	16	4	0.209	0.506	17.0
Scaling Ψ	8	128	128	1.976	2.979	58.0

Monitor overhead per event (selected workloads)

Papers With

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows