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.

Multi-head-self-attention (MHSA) mechanisms achieve state-of-the-art (SOTA) performance across natural language processing and vision tasks. However, their quadratic dependence on sequence lengths has bottlenecked inference speeds. To circumvent this bottleneck, researchers have proposed various sparse-MHSA models, where a subset of full attention is computed. Despite their promise, current sparse libraries and compilers do not support high-performance implementations for diverse sparse-MHSA patterns due to the underlying sparse formats they operate on. These formats are either too specialised, failing to cover a wide-range of sparse patterns, or too general, incurring high metadata overhead when computing on the moderately sparse (10-50% non-zeros) matrices present in sparse-MHSA. We bridge this gap, achieving both generality and performance, by proposing a novel sparse format: affine-compressed-sparse-row (ACSR) and supporting code-generation scheme, SPLAT, that generates highperformance implementations for diverse sparse-MHSA patterns on GPUs. Core to our proposed format and code generation algorithm is the observation that common sparse-MHSA patterns have uniquely regular geometric properties. These properties, which can be analyzed just-in-time, expose novel optimizations and tiling strategies that SPLAT exploits to generate high-performance implementations for diverse patterns. To demonstrate SPLAT’s efficacy, we use it to generate code for various sparse-MHSA models, achieving speedups of up-to 2.05x and 4.05x over hand-written kernels written in Triton and TVM respectively on A100 GPUs in single-precision.