Aug 2026· Proceedings of the ACM on Programming Languages· Vol 10, pp. 66 - 99· 0 citations· 39 references
TL;DR
RunbookFX is presented, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically, and key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability.
Abstract
Large language models are increasingly deployed as autonomous agents for cloud incident response, yet their direct use admits hallucinated diagnoses, unauthorized actions, irreversible changes, and unauditable decision trails. We present RunbookFX, a typed functional domain-specific language that elevates incident response from natural-language suggestions to executable programs whose safety is established statically. The key insight is that incident-response safety decomposes into three interacting dimensions: risk severity, exercised capabilities, and rollback resource availability. RunbookFX formalizes this decomposition as a product effect algebra Risk × K × ℕ whose four cross-component interaction axioms yield domain-specific safety theorems unexpressible in flat effect frameworks; a strong handler parametricity result then transfers these guarantees from a replay handler to any bisimilar live handler, bridging offline verification and production deployment. An LLM proposes candidate programs that a CEGIS-style verifier filters by static type checking and dynamic contract replay. A ∼2,200-line Coq development discharges the product effect algebra, its composition-preservation property, and four core safety theorems: Effect WF Preservation, Progress, single-step No Unauthorized Action, and Rollback Linearity. Of the 27 supporting obligations in the substitution and multi-step layers, 18 now close with Qed—including all Canonical Forms, all effect-operation Inversion lemmas, Value Typing, de Bruijn weakening, and the typing-respecting reduction cases for observe, act, rollback, and the affirmative guard; the remaining nine trace back to the de Bruijn substitution lemma, whose proof skeleton follows Pierce et al. [2019]. Evaluated on RCAEval for root cause analysis and ITBench for end-to-end mitigation, RunbookFX achieves 64% Top-1 RCA accuracy against 53% for the best LLM baseline and 38% mitigation success at 3.3× the official ITBench agent, with zero safety violations and 100% rollback coverage by construction.
This paper proposes SafeKeep, an inference-time safeguard that decouples safety judgment from tool execution: it assesses requests using flattened textual tool specifications while retaining the original schema-formatted specifications for execution.
Minghui Pan, Jiayuxuan Yang, Yuanyuan Yuan et al.· 0 citations
This work presents FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution that utilizes an LLM-guided Permission Intermediate Representation to translate ambiguous natural-language tasks into structured constraints.
Yifan Zhang, Xinkui Zhao, Sai-Da Liu et al.· 3 citations
Large language models (LLMs) are increasingly used to interpret operational evidence and assist incident response in cloud-native microservice systems. However, recovery-oriented use cases require more than identifying a root cause. After observing symptoms and diagnosing a fault, an operator or agent must translate the diagnosis into a concrete recovery action, apply it to an admissible target, and verify that service health has been restored. Existing RCA and log-analysis evaluations are well-suited to diagnosis, but they do not characterize this subsequent action decision. This paper presents R2Act, a recovery-action evaluation framework for post-diagnosis incident response. R2Act defines an incident schema, quality gate, action-space representation, recovery-validity metrics, offline evaluator, and live-replay protocol. We instantiate the framework as a benchmark dataset of 302 quality-audited Kubernetes incidents from \system. Each incident provides synchronized multi-modal observations, root-cause labels, an incident-specific action space, and annotated valid and invalid recovery plans. We evaluate heuristic, supervised, RCA-oriented, deep log, and LLM-based methods. The strongest RAG-based LLMs reach 91.4\%--99.7\% root-cause service accuracy, yet their recovery validity remains only 36.8\%--60.3\%. Even when both the root-cause service and fault type are correct, recovery-oriented methods still choose invalid actions for 39.5\%--62.0\% of correctly diagnosed incidents. Overall, this work reveals that many recovery failures arise not from missing diagnostic knowledge, but from the difficulty of translating diagnostic evidence into valid recovery actions and admissible targets. This work provides a reproducible, simplified starting point for research and evaluation.
Jiaxing Qi, Zhongzhi Luan, Hongyu Zhang et al.· 0 citations
RedAgentBench is introduced, an executable framework for autonomous red-teaming and faithful measurement that shows that executable evaluation can improve safety measurement and identify actionable intervention points.
Zixing Chen, Xingyuan Liu, Jie Zhu et al.· 0 citations
LLM agents deployed in practical workflows routinely mix private context, untrusted tool and web outputs, and external side effects. While information-flow control (IFC) provides structural defenses against prompt injection, data exfiltration, and confused-deputy attacks, conventional IFC relies on monotone taint tracking that either over-blocks benign operations or permanently strands downstream execution once an agent ingests unvetted data. We present APPA (Agentic Permissions Policy Algebra), which turns agent IFC from an abort-only barrier into a policy-governed recovery system. APPA enforces a dual-phase reference monitor at tool dispatch and protocol gateways (e.g., Model Context Protocol): before tool execution, it prospectively evaluates composite label restrictions and workflow history; upon completion, it validates realized outputs before context admission. For incremental rollout across unannotated tools, APPA incorporates gradual security typing with bounded cast resolution. To inspect untrusted data without poisoning primary agent context, APPA introduces on-demand trajectory confinement: disposable child branches absorb taint locally and exit through shape-bounded channels (attest-schema) with exact parent-label and transcript preservation, avoiding permanently partitioned multi-agent infrastructure. We prove core safety invariants: no-laundering gradual resolution, branch boundary isolation, and recovery containment against prompt-injected models. Across 6,600 controlled benchmark episodes spanning OWASP AgentThreatBench and enterprise workflows (Bench-Corp), APPA sustains 64.2-91% utility with zero observed attacks across 1,320 guarded episodes, establishing a practical defense for deployed tool-using agents.
Arseny Kravchenko, V. Liventsev, I. Konstantinov et al.· 1 citation
ContainmentBench, a sandboxed benchmark comprising a 504-scenario specification dataset, a shared rollout-trace schema, and stage-scoped metrics for endpoint violations, logged propagation, and explicitly authorized taint-exposed proposals that commit, is introduced.