Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety

Ruiyang Zhang

REVIEW 4 major objections 5 minor 15 references

Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that the recall of any fixed-invariant LTL/FSA safety monitor for LLM agents is bounded by the top-k concentration of the attack distribution, and that a pre-deployment Shannon-entropy test can predict which backends the m

desk verdict A paper with a false core theorem: the entropy-coverage bound is a trivial inequality, the entropy implication is false, and the validation is partly circular. read the letter →

arxiv 2608.01388 v1 pith:AQWWNNOB submitted 2026-08-02 cs.CR cs.AIcs.LG

Ruiyang Zhang This is my paper · ORCID

classification cs.CRcs.AIcs.LG

keywords LTLruntimemonitorsattackdistributionentropyFSAcoverageboundsLLMagentsafetyformalverificationlimitsintelligentsystemssecurityShannonpre-deploymenttest

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Formal safety monitors for LLM agents encode forbidden tool-call patterns as LTL formulas and halt an agent when one fires. This paper tries to explain a recurring empirical anomaly: the identical monitor blocks 68–75% of attacks on one model family and 6–13% on another, with retraining making no difference. Its answer is that recall is capped by how concentrated the attack distribution is; when attacks split across many structurally distinct trigger-completion patterns, no fixed set of invariants of practical size can cover them. The paper derives an inequality bounding recall by the sum of the $k$ most probable pattern probabilities, validates it across eight frontier architectures, and proposes a pre-deployment entropy test that predicts monitor usefulness from 50–100 attack samples. If correct, it gives practitioners a cheap, architecture-agnostic way to decide when formal monitors are worth deploying and when learned monitors are required.

What carries the argument

The load-bearing mechanism is the top-$k$ concentration $C_k(D) = \sum_{i=1}^k p^*_i$ of the attack distribution $D$ over trigger-completion pairs $(T, t_c)$, where $p^*_i$ are the pattern probabilities in decreasing order. Theorem 1 bounds monitor recall by $C_n(D)$. The monitor itself is a set of LTL bounded-finally invariants $\phi = G(T_{\text{trig}} \rightarrow F_{[1,k]}(t_{\text{comp}}))$ compiled to sliding-window FSAs; Theorem 3 gives the sample-size guarantee for the plug-in entropy estimator. Together these convert a deployment failure into a measurable quantity.

What would settle it

A direct counter-check: take any attack distribution with one pattern at probability 0.6 and a long tail of 20 patterns at 0.02 each. Then $H(D) \approx 1.53$ bits while $C_1(D) = 0.6$, so high Shannon entropy does not by itself force small top-$k$ concentration. Observing such a distribution in the wild with high monitor recall despite $H > 1$ bit would break the paper's stated equivalence. A more direct refutation: on a fresh backend, measure observed recall and the empirical top-8 concentration $C_8(\hat{D})$; if recall exceeds $C_8(\hat{D})$, Theorem 1 is false.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 1: for any fixed-invariant FSA monitor $M$ with $n$ invariants and any attack distribution $D$ over trigger-completion patterns, $R(M,D) \le C_n(D)$, where $C_n(D)$ is the total probability of the $n$ most frequent patterns. The authors present this as a coverage ceiling that survives retraining, since retraining changes only which $n$ patterns the invariants target, not the distribution's concentration. They add a duality theorem asserting $H(D) \ge H_b(C_n(D))$, so $H(D) < 1$ bit forces $C_n(D) > 0.5$, and a sample-complexity theorem that estimates $H(D)$ from $N$ i.i.d. trajectories with a Hoeffding-style error bound. Empirically, they report entropy a

Load-bearing premise

The load-bearing premise is that the attack-pattern distribution measured from attacks the monitor did not block (Section IV, Type II misses) is the same distribution that governs all attacks the monitor will face; if the monitor's own invariants shape which trajectories are recorded, the entropy estimate and the pre-deployment test describe misses, not attacks.

