pith. sign in

arxiv: 2605.20923 · v1 · pith:AOLCRCUInew · submitted 2026-05-20 · 💻 cs.LO · cs.AI· cs.PL

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Benedikt Bollig This is my paper

Pith reviewed 2026-05-21 02:27 UTC · model grok-4.3

classification 💻 cs.LO cs.AIcs.PL
keywords causal past logicruntime verificationdistributed LLM agentsvector clockstemporal logicasynchronous workflowsagent coordinationonline monitoring
0
0 comments X

The pith

A vector-clock monitor lets distributed LLM agents evaluate causal-past guards correctly at runtime.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Causal Past Logic to let guards in distributed agent workflows depend only on events that are causally visible to the deciding lifeline. This matters because in asynchronous settings an event earlier in one log may not yet be known locally. The logic adds modalities for previous events and latest values from other lifelines. It supplies a vector-clock monitor with latest-value views that evaluates the formula online. The central result proves that the locally computed monitor value coincides with the denotational semantics of the guard at the current event.

Core claim

In distributed LLM agent workflows, a decision at a lifeline can only depend on causally visible past events. Causal Past Logic (CPL) extends past-time temporal logic with inspection of the latest causally visible event of another lifeline and selected variables stored there. A vector-clock monitor with latest-value views evaluates the formula locally, and its result coincides with the denotational semantics of the guard at the current event.

What carries the argument

Vector-clock monitor with latest-value views: it tracks causal history and selected variable values to evaluate guards online in the asynchronous model.

If this is right

  • Runtime verification becomes part of the coordination language itself rather than a post-hoc check over an execution log.
  • Guards in conditionals and while loops can influence control flow at runtime using only causally visible information.
  • The monitor works for any source-level guard written in CPL without requiring a separate verification phase.
  • Local computation at each lifeline produces the same result as the global denotational semantics for that guard.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same monitor construction could apply to other distributed asynchronous systems that need past-time guards over causal histories.
  • Embedding such monitors might reduce incorrect control-flow decisions in multi-agent setups where information propagates unevenly.
  • Further extensions could combine CPL with mechanisms that recover from lost causal information in lossy networks.

Load-bearing premise

Standard vector-clock properties suffice to capture exactly the causally visible past for every lifeline without additional synchronization or loss of information in the asynchronous model.

What would settle it

An execution trace in which the value computed by the local vector-clock monitor for a CPL guard differs from the value given by the denotational semantics over the full causal past at that event.

Figures

Figures reproduced from arXiv: 2605.20923 by Benedikt Bollig.

Figure 1
Figure 1. Figure 1: Architecture for concurrent code review. The Orchestrator distributes the patch to the TestRunner and Security agent, and sends a merge proposal to the Committer when a candidate is ready to be considered. The proposal triggers the Committer’s decision procedure. The reviewers run in parallel and may send updated assessments after their first report. merged. These agents run concurrently and report their r… view at source ↗
Figure 2
Figure 2. Figure 2: Causal structure around a merge decision, focusing on the events relevant to the Committer’s guard. Earlier messages that assign the patch to the TestRunner are omitted. The required check passes and its result reaches the Committer before the merge proposal. A subsequent check finds a failure, but this update has not yet been delivered. It is therefore not in the Committer’s causal past at the choice even… view at source ↗
read the original abstract

Distributed LLM agent workflows should not be monitored as if they produced a single sequential log. 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), a small past-time temporal logic for guards in conditionals 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 formula is a source-level guard: it is evaluated online by the owner lifeline and can influence control flow at runtime. We give a vector-clock monitor with latest-value views and prove that the locally computed monitor value coincides with the denotational semantics of the guard at the current event. Thus runtime verification becomes part of the coordination language itself, rather than a post-hoc check over an execution log.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces Causal Past Logic (CPL), a small past-time temporal logic extending the ZipperGen framework for guards in conditionals and while loops within distributed LLM agent workflows. It defines modalities for inspecting the latest causally visible event on another lifeline and selected variables, presents a vector-clock monitor with latest-value views, and claims to prove that the locally computed monitor value coincides with the denotational semantics of the guard at the current event, thereby integrating runtime verification into the coordination language.

