時相論理の形式仕様の Quint を使って、denoland/celld の二重 writer バグを見つけた

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

[igrep]

"1. 守りたい制約を一行の invariant にする 2. 関係する状態遷移だけを小さく書く 3. checker に嫌な実行順序を探してもらう 4. 反例を本物のテストとして実装へ戻す"

[tinsep19]

時間が合わないとキツい処理はデバッグも大変

[mska]

論理型言語大好き人間なので大変興味あり

[mkusaka]

Quintでcelldのsingle-writer違反を探索し、TTL10s・clock skewで二重writer反例を特定してRustテストで再現

[yhara]

形式手法、Alloyとか触ったことはあるけど、実際の課題に適用したことはなくて、このへんAIに手伝ってもらって実用できるようになるとよさそう