一句话：提出类型化函数式 DSL RunbookFX，用乘积效应代数把事故响应安全分解为风险、能力、回滚三维，并以 Coq 机化证明保障 LLM 合成程序的安全性。
云事故响应中直接使用 LLM 智能体会带来幻觉诊断、未授权操作、不可逆变更与不可审计决策链。RunbookFX 是一个类型化函数式 DSL，把响应从自然语言建议提升为安全性可静态确立的可执行程序。作者将响应安全分解为风险严重度、可执行能力与回滚资源三维，形式化为乘积效应代数 Risk × K × ℕ；四条跨分量交互公理给出扁平效应框架无法表达的安全定理，强 handler 参数化结果把保证从 replay handler 迁移到任意互模拟的 live handler。LLM 提出候选程序，CEGIS 式验证器以静态类型检查与动态契约重放筛选。约 2200 行 Coq 开发机化了该代数与四条核心安全定理。在 RCAEval 与 ITBench 上，Top-1 根因准确率 64%、缓解成功率 38%（为官方 agent 的 3.3 倍），且零安全违规、100% 回滚覆盖。
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.
@article{XiaoLG26,
title = {RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation},
author = {Yifan Xiao and Shijie Li and Yuhao Ge},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828675}
}