Significance. If the equivalence holds, the work enables embedding causal-aware runtime verification directly into asynchronous agent coordination, addressing the mismatch between sequential logs and causally visible pasts in LLM workflows. The approach builds on standard vector-clock theory and denotational semantics without introducing new parameters or self-referential definitions, which is a methodological strength for reproducibility and falsifiability.

major comments (2)
  1. [Abstract] Abstract: the central claim that the vector-clock monitor with latest-value views computes exactly the denotational semantics relies on the assumption that standard vector-clock properties suffice to capture the causally visible past exactly. In the presence of runtime message routing and non-deterministic agent decisions, the monitor update rule must explicitly recompute latest values only on causal predecessors (rather than delivery order) to prevent divergence; without this detail the equivalence is not yet load-bearing.
  2. [Abstract] Abstract (proof sketch): the asserted proof of monitor equivalence lacks the full derivation, error handling details, or edge cases for asynchronous interleavings and arbitrary causal histories. These are required to confirm that every causally preceding event is reflected exactly when the vector clock indicates it and that no spurious later values become visible.
minor comments (2)
  1. [Monitor construction] The manuscript would benefit from an explicit definition of the latest-value view update function and how it interacts with the vector-clock advancement rule.
  2. [Examples] Consider adding a small example workflow with an interleaving that exercises the 'latest causally visible event' modality to illustrate the distinction from sequential past-time logic.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We are grateful to the referee for the insightful comments on the abstract and proof presentation. We believe the core technical contribution is sound, and we will make revisions to improve clarity as detailed in the responses below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that the vector-clock monitor with latest-value views computes exactly the denotational semantics relies on the assumption that standard vector-clock properties suffice to capture the causally visible past exactly. In the presence of runtime message routing and non-deterministic agent decisions, the monitor update rule must explicitly recompute latest values only on causal predecessors (rather than delivery order) to prevent divergence; without this detail the equivalence is not yet load-bearing.

    Authors: We thank the referee for pointing this out. The full paper defines the monitor update rule in Definition 4.2 to only incorporate latest values from events where the incoming vector clock is dominated by the current one, which enforces causal predecessors exclusively. This is independent of message delivery order due to the properties of vector clocks. Non-deterministic agent decisions are handled because the guard evaluation uses only the locally visible past. We will revise the abstract to include a short statement on this update rule to make the claim load-bearing. revision: yes

  2. Referee: [Abstract] Abstract (proof sketch): the asserted proof of monitor equivalence lacks the full derivation, error handling details, or edge cases for asynchronous interleavings and arbitrary causal histories. These are required to confirm that every causally preceding event is reflected exactly when the vector clock indicates it and that no spurious later values become visible.

    Authors: The proof is given in Theorem 5.1 of the manuscript, which proceeds by structural induction on the formula and on the length of the causal history. Edge cases for asynchronous interleavings are covered by the fact that vector clocks provide a partial order, and only comparable clocks allow visibility. We will expand the abstract's proof sketch to mention that the equivalence holds for arbitrary causal histories by the induction hypothesis, and add a paragraph on error handling for out-of-order messages (which are discarded if not causal). This addresses the request for more details. revision: partial

Circularity Check

0 steps flagged

No circularity: proof relies on external vector-clock properties and denotational semantics.

full rationale

The paper constructs a vector-clock monitor for CPL guards and proves local computation coincides with denotational semantics at the current event. This uses standard vector-clock theory (external to the paper) to identify causally visible past events and latest-value views. No step reduces by construction to a fitted parameter, self-definition, or self-citation chain; the equivalence is derived from established concurrency results rather than renaming or smuggling an ansatz. The derivation is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The contribution rests on standard distributed-systems assumptions and the introduction of a new logic; no free parameters are fitted to data.

axioms (2)
  • standard math Vector clocks correctly track causal precedence in asynchronous distributed executions
    Invoked for the monitor construction and equivalence proof.
  • domain assumption Denotational semantics of past-time temporal logic with latest-value views is well-defined
    Used as the target that the local monitor must match.
invented entities (1)
  • Causal Past Logic (CPL) no independent evidence
    purpose: Express guards that inspect causally visible events and variables across lifelines
    New logic defined in the paper for this setting.

