monotykamary/gdp-wired は、予算上限や速度制限のように状態が変化しても守られなければならない規則を扱う TypeScript ツールである。リポジトリの説明によれば、規則が成立するかどうかを判定し、GPU 探索によって反例を探して規則が破れる実行経路を示す。2026 年 10 月 16 日に作成され、MIT ライセンスで公開されている。最新のリリースは登録されていない。
このツールは、状態規則の不変条件（invariant）、すなわち可能な状態変化があっても引き続き成立しなければならない条件を自動的に証明することに焦点を置いている。予算や速度制限だけでなく状態遷移も規則として扱い、状態図と XState モデルに対応する。また、コードから規則を抽出する機能を備えており、リポジトリには複数の分野の例と比較文書が含まれている。証明結果は Lean で再確認する。Lean は証明過程が正しいかどうかを機械的に検査する定理証明器である。説明では、判断を担う小さな信頼カーネル、信頼されない証明実行系（prover）、そして Lean ツイン（Lean twin）が併せて示されている。
ただし公開されている資料には、規則の証明にかかる時間や他のツールとの性能比較の数値は示されていない。リポジトリはスター 15 件を記録しており、最新のリリースも登録されていない。そのため、GPU 探索と Lean による再検証を組み合わせた構造は確認できるものの、実際の作業でどの範囲の規則をどれだけ効率的に扱えるかは、現在の資料だけでは判断しにくい。