Editorial extensions

If this is right

Retraining a fixed FSA monitor cannot lift recall above $C_n(D)$; on high-entropy backends the near-zero recall is a structural limit, not a data or tuning failure.
A pre-deployment entropy test using 50–226 trajectories can classify a backend as FSA-suitable ($H < 0.5$ bits), grey zone, or FSA-insufficient ($H > 2.0$ bits), guiding monitor selection before production.
Model capability scores are not a useful guide: the paper finds Elo explains no significant variance in monitor coverage, so upgrading the model is not a coverage fix.
For high-entropy backends, probabilistic or learned monitors are the indicated replacement, because the bound applies to any fixed pattern-matching approach, not only LTL/FSA monitors.
The same top-$k$ ceiling applies to regex monitors, signature rules, and behavioral allowlists, so the entropy test doubles as a general monitor-selection criterion.
Rising entropy over time on a previously low-entropy backend could serve as a drift alarm, signaling that the formal monitor's coverage ceiling is falling.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The same entropy test should transfer to any discrete action space — file system calls, permission grants, API routes — because the bound depends only on pattern probabilities, not on the semantics of tool calls; applying it outside AgentDojo is a direct testable extension.
Deployment teams could run the entropy estimate periodically as a drift alarm: a rising $H(\hat{D})$ signals that a backend is moving toward the grey zone and the formal monitor's ceiling is dropping.
A portfolio defense is implied: keep FSA monitors on low-entropy backends, route high-entropy backends to probabilistic or learned monitors, and re-estimate entropy after model updates, since a new checkpoint can shift the attack distribution without changing capability scores.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

I read the Zhang paper. Here's the short version: the empirical finding is real enough to pay attention to, but the theory section does not hold, and the validation is partly circular. I wouldn't trust the pre-deployment test as stated.

What's genuinely interesting: the observation that the same LTL/FSA monitor has wildly different recall across model families, and that this difference tracks something like the dispersion of attack patterns rather than capability scores. The eight-point correlation (r=-0.87) with leave-one-out is worth a look, though n=8 is thin. The idea of a quick pre-deployment entropy test is practically appealing.

The problem is the central theorem. Theorem 1 (R ≤ C_n) is true but it's just the definition of recall: with n patterns you can cover at most the n most probable ones. It says nothing about entropy. Corollary 1 claims H(D) ≥ log2(n+1) implies C_n ≤ n/(n+1). That's false: take p1=0.6 and a long tail of smaller probabilities; H grows without bound as the tail lengthens while C_1 stays 0.6. Theorem 2 has a similar inversion error: H_b(p)<1 for every p ≠ 0.5, so H<1 bit doesn't imply C_n>0.5. These aren't minor slips; they're the load-bearing pieces of the 'high entropy means no monitor can work' story.

There's also a circularity in the evaluation. Entropy is estimated from Type II misses—attacks the monitor failed to block. That distribution is conditioned on the very monitor whose recall you're predicting. If the monitor blocks some patterns, the remaining miss distribution isn't the attack distribution. The claim that 'Gemini retraining changes nothing' (0.0 pp) may be true but it's a property of the bound, not a new empirical result, since the bound is a property of the distribution.

Theorem 3's sample-complexity proof says E[ℓ_i]=H(D), but ℓ_i uses the empirical cluster probabilities from the same sample; its expectation is a cross-entropy, not the true entropy, so the claimed guarantee doesn't follow. The thresholds H*_low, H*_high and the clustering θ are fit to the same data.

The paper is clearly written and engages with the right literature, but the theory needs substantial revision. A serious referee could help the author recast this as a heuristic observation; as is, the central claim is false.

Referee Report

4 major / 5 minor