pith-pipeline@v0.9.0 · 5698 in / 1296 out tokens · 34854 ms · 2026-05-21T02:27:56.164027+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 49 canonical work pages · 4 internal anchors

  1. [1]

    In: Sobocinski, P., Lago, U.D., Esparza, J

    Adsul, B., Gastin, P., Kulkarni, S., Weil, P.: An expressively complete local past propositional dynamic logic over mazurkiewicz traces and its applications. In: Sobocinski, P., Lago, U.D., Esparza, J. (eds.) Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Esto- nia, July 8-11, 2024. pp. 2:1–2:13. ACM (2024)

    work page 2024

  2. [2]

    In: Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Trans- parency (FAccT 2026)

    Alamdari, P.A., Klassen, T.Q., McIlraith, S.A.: Formal methods meet LLMs: Au- diting, monitoring, and intervention for compliance of advanced AI systems. In: Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Trans- parency (FAccT 2026). ACM, Montreal, QC, Canada (Jun 2026), to appear

    work page 2026

  3. [3]

    In: Baeten, J.C.M., Mauw, S

    Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR ’99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings. pp. 114–129. Lecture Notes in Computer Science, Springer (1999)

    work page 1999

  4. [4]

    In: Bartocci, E., Falcone, Y

    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification - Introductory and Advanced Topics, pp. 1–33. Lecture Notes in Computer Science, Springer (2018)

    work page 2018

  5. [5]

    Formal Methods Syst

    Bauer, A., Falcone, Y.: Decentralised LTL monitoring. Formal Methods Syst. Des. 48(1-2), 46–93 (2016)

    work page 2016

  6. [6]

    ACM Trans

    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol.20(4), 14:1–14:64 (2011)

    work page 2011

  7. [7]

    Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci.669, 33–58 (2017)

    work page 2017

  8. [8]

    In: Gastin, P., Laroussinie, F

    Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. pp. 162–176. Lecture Notes in Computer Science, Springer (2010)

    work page 2010

  9. [9]

    Gossiping in Message-Passing Systems

    Bollig, B., Fortin, M., Gastin, P.: Gossiping in message-passing systems. CoRR abs/1802.08641(2018)

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  10. [10]

    Bollig, B., Fortin, M., Gastin, P.: Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic. J. Comput. Syst. Sci.115, 22–53 (2021)

    work page 2021

  11. [11]

    Provable Coordination for LLM Agents via Message Sequence Charts

    Bollig, B., F¨ ugger, M., Nowak, T.: Provable coordination for LLM agents via mes- sage sequence charts. CoRRabs/2604.17612(2026)

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  12. [12]

    Bollig, B., Kuske, D., Meinecke, I.: Propositional dynamic logic for message-passing systems. Log. Methods Comput. Sci.6(3) (2010)

    work page 2010

  13. [13]

    Dagstuhl Artifacts Ser.7(2), 02:1–02:3 (2021)

    Burl` o, C.B., Francalanza, A., Scalas, A.: On the monitorability of session types, in theory and practice (artifact). Dagstuhl Artifacts Ser.7(2), 02:1–02:3 (2021)

    work page 2021

  14. [14]

    In: Giacobazzi, R., Cousot, R

    Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. pp. 263–274. ACM (2013)

    work page 2013

  15. [15]

    In: Halbwachs, N., Zuck, L.D

    Chen, F., Rosu, G.: Java-mop: A monitoring oriented programming environment for java. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Con- struction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Soft- ware, ETAPS 2005, Edinburgh, UK, April 4-8,...

    work page 2005

  16. [16]

    In: Bruni, R., Sassone, V

    Chen, T., Bocchi, L., Deni´ elou, P., Honda, K., Yoshida, N.: Asynchronous dis- tributed monitoring for multiparty session enforcement. In: Bruni, R., Sassone, V. (eds.) Trustworthy Global Computing - 6th International Symposium, TGC 2011, Aachen, Germany, June 9-10, 2011. Revised Selected Papers. pp. 25–45. Lecture Notes in Computer Science, Springer (2011)

    work page 2011

  17. [17]

    In: Finkbeiner, B., Mariani, L

    Dawes, J.H., Reger, G.: Explaining violations of properties in control-flow temporal logic. In: Finkbeiner, B., Mariani, L. (eds.) Runtime Verification - 19th Interna- tional Conference, RV 2019, Porto, Portugal, October 8-11, 2019, Proceedings. pp. 202–220. Lecture Notes in Computer Science, Springer (2019)

    work page 2019

  18. [18]

    Formal Methods Syst

    Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interrupt- ible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods Syst. Des.46(3), 197–225 (2015)

    work page 2015

  19. [19]

    In: Ong, C.L., de Queiroz, R.J.G.B

    Diekert, V., Muscholl, A.: On distributed monitoring of asynchronous systems. In: Ong, C.L., de Queiroz, R.J.G.B. (eds.) Logic, Language, Information and Com- putation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings. pp. 70–84. Lecture Notes in Computer Science, Springer (2012)

    work page 2012

  20. [20]

    In: Proceedings of the 11th Australian Computer Science Conference

    Fidge, C.J.: Timestamps in message-passing systems that preserve the partial or- dering. In: Proceedings of the 11th Australian Computer Science Conference. Aus- tralian Computer Science Communications, vol. 10, pp. 56–66 (Feb 1988)

    work page 1988

  21. [21]

    Pact: A Choreographic Language for Agentic Ecosystems

    Gopinathan, K., Feser, J., Naim, M., Tavares, Z., Bingham, E.: Pact: A choreo- graphic language for agentic ecosystems. In: Proceedings of the 2nd International Workshop on Choreographic Programming (CP 2026) (2026), to appear. Also avail- able as arXiv:2605.03143

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  22. [22]

    In: Bruni, R., Dingel, J

    Graf, S., Peled, D.A., Quinton, S.: Monitoring distributed systems using knowledge. In: Bruni, R., Dingel, J. (eds.) Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik, Iceland, June 6-9, 2011. Proceedings. pp. 183–197. Lecture Notes...

    work page 2011

  23. [23]

    In: Katsaros, P., Nenzi, L

    van den Heuvel, B., P´ erez, J.A., Dobre, R.A.: Monitoring blackbox implementa- tions of multiparty session protocols. In: Katsaros, P., Nenzi, L. (eds.) Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, Octo- ber 3-6, 2023, Proceedings. pp. 66–85. Lecture Notes in Computer Science, Springer (2023)

    work page 2023

  24. [24]

    Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang.6(POPL), 1–27 (2022)

    work page 2022

  25. [25]

    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM63(1), 9:1–9:67 (2016)

    work page 2016

  26. [26]

    ITU-T: Recommendation Z.120: Message sequence chart (MSC). Tech. rep., Inter- national Telecommunication Union (2011)

    work page 2011

  27. [27]

    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM21(7), 558–565 (1978)

    work page 1978

  28. [28]

    In: Ciobanu, G., M´ ery, D

    de Le´ on, H.P., Haar, S., Longuet, D.: Distributed testing of concurrent systems: Vector clocks to the rescue. In: Ciobanu, G., M´ ery, D. (eds.) Theoretical Aspects of Computing - ICTAC 2014 - 11th International Colloquium, Bucharest, Roma- nia, September 17-19, 2014. Proceedings. pp. 369–387. Lecture Notes in Computer Science, Springer (2014)

    work page 2014

  29. [29]

    In: Bertrand, N., Dubslaff, C., Kl¨ uppelholz, S

    Leucker, M.: A note on runtime verification of concurrent systems. In: Bertrand, N., Dubslaff, C., Kl¨ uppelholz, S. (eds.) Principles of Formal Quantitative Analysis - Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday. pp. 253–265. Lecture Notes in Computer Science, Springer (2025) 18

    work page 2025

  30. [30]

    Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Alge- braic Methods Program.78(5), 293–303 (2009)

    work page 2009

  31. [31]

    Mahe, E., Bannour, B., Gaston, C., Gall, P.L.: Efficient interaction-based offline runtime verification of distributed systems with lifeline removal. Sci. Comput. Pro- gram.241, 103230 (2025)

    work page 2025

  32. [32]

    In: Parallel and Distributed Algorithms: Proceedings of the International Workshop on Parallel and Distributed Algorithms

    Mattern, F.: Virtual time and global states of distributed systems. In: Parallel and Distributed Algorithms: Proceedings of the International Workshop on Parallel and Distributed Algorithms. pp. 215–226. North-Holland, Amsterdam (1989)

    work page 1989

  33. [33]

    In: Brauer, W., Reisig, W., Rozenberg, G

    Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September

    work page 1986

  34. [34]

    pp. 279–324. Lecture Notes in Computer Science, Springer (1986)

    work page 1986

  35. [35]

    In: Montanari, U., Rolim, J.D.P., Welzl, E

    Meenakshi, B., Ramanujam, R.: Reasoning about message passing in finite state environments. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) Automata, Lan- guages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings. pp. 487–498. Lecture Notes in Computer Science, Springer (2000)

    work page 2000

  36. [36]

    Cambridge University Press (2023)

    Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023)

    work page 2023

  37. [37]

    In: 2015 IEEE International Parallel and Dis- tributed Processing Symposium, IPDPS 2015, Hyderabad, India, May 25-29, 2015

    Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL spec- ifications in distributed systems. In: 2015 IEEE International Parallel and Dis- tributed Processing Symposium, IPDPS 2015, Hyderabad, India, May 25-29, 2015. pp. 494–503. IEEE Computer Society (2015)

    work page 2015

  38. [38]

    In: Platzer, A., Sutcliffe, G

    de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th In- ternational Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. pp. 625–635. Lecture Notes in Computer Science, Springer (2021)

    work page 2021

  39. [39]

    In: K¨ onighofer, B., Torfah, H

    Omer, M., Peled, D., Porat, E., Garg, V.K.: Monitoring distributed systems based on partial order executions with global states. In: K¨ onighofer, B., Torfah, H. (eds.) Runtime Verification - 25th International Conference, RV 2025, Graz, Austria, September 15-19, 2025, Proceedings. pp. 252–273. Lecture Notes in Computer Sci- ence, Springer (2025)

    work page 2025

  40. [40]

    Paduraru, C., Bouruc, P.L., Stefanescu, A.: A trace-based assurance framework for agentic AI orchestration: Contracts, testing, and governance (2026)

    work page 2026

  41. [41]

    Acta Informatica60(2), 145–178 (2023)

    Samadi, M., Ghassemi, F., Khosravi, R.: Decentralized runtime verification of mes- sage sequences in message-based systems. Acta Informatica60(2), 145–178 (2023)

    work page 2023

  42. [42]

    ACM Trans

    Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur.3(1), 30–50 (2000)

    work page 2000

  43. [43]

    In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece

    Sen, K., Vardhan, A., Agha, G., Rosu, G.: Decentralized runtime analysis of mul- tithreaded applications. In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, 25-29 April 2006, Rhodes Island, Greece. IEEE (2006)

    work page 2006

  44. [44]

    Shen, G., Kashiwa, S., Kuper, L.: Haschor: Functional choreographic programming for all (functional pearl). Proc. ACM Program. Lang.7(ICFP), 541–565 (2023)

    work page 2023

  45. [45]

    In: Caltais, G., Schilling, C

    Soueidi, C., Falcone, Y.: Sound concurrent traces for online monitoring. In: Caltais, G., Schilling, C. (eds.) Model Checking Software - 29th International Symposium, SPIN 2023, Paris, France, April 26-27, 2023, Proceedings. pp. 59–80. Lecture Notes in Computer Science, Springer (2023)

    work page 2023

  46. [46]

    In: Barringer, H., Finkbeiner, B., Gurevich, Y., Sipma, H

    Stolz, V., Bodden, E.: Temporal assertions using aspectj. In: Barringer, H., Finkbeiner, B., Gurevich, Y., Sipma, H. (eds.) Proceedings of the Fifth Work- shop on Runtime Verification, RV@CAV 2005, Edinburgh, UK, July 12, 2005. 19 pp. 109–124. No. 4 in Electronic Notes in Theoretical Computer Science, Elsevier (2005)

    work page 2005

  47. [47]

    AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents

    Wang, H., Poskitt, C.M., Sun, J.: Agentspec: Customizable runtime enforcement for safe and reliable LLM agents. CoRRabs/2503.18666(2025)

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  48. [48]

    CoRRabs/2511.00531(2025)

    Weil-Kennedy, C., Rammal, D., Gaston, C., Lapitre, A.: Runtime verification of interactions using automata. CoRRabs/2511.00531(2025)

    work page arXiv 2025

  49. [49]

    In: Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2025, NeurIPS 2025 (2025) 20

    Zhang, Y., Emma, S.Y., En, A.L.J., Dong, J.S.: RvLLM: LLM runtime verification with domain knowledge. In: Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2025, NeurIPS 2025 (2025) 20

    work page 2025