monotykamary/gdp-wired 是一个 TypeScript 工具，处理那些即使状态发生变化也必须遵守的规则，例如预算上限或速率限制。据仓库说明，它能判定规则是否成立，并通过 GPU 搜索寻找反例，给出规则被破坏的执行路径。它于 2026 年 10 月 16 日创建，以 MIT 许可证公开。最新版本尚未发布。
该工具专注于自动证明状态规则的不变量（invariant），即在所有可能的状态变化下都应持续成立的条件。它不仅把预算和速率限制作为规则，也涵盖状态转换，并支持状态图和 XState 模型。它还可以从代码中提取规则，仓库中还包含多个领域的示例和对比文档。证明结果会用 Lean 再次检验。Lean 是一种定理证明器，用于机械地检查证明过程是否正确。说明中同时提出了负责判断的小型可信内核、不受信任的证明执行器（prover），以及 Lean 孪生（Lean twin）。
不过，已公开的资料没有给出证明规则所需的时间，也没有与其他工具的性能对比数据。该仓库目前有 15 个星标，最新版本同样未发布。因此，GPU 搜索与 Lean 复验相结合的架构是可以确认的，但仅凭现有资料难以判断它在实际工作中能处理多大范围的规则，以及处理得有多高效。