Summary. The paper claims a structural information-theoretic limit for fixed-invariant LTL/FSA monitors: monitor recall R(M,D) is bounded by the top-n concentration of the attack pattern distribution (Theorem 1), and that high Shannon entropy of the attack distribution implies that this bound is small (Corollary 1 and the abstract's equivalence). It reports an empirical study on eight LLM backends, with recall from an 8-invariant monitor mined from GPT-4o-mini attacks, entropy estimated from Type-II misses, and a strong correlation (r=-0.87) between entropy and recall, plus a proposed pre-deployment entropy test and a sample-complexity guarantee (Theorem 3).

Significance. If valid, the paper would contribute a practically useful selection criterion: measure attack entropy before deployment and choose between fixed-pattern formal monitors and probabilistic/neural monitors. The authors deserve credit for the explicit robustness analyses (bootstrap, leave-one-out), for separating the theoretical bound from FPR and distribution-mismatch gaps, and for reporting the per-architecture data in Table I. However, the central theoretical bridge from entropy to coverage is not established: the claimed high-entropy implies low-concentration step is false. In addition, the empirical distribution used for the correlation is itself conditioned on the same monitor's misses, so the pre-deployment test lacks the independence needed for the structural reading. The contribution therefore reduces to a descriptive correlation with an unproven bound.

major comments (4)

[§III.B, Corollary 1 and Abstract] The claim that high Shannon entropy H(D) implies small top-k coverage is false. Corollary 1 states that if H(D)>=log2(n+1) then C_n(D)<=n/(n+1), but this does not follow. For n=1, let p1=0.6 and spread the remaining 0.4 uniformly over M atoms. For M=10, H≈2.30>=1 while C1=0.6>0.5. For n=8, take p1...p8=0.1125 (sum 0.9) and spread the remaining 0.1 over many atoms; H can be made at least log2(9)≈3.17 while C8=0.9>8/9. Thus Theorem 1, a definitional ordering of probabilities, does not imply the entropy-coverage bound claimed in the abstract.
[§III.C, Theorem 2] The inequality H(D)>=H_b(C_n(D)) follows by grouping, but the stated consequence 'if H(D)<1 bit then C_n(D)>0.5' is not proved by the given reasoning. H_b(p)<1 holds for every p in (0,1) except p=0.5, including p<0.5, so the inversion is invalid. Moreover, even if C_n>0.5, this is an upper bound on the best possible monitor, not a guarantee that 'any FSA monitor achieves better-than-random coverage'; a particular monitor can cover low-probability patterns and have recall far below C_n. The conclusion needs a separate proof or should be removed.
[§IV, Attack pattern extraction] The attack-pattern distribution is computed from 'attack trajectories that were not blocked by the monitor (Type II misses)'. This distribution is conditioned on the very monitor whose recall is the outcome variable. If the monitor blocks concentrated patterns, the remaining miss distribution becomes higher-entropy by construction, and a monitor with low recall contributes many varied misses. The pre-deployment test in §VI requires an estimate of the full attack distribution independent of the deployed monitor; no such independent sample is provided. This conditioning is load-bearing for contributions C2 and C3 and is not listed among the threats to validity in §VII.D.
[§VI.C, Theorem 3] The sample-complexity proof asserts E[ℓ]=H(D) for ℓ_i=-log2 \hat p_{c(τ_i)}. This is not exact: \hat p_c is computed from the full sample and includes τ_i, so the plug-in estimator is biased and its expectation is not the true entropy. The variables ℓ_i are also not fixed independent contributions in the way required by the stated Hoeffding application. Equation (10) is therefore not established. While this is a secondary issue compared with Corollary 1, it affects contribution C3's formal guarantee.

minor comments (5)

[§II.B] The sentence 'For fixed k, low H implies high C_k' is true in one direction only, but the paper later uses the reverse direction when calibrating thresholds in §VI.B. The thresholds should be justified empirically, not derived from an unproved entropy-concentration equivalence.
[§III.B] The proof of Theorem 1 asserts that formulas are 'semantically disjoint at the pattern level' and that each formula detects exactly one trigger-completion pattern. The definition of patterns is tailored to this claim; please clarify whether an LTL formula of form (1) can cover multiple trigger-completion pairs and how the bound changes in that case.
[Table I / §IV] Notation is inconsistent: the table lists C_8(\hat D) and H(\hat D), while the theorems use D. State explicitly that the empirical quantities estimate the theoretical distribution D, and note the Type-II-miss conditioning in the table caption.
[§IV] The parameters 'support σ=0.02' and 'FPR threshold φ=0.05' are not defined. Define how support and FPR are measured for mined invariants.
[§I] The phrase 'theater gap' appears in the introduction and §III.D. This may be a typo for 'the gap' or 'therapy gap'; please clarify the intended term.

Circularity Check

3 steps flagged · score 8.0 of 10

The entropy-coverage bound is a definitional rearrangement of recall; the claimed entropy-to-coverage equivalence is assumed and false; and the empirical entropy values are computed from the same monitor's Type II misses, making the pre-deployment test calibrated on the data it claims to predict.

self definitional [Section III.B, Definition 1 and Theorem 1]
"Definition 1 (Monitor Recall). The recall of monitor M under attack distribution D is: R(M,D) = Σ_{(T,t_c)∈Π} p(T,t_c)·1[M covers (T,t_c)] ... Theorem 1 (Entropy-Coverage Bound). For any fixed-invariant FSA monitor M containing n invariants and attack distribution D over patterns Π: R(M,D) ≤ C_n(D) = Σ_{i=1}^n p*_i"

The 'bound' is a restatement of Definition 1. Recall is defined as the total probability of the patterns the monitor covers. A monitor with n invariants covers at most n patterns. The n largest probabilities are, by definition, the maximum possible total probability of any n-element subset of patterns. The proof explicitly says the maximum is achieved by the n most probable patterns. No property of Shannon entropy is used. Thus Theorem 1 cannot fail for any monitor and adds no information-theoretic content; calling it an entropy-coverage bound renames a definitional ordering as a discovery.
other [Abstract and Section III.B, Corollary 1]
"Equivalently, high Shannon entropy H(D) implies that Cov_k(D) is small for any tractable k. / Corollary 1 ... When H(D) ≥ log2(n+1), we have C_n(D) ≤ n/(n+1)"

The 'equivalently' is not derived from Theorem 1; it is an assumed bridge between entropy and top-k concentration, and it is false. A distribution with p1=0.6 and p_i=0.4/M for i=2..M+1 has H(D) arbitrarily large while C_1(D)=0.6 and C_n(D)≥0.6 for every n. The paper's central prediction—that high-entropy attack distributions exceed the coverage capacity of any fixed invariant set—therefore rests on an unproven and incorrect assertion that is exactly the conclusion the paper needs. The entropy-coverage result is an input, not a consequence.

1 more flagged steps

fitted input called prediction [Section IV 'Attack pattern extraction' and Section V, Table I]
"Attack pattern extraction. For each backend, we extract trigger-completion pairs (T, tc) from attack trajectories that were not blocked by the monitor (Type II misses). ... Entropy computation. For each architecture A, we compute: 1) The empirical attack pattern distribution D_hat_A from observed trajectories 2) Shannon entropy H(D_hat_A) via (2)"

The entropy values in Table I are computed from the miss set of the very monitor whose recall they are said to predict. H(D_hat) is therefore H(attacks | monitor did not block), a quantity defined by the monitor's own coverage decisions. A high-recall monitor leaves a small residual miss distribution; a low-recall monitor leaves almost the full attack distribution. Correlating this monitor-conditioned entropy with the same monitor's recall is not an independent architectural prediction. The pre-deployment test in Section VI is calibrated on these same monitor-conditioned entropies and then presented as predicting the monitor, so the 'prediction' is fitted to the data it claims to forecast.

full rationale

The paper's central theoretical contribution, Theorem 1, is definitional: recall is defined as the sum of probabilities of covered patterns, and a monitor with n invariants covers at most n patterns, so R ≤ C_n is true by construction. The paper's additional claim that high entropy implies small C_k is not a consequence of Theorem 1 and is mathematically false; a distribution can have arbitrarily high entropy while retaining a large top-k mass. The empirical validation is also contaminated: Section IV computes entropy from Type II misses of the same monitor whose recall is being predicted, so the correlation in Table I reflects the monitor's conditioning of the observed sample. The pre-deployment entropy test is then calibrated on this monitor-conditioned data. There is no load-bearing self-citation chain; all references are external. Some independent empirical content may exist in the raw correlation, but as presented the theoretical bound reduces to a definition, the entropy implication is an assumed (and false) premise, and the empirical prediction is fitted to the same monitor's miss distribution. This warrants a circularity score of 8.

Assumptions & free parameters 4 free parameters · 4 assumptions · 1 invented entities

The bound's content is carried by definitions, with a false entropy implication added on top. The empirical correlation depends on post-hoc thresholds and on entropy estimated from the monitor's own misses.

free parameters (4)

clustering threshold theta = 0.4
Chosen as the 'standard midpoint' of the normalized Jaccard range; stability is claimed for theta in [0.3,0.5] but per-architecture results are not shown.
H*_low threshold = 0.5 bits
Calibrated from Table I to separate architectures with greater than 50 percent recall.
H*_high threshold = 2.0 bits
Calibrated from Table I to separate architectures with near-zero recall.
invariant count n = 8
The number of LTL invariants mined from 847 gpt-4o-mini trajectories; the bound C_n and the entropy thresholds depend on this count.

assumptions (4)

standard math Bounded-finally LTL formulas of the form G(T -> F[1,k] t_c) are monitorable from finite prefixes.
Section II.C invokes classical runtime verification theory; accepted background.
domain assumption Each LTL formula detects exactly one trigger-completion pattern, no two formulas cover the same pattern, and each attack belongs to at most one pattern.
Section III.B uses this to assert |S| <= n and additivity of recall; this defines away multi-pattern attacks and shared coverage.
ad hoc to paper The empirical cluster distribution trained on Type II misses is representative of the full attack distribution.
Section IV computes entropy from attacks the monitor failed to block, then uses that entropy as the predictor of coverage for the same monitor.
ad hoc to paper High Shannon entropy forces small top-k concentration in the direction used by Corollary 1.
This is the load-bearing step that is false: H(D) >= log2(n+1) can hold while C_n(D) > n/(n+1).

invented entities (1)

Atomic trigger-completion pattern
purpose: Defines the attack distribution and the top-k concentration bound.
No independent falsifiable handle; mutual exclusivity is imposed by definition rather than demonstrated from observed trajectories.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety." pith.science (2026). https://pith.science/paper/AQWWNNOB

@misc{pith2026260801388,
  author       = {Pith},
  title        = {Pith review of: Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AQWWNNOB}},
  note         = {Machine review of arXiv:2608.01388}
}

read the original abstract

Runtime safety monitors based on Linear Temporal Logic (LTL) and finite automata (FSA) are increasingly deployed to intercept unsafe tool-call sequences in LLM agents. Yet the same monitor achieves 68-75% attack coverage on some model architectures and near-zero on others, with no explanation from capability scores, training data, or prompt design. We provide the missing theory. We prove that the recall of any fixed-invariant FSA monitor is bounded above by the concentration of the attack distribution: the fraction of attacks covered by the k most frequent trigger-completion patterns. When attacks concentrate (low Shannon entropy), a small fixed invariant set achieves high recall; when they disperse across many structurally distinct patterns (high entropy), no fixed invariant set of tractable size can, regardless of how the invariants were derived. We validate this entropy-coverage bound across eight frontier LLM architectures. GPT-class and DeepSeek backends yield highly concentrated attacks (H ~ 0.24 bits; one pattern covers 96%), explaining 68-75% recall; Gemini variants yield high-entropy distributions (H ~ 2.81 bits; 7 clusters each <= 7%), explaining near-zero recall (6-13%), invariant to architecture-matched retraining. Entropy accounts for 76% of variance in coverage (Pearson r = -0.87, p = 0.005, 95% CI [-0.98, -0.78]), holding under leave-one-out (r in [-0.91, -0.82]). We introduce a pre-deployment entropy test that predicts monitor coverage from a small attack sample, enabling architecture-aware monitor selection before deployment. The bound and test are architecture-agnostic and apply to any FSA-based runtime monitor over discrete action sequences.

