monotykamary/gdp-wired는 예산 상한이나 속도 제한처럼 상태가 바뀌어도 지켜져야 하는 규칙을 다루는 TypeScript 도구다. 저장소 설명에 따르면 규칙이 성립하는지 판정하고, GPU 검색으로 반례를 찾아 규칙이 깨지는 실행 경로를 제시한다. 2026년 10월 16일 생성됐으며 MIT 라이선스로 공개됐다. 최신 릴리스는 등록돼 있지 않다.
이 도구는 상태 규칙의 불변식(invariant), 즉 가능한 상태 변화에도 계속 성립해야 하는 조건을 자동으로 증명하는 데 초점을 둔다. 예산이나 속도 제한뿐 아니라 상태 전이도 규칙으로 다루며, 상태도와 XState 모형을 지원한다. 코드에서 규칙을 추출하는 기능도 있고, 저장소에는 여러 분야의 예제와 비교 문서가 포함돼 있다. 증명 결과는 Lean으로 다시 확인한다. Lean은 증명 과정이 올바른지 기계적으로 검사하는 정리 증명기다. 설명에는 판단을 맡는 작은 신뢰 커널, 신뢰하지 않는 증명 수행기(prover), 그리고 Lean 쌍둥이(Lean twin)가 함께 제시돼 있다.
다만 공개된 자료에는 규칙을 증명하는 데 걸리는 시간이나 다른 도구와의 성능 비교 수치가 제시돼 있지 않다. 저장소는 별 15개를 기록하고 있으며, 최신 릴리스도 등록돼 있지 않다. 따라서 GPU 검색과 Lean 재검증을 결합한 구조는 확인할 수 있지만, 실제 작업에서 어느 범위의 규칙을 얼마나 효율적으로 다룰 수 있는지는 현재 자료만으로 판단하기 어렵다.