主题: 实践部分 4. LLM 决斗：验证者与实现者在形式化断言中的对决
难度等级: 中级
预计学习时间: 3-4 小时
前置要求: 对 JSON Schema 和数据验证格式有基本了解
熟悉 BDD（行为驱动开发）方法及 Given/When/Then 语法
具有 REST API、Webhook 和监控系统（例如 Prometheus、Grafana、PagerDuty）的工作经验
理解自动伸缩（autoscaling）原理和事件管理
学习目标: 描述在对抗性验证（LLM 决斗）过程中验证者和实现者的角色。
学习如何为规范的操作边界检查构造最小反例。
掌握通过包含操作限制（配额、爆炸半径）来扩展 JSON Schema 的实践。
实施 validation.md 日志协议，以记录先例和新规则（next_guard）。
配置本地 CI 流水线，通过 run_duel.py 自动检查规范。
概述: 本模块致力于介绍使用 LLM 进行形式化规范对抗性验证的方法——即所谓的「LLM 决斗」。在实际的自动事件解决系统中，输入数据（例如 Webhook）可能在形式上是正确的，但由于违反了操作边界而导致灾难性后果。在本课程中，我们考虑一种架构，其中一个语言模型（验证者）试图找到最小的破坏性反例，而另一个（实现者）修复规则和 JSON Schema，使系统稳定地拒绝危险操作。通过 autoscale_200pct 案例研究，您将学习如何将检查从纯逻辑层面转移到操作层面。
关键概念: LLM 决斗：一种对抗性验证方法，其中角色在两个 LLM 之间分配：验证者寻找漏洞（反例），而实现者修复规范和代码。
最小反例：包含恰好使违规消失所必需的字段和值的输入数据。它在 JSON Schema 上有效，但违反了已批准的 Then 规则。使用最小反例可以避免回归并精确定位问题。
操作边界：真实基础设施的限制（配额、速率限制、影响半径、去重），这些限制必须与数据类型一起在规范中形式化。
Given/when/then：行为契约的严格记录格式。Given（初始状态）、When（输入影响，例如 Webhook）、Then（预期结果或防护）。
Validation.md：存储决斗历史的日志文件。包含 duel_id、assertion_id、反例、裁决和生成的 next_guard。
Next guard：在成功反例之后制定的新安全规则，系统在所有后续运行中都必须检查该规则。
协调器（coordinator）：LLM 决斗过程中的仲裁者，当验证者和实现者在给定轮数内无法达成一致时介入，并将事件状态转为 DEFERRED。
练习题: 名称: 运行 LLM 决斗的练习性执行
问题: 您需要检查 autoscale_spec.yaml 规范对增加副本数 200% 攻击的韧性。运行本地决斗脚本并分析基本裁决。
解决方案: 1. 打开终端并切换到示例目录：cd book2/examples/tribunal。2. 执行命令：python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json。3. 打开生成的文件 out/duel.json。找到 autoscale_counter_200pct 案例，并确认裁决已变为 PASS（如果规范尚未修补，则分析 FAIL）。
难度: beginner
名称: 构建最小反例
问题: 系统收到一个用于重启 Pod 的 Webhook，参数为：readiness=24/25、stateful=true、backup_verified=false。请以 JSON 格式构建一个最小反例，证明应阻止 dry-run。
解决方案: 对于最小反例，需要仅保留直接影响安全逻辑的字段。{ "readiness": 24, "stateful": true, "backup_verified": false }。我们排除了 namespace、pod_id 和其他元数据，因为没有它们逻辑违规（在没有 stateful Pod 备份的情况下尝试 dry-run）仍然存在，但分析变得更有针对性。
难度: intermediate
名称: 将 next_guard 集成到 validation.md
问题: 实现者成功保护了规范免受重复触发的 Webhook（去重）的影响。请使用课程中描述的原则，以 Given/When/Then 格式将决斗结果记录在 validation.md 中。
解决方案: 在 validation.md 中添加以下记录：
assertion_id: DEDUP-SCALE-01 counterexample: "两个 scale_up_percent=100 的 Webhook 以 1 秒的间隔到达" verdict: PASS next_guard: "Given 去重窗口为 2 秒 When 收到重复的伸缩 Webhook Then executed_delta 不会重复增加，并返回诊断代码 DUPLICATE_WEBHOOK_IGNORED"。
难度: advanced
案例研究: 名称: AgentClinic 生产环境中的关键事件：Autoscale 200%
场景: 集群中运行着 appointments-api 服务。当前 CPU 使用率为 98%，运行 12 个副本。配额允许再增加 3 个（集群限制为 15 个副本）。此时自动化系统发送 Webhook：「将副本数增加 200%」。
挑战: 形式上，输入数据完全正确——scale_up_percent 字段已正确填写，类型匹配。但是，执行此命令将请求创建 24 个额外副本，导致配额耗尽、限制被违反，并在伸缩操作中途导致服务崩溃。
解决方案: 使用 LLM 决斗技术。验证者生成了最小反例：{ current_replicas: 12, remaining_quota: 3, scale_up_percent: 200 }。实现者在 JSON Schema 和逻辑中添加了操作边界：引入了公式 allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) 以及带有 hard_block / soft_clamp 值的 clamp_policy 策略。
结果: 自动伸缩器不再因基础设施层面无效（但形式上正确）的请求而崩溃。当收到 200% 的请求时，系统安全地将步长限制为 +3 个副本（soft_clamp），并将诊断代码 QUOTA_EXCEEDED_AFTER_CLAMP 写入审计跟踪。
经验教训: 对于安全的自动化，仅进行形式化的模式检查是不够的；配额和限制必须成为规范的一部分。
最小反例允许对系统针对特定故障类别的韧性进行测试，而不会使数据变得嘈杂。
决斗的结果应自动成为 CI 流水线的新规则（next_guard）。
相关概念: 最小反例
操作边界
JSON Schema
对抗性验证
学习建议: 不要试图立即引入外部协调器（Coordinator）——从手动离线执行开始，以理解决斗机制。
在创建反例时，请始终问自己：「如果删除此字段会怎样？」。如果违规仍然存在，则该字段不是最小的，应将其删除。
专注于 validation.md 格式。在实际工作中，此文件是您用于自动阻止回归的「法律基础」（先例）。
区分概念：「有毒规范」（需求缺陷）、「变体」（缺陷类别）和「决斗反例」（破坏 Then 的具体输入）。
附加资源: Github spec kit：https://github.com/github/spec-kit — 用于学习规范优先（specification-first）方法。
维基百科：formal specification：https://en.wikipedia.org/wiki/Formal_specification — 形式化规范的理论基础。
离线示例 tribunal：book2/examples/tribunal/ — 脚本源代码和用于本地运行的 JSON 示例。
摘要: LLM 决斗（验证者对抗实现者）将形式化规范转变为事件管理的可靠防御机制。系统不再仅仅检查数据类型的正确性，而是转向检查操作边界（配额、后果限制）。最小反例允许隔离漏洞，所有更改和失败都记录在 validation.md 中，将每个错误转化为未来 CI 的回归测试（next_guard）。