Figures

Figures reproduced from arXiv: 2608.01388 by the authors.

**Figure 1.** Attack entropy H(Dˆ) vs. monitor recall across eight architectures (Pearson r = −0.87, p = 0.005). Elo capability score is not a significant predictor (|ρ| < 0.35, p > 0.4), confirming entropy as the operative factor. TABLE II: Robustness analysis of entropy-recall correlation (r = −0.87, n = 8). Bootstrap and LOO confirm the relationship is not driven by any single architecture. Analysis Result Verdict Pearson r (f… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 9 canonical work pages

[1]

Enforcing temporal constraints for LLM agents,

A. Kamath, S. Zhang, C. Xu, S. Ugare, G. Singh, and S. Misailovic, “Enforcing temporal constraints for LLM agents,”arXiv:2512.23738, 2025, system presented: Agent-C

arXiv 2025
[2]

AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents,

H. Wang, C. M. Poskitt, and J. Sun, “AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents,” inICSE, 2026

work page 2026
[3]

ProbGuard: Probabilistic runtime monitoring for LLM agent safety,

H. Wang, C. M. Poskitt, J. Wei, and J. Sun, “ProbGuard: Probabilistic runtime monitoring for LLM agent safety,”arXiv:2508.00500, 2025

arXiv 2025
[4]

AgentSentry: Mitigating indirect prompt injection in LLM agents via temporal causal diagnostics and context purification,

T. Zhang, Y . Xu, J. Wang, K. Guo, X. Xu, B. Xiao, Q. Guan, J. Fan, J. Liu, Z. Liu, and H. Hu, “AgentSentry: Mitigating indirect prompt injection in LLM agents via temporal causal diagnostics and context purification,”arXiv:2602.22724, 2026

arXiv 2026
[5]

LTL-based runtime verification framework for cyber-attack anomaly prediction in cyber-physical systems,

A. J. Akandeet al., “LTL-based runtime verification framework for cyber-attack anomaly prediction in cyber-physical systems,”Computers & Security, vol. 155, 2025

work page 2025
[6]

Efficient mining of temporal safety properties for intrusion detection in industrial control systems,

O. Koucham, S. Mocanu, G. Hiet, J.-M. Thiriet, and F. Majorczyk, “Efficient mining of temporal safety properties for intrusion detection in industrial control systems,” inSAFEPROCESS, 2018

work page 2018
[7]

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

C. Mascle, D. Neider, M. Schwenger, P. Tabuada, A. Weinert, and M. Zimmermann, “From LTL to rLTL monitoring: Improved monitora- bility through robust semantics,”Formal Methods in System Design, 2022, arXiv:1807.08203

work page Pith review arXiv 2022
[8]

AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents,

E. Debenedetti, J. Zhang, M. Balunovi ´c, L. Beurer-Kellner, M. Fischer, and F. Tram `er, “AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents,” inNeurIPS, 2024

work page 2024

Show all 15 references

[9]

GPT-4.1: Technical report,

OpenAI, “GPT-4.1: Technical report,” OpenAI, Tech. Rep., 2025. [Online]. Available: https://openai.com/index/gpt-4-1/

2025
[10]

Claude Sonnet 4 model card,

Anthropic, “Claude Sonnet 4 model card,” Anthropic, Tech. Rep., 2025. [Online]. Available: https://www.anthropic.com/claude/sonnet

2025
[11]

Gemini 2.5 Flash: Technical report,

Google DeepMind, “Gemini 2.5 Flash: Technical report,” Google DeepMind, Tech. Rep., 2025. [Online]. Available: https://deepmind. google/models/gemini/flash/

2025
[12]

The Llama 3 herd of models,

Meta AI, “The Llama 3 herd of models,” Meta AI, Tech. Rep., 2024, arXiv:2407.21783

2024 arXiv
[13]

Mining anomalies using traffic feature distributions,

A. Lakhina, M. Crovella, and C. Diot, “Mining anomalies using traffic feature distributions,” inACM SIGCOMM, 2005

2005
[14]

AgentVerify: Compositional formal verification of AI agent safety properties via LTL model checking,

E. Fang, “AgentVerify: Compositional formal verification of AI agent safety properties via LTL model checking,”Preprints.org, 2026, dOI:10.20944/preprints202604.1029.v1

2026
[15]

Mapping the exploitation surface: A 10,000-trial taxonomy of what makes LLM agents exploit vulnerabilities,

C. Mouzouni, “Mapping the exploitation surface: A 10,000-trial taxonomy of what makes LLM agents exploit vulnerabilities,”arXiv:2604.04561, 2026

2026 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [1]

Enforcing temporal constraints for LLM agents,

A. Kamath, S. Zhang, C. Xu, S. Ugare, G. Singh, and S. Misailovic, “Enforcing temporal constraints for LLM agents,”arXiv:2512.23738, 2025, system presented: Agent-C

arXiv 2025

[2] [2]

AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents,

H. Wang, C. M. Poskitt, and J. Sun, “AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents,” inICSE, 2026

work page 2026

[3] [3]

ProbGuard: Probabilistic runtime monitoring for LLM agent safety,

H. Wang, C. M. Poskitt, J. Wei, and J. Sun, “ProbGuard: Probabilistic runtime monitoring for LLM agent safety,”arXiv:2508.00500, 2025

arXiv 2025

[4] [4]

AgentSentry: Mitigating indirect prompt injection in LLM agents via temporal causal diagnostics and context purification,

T. Zhang, Y . Xu, J. Wang, K. Guo, X. Xu, B. Xiao, Q. Guan, J. Fan, J. Liu, Z. Liu, and H. Hu, “AgentSentry: Mitigating indirect prompt injection in LLM agents via temporal causal diagnostics and context purification,”arXiv:2602.22724, 2026

arXiv 2026

[5] [5]

LTL-based runtime verification framework for cyber-attack anomaly prediction in cyber-physical systems,

A. J. Akandeet al., “LTL-based runtime verification framework for cyber-attack anomaly prediction in cyber-physical systems,”Computers & Security, vol. 155, 2025

work page 2025

[6] [6]

Efficient mining of temporal safety properties for intrusion detection in industrial control systems,

O. Koucham, S. Mocanu, G. Hiet, J.-M. Thiriet, and F. Majorczyk, “Efficient mining of temporal safety properties for intrusion detection in industrial control systems,” inSAFEPROCESS, 2018

work page 2018

[7] [7]

From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics

C. Mascle, D. Neider, M. Schwenger, P. Tabuada, A. Weinert, and M. Zimmermann, “From LTL to rLTL monitoring: Improved monitora- bility through robust semantics,”Formal Methods in System Design, 2022, arXiv:1807.08203

work page Pith review arXiv 2022

[8] [8]

AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents,

E. Debenedetti, J. Zhang, M. Balunovi ´c, L. Beurer-Kellner, M. Fischer, and F. Tram `er, “AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for LLM agents,” inNeurIPS, 2024

work page 2024