時相論理の形式仕様の Quint を使って、denoland/celld の二重 writer バグを見つけた本記事は、AIに分散システムのバグを探させて、そのレポートを自分が理解できるように整形させたものです。 実際に見つかったバグは以下の Issues で、現在修正済みです。 これをどうやって見つけたのか、それを解説します。 ただし、形式仕様によるバグ検査は2026/08現在 Claude/ChatGPT のガードレールが発動しやすくなっています。自分は Anthropic Cyber Verifaction を取得しており、その環境で Claude 5 Opus を使った記録になります。 最近、形式仕様に興味があります。最近はその中で Quint という形式仕様の記述言語を試してみました。 これは分散システムの仕様をモデル化して、その中で守りたい仕様を破るパターンがないか検査することができます。 これをどう使うか、ちょうどいいところにdenoland/celld という、DurableObj
