Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

🕒 Published (v1): 2026-05-20 09:09 UTC · Source: Arxiv · link

Why this paper was selected

Causal past logic for correct runtime monitoring of asynchronous distributed agent workflows

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Distributed LLM agent workflows execute asynchronously, so monitoring based on a sequential log is semantically wrong: a local decision can only depend on events causally visible to the deciding agent. This paper extends the ZipperGen choreographic-programming framework with Causal Past Logic (CPL), a past-time temporal logic used as source-level runtime guards, and proves (mechanized in Lean 4) that a vector-clock monitor evaluates every guard correctly with respect to the MSC denotational semantics.

Problem

Existing guardrail and monitoring mechanisms for LLM workflows treat execution as a single sequential log. In an asynchronous multi-agent system, this is incorrect: an event that appears earlier in global time may not yet be causally visible to the lifeline making a decision, and a monitor using global ordering can block or permit actions that contradict local knowledge. There was no formal language for expressing causal-temporal guards directly inside workflow control flow, nor a proved-correct online algorithm for evaluating them distributedly.

Method

Execution model. Runs are modeled as Message Sequence Charts (MSCs): a finite set of events partitioned across lifelines with a local linear order \(\leq_A\) per lifeline and a message relation \(\triangleleft\) between sends and receives. The causal order \(\leq_M\) is the reflexive-transitive closure of local-successor and message edges.

Causal Past Logic (CPL). A small past-time temporal logic with four key constructs: - \(Y\phi\): \(\phi\) held at the immediately preceding local event (standard previous operator). - \(\phi_1 \,S\, \phi_2\): since along the owner lifeline's local order. - \(@A(\phi)\): evaluate \(\phi\) at \(\text{last}_A(e)\), the latest event of lifeline \(A\) causally visible from the current event \(e\). - \(@A.x\): read variable \(x\) from \(\text{last}_A(e)\)'s valuation (usable inside atomic predicates).

Guards are written \(\phi@A\) and owned by lifeline \(A\); they are evaluated locally by \(A\) at a choice event and gate control flow (branch/loop), not just reported post-hoc.

Online monitor. Each lifeline \(A\) maintains: 1. A vector clock \(vc_A : \mathcal{L} \to \mathbb{N}\) tracking causal predecessor counts. 2. A Boolean latest-value view \(\text{view}_A : \mathcal{L} \times \text{sub}(\Phi) \rightharpoonup \{0,1\}\): truth of each subformula at the latest visible event per lifeline. 3. A variable view \(\text{var}_A : \mathcal{L} \times \text{Vars}(\Phi) \rightharpoonup \text{Val}\): selected variable values at those events. 4. A local store \(\sigma_A\) and a previous-local copy \(\text{old}_A\) for \(Y\)/\(S\) evaluation.

On each event, \(A\) merges incoming vector clocks and views (taking the message's entry for lifeline \(B\) when \(\mu.\text{vc}(B) > vc_A(B)\)), increments its own clock, updates \(\sigma_A\), and re-evaluates all subformulas bottom-up. Sends carry the current \((vc_A, \text{view}_A, \text{var}_A)\) to receivers.

Monitor state size per lifeline: \(O(|\mathcal{L}| \cdot |\text{sub}(\Phi)|)\) Boolean bits plus \(O(|\mathcal{L}| \cdot |\text{Vars}(\Phi)|)\) variable values.

Correctness. Coherent pre-evaluation state (Definition 5) formalizes that \(vc_A(B) = |\{f \in E_B \mid f \leq_M e\}|\) and that \(\text{view}_A, \text{var}_A\) accurately describe the latest visible \(B\)-event. Lemma 1 (proved by structural induction on \(\phi\), mechanized in Lean 4): if the state is coherent before evaluating at \(e\), then \(\text{EvalA}(\psi, e, \text{old}_A) = 1 \iff M, e \models \psi\).

Key Contributions

• CPL: a formally defined past-time temporal logic with causal modalities \(@A(\phi)\) and \(@A.x\) over MSC semantics.
• Source-level guards: CPL formulas integrated into ZipperGen's conditional/loop syntax so they influence control flow at decision time, not only after the fact.
• Proved-correct online monitor: vector-clock + latest-value-view algorithm with a formal coherence invariant and a mechanized correctness theorem.
• Lean 4 mechanization: full formalization of MSC definitions, CPL satisfaction, monitor state, and the correctness proof.
• Prototype implementation in ZipperGen (https://zippergen.io).

Results

No empirical benchmarks are reported; this is a formal-methods contribution. The headline result is:

• Lemma 1 (mechanized): For any coherent pre-evaluation state at event \(e \in E_A\), \(\forall \psi \in \text{sub}(\Phi)\): \(\text{EvalA}(\psi, e, \text{old}_A) = 1 \iff M, e \models \psi\). Proved by structural induction and verified in Lean 4.
• Illustrated example: concurrent code-review workflow with TestRunner, Security, and Committer agents; shows a scenario where a sequential-log monitor would incorrectly block a merge because a failure message is in-flight but causally invisible at the decision point.

Limitations

• Vector-clock entries are unbounded counters; consistent with known lower bounds showing finite-state monitors cannot track latest values exactly in general.
• No empirical evaluation of runtime overhead (message size inflation from piggybacked views, latency impact).
• Per-lifeline parallel composition (multiple simultaneously-enabled local actions) is noted as adding complexity but not fully elaborated.
• CPL does not replace synchronization barriers; it only makes explicit what is locally visible — stronger policies still require explicit sync in the workflow.
• The approach assumes ZipperGen's projection discipline (explicit ownership of branch/loop decisions); applicability to arbitrary agent frameworks requires additional scaffolding.

Relevance to Harnesses / Meta-Harnesses

A meta-harness that fans out work to parallel agents and then conditions downstream actions on their results faces exactly the causal-visibility problem this paper solves: a result that exists in one agent's output may not yet have propagated to the coordinator deciding the next step. CPL provides a principled language for specifying cross-agent preconditions (e.g., "the reviewer's latest visible status is 'passed' with no subsequent failure") directly inside orchestration logic, replacing ad-hoc polling or sequential-log scans. The vector-clock + latest-value-view propagation mechanism shows how to implement causal-state tracking in a distributed pipeline without a central log aggregator, which is directly applicable to harness coordination layers. The correctness theorem gives formal guarantees that guards embedded in a harness's branching logic reflect true causal knowledge — a property that most current harness designs lack entirely.