Montanalabs/incident-bot

[](https://github.com/Montanalabs/eidos-lang) # 事件响应机器人 不受信任的输入是一个寻呼机警报；它只能成为封闭类型（closed type）上的一组固定决策中的一种，绝不能作为工具参数。被注入的指令无法在该封闭类型中表示，因此它会被拒绝——在编译时由 `check` 证明，并在运行时由 `extract` 域检查再次进行限制。 - **不受信任的输入：** `fetch` —— 一个寻呼机警报 - **封闭类型：** `type Decision = Mitigate(Runbook) | Page | Ack`，其中 `Runbook` 是封闭的 - **接收端 / 能力：** `grant mitigate irreversible` → `commit { mitigate(d) }` - **后果维度：** 信任，可逆性 ## 运行演示 ``` examples/apps/incident-bot/demo.sh ``` 安全代理证明 `SAFE`，在一个良性输入上运行，并且**在信任边界处拒绝注入 payload（退出状态 3）**。易受攻击的版本证明 `UNSAFE` —— 它永远无法编译成可运行的代理。 ## 文件 - `incident-bot_safe.eide` —— 正确的设计。 - `incident-bot_unsafe.eide` —— 诱人但错误的版本（模型必须学会拒绝的反面示例）。 - `eidos.toml` —— 项目清单（每个应用都是一个独立的 Eidos 项目）。 _{Eidos 示例语料库的一部分 —— 200 个独立的、防止注入的项目。使用 Eidos 构建，这是一种其类型系统从结构上杜绝了 prompt injection 的语言。将 ./demo.sh 与 Eidos 工具链一起放在您的 PATH 上运行。}

标签：Cutter