create-formal-verification-skill

形式検証スキルを作成する

Codex では、このスキルに従う前に、スキルごとの注記を含めてプラットフォームマッピングを読んでください。

GitHub Copilot では、このスキルに従う前に、スキルごとの注記を含めてプラットフォームマッピングを読んでください。

Muse では、このスキルに従う前に、スキルごとの注記を含めてプラットフォームマッピングを読んでください。

テストで確認できるのは、誰かがテストケースとして書くことを思いついたケースです。形式検証では、定められた範囲内のすべてのケース、つまりモデルにおけるすべてのステップの順序、上限までのすべての入力、あるいはすべての入力を確認します。このスキルでは、リポジトリで特に重要な箇所を見つけ、その箇所の性質を1つ検証し、次のエージェントがその性質に照らして変更を確認できるよう、プロジェクト内のスキルを残します。そのスキルは、初めて読み、変更作業の途中で参照し、あなたの作業を一切知らないエージェント向けに書いてください。ユーザーが検証言語を学ばなくても、結果を信頼し、それに基づいて行動できる必要があります。

コードから対象を選ぶ

コードベースを根拠に判断し、観察できないことだけをユーザーに尋ねてください。ユーザーが対象領域やバグを指定している場合は、そこから始めてください。

適切な対象は、コードが保証している性質のうち、それが破られるとユーザーに被害が及び、テストでは破綻するケースに届きにくいものです。検証しやすいものではなく、リポジトリ内で最も重要な性質を選んでください。

問いに合ったツールを選ぶ

問いに答えられるツールのうち、最もコストの低いものを選んでください。モデル検査器、定理証明支援系、SMT を利用する検証器、または別のツールが候補です。イベントが望ましくない順序で発生する可能性を調べるなら、設計の小さなモデルを対象とするモデル検査器が適していることが多く、どの言語でも TLA+ を標準の選択肢とします。メモリ安全性、オーバーフロー、データ構造の不変条件のように、あらゆる入力に対するコード自体の振る舞いを調べるなら、通常はコード上で動作する検証器が適しています。この言語で動作する検証器がない場合は、そのことを明記し、関数の手作りモデルではなく、生成した入力で実際のコードをテストしてください。上限では不十分で、あらゆるサイズで成り立つ必要がある性質には、証明が必要になることがあります。リポジトリの開発者がインストールして実行できるツールを優先し、選んだ理由をユーザーに説明してください。

優れた検証の条件

• コードに忠実であること。 モデルや証明のすべての部分が、レビュー担当者が確認できるコードに対応している必要があります。検証で不可分な1ステップとして扱う処理は、コードでも不可分な1ステップでなければなりません。名前にはこのリポジトリのものを使ってください。
• 失敗を検出できること。 失敗するのを一度も見たことがないチェックでは、何も証明できません。削除したチェックや順序を入れ替えたステップなど、チェック対象のコードを意図的に壊した版で、各性質の検証が失敗することを示してください。
• 検出した問題をそのまま報告すること。 現在のコードが性質に違反している場合は、コード上の用語で反例を添えて報告してください。合格させるために性質やモデルを弱めてはいけません。また、ユーザーが求めない限り、製品コードを変更してはいけません。
• 検証範囲を正直に伝えること。 何を、どの上限と前提のもとで検証したのか、何が対象外なのかを明記してください。合格が保証するのはモデルまたは上限までの範囲であり、システム全体ではありません。
• ツールがなくても読めること。 性質と、それが破られた場合の被害を、それぞれ平易な一文で述べてください。反例は、コードで使われている言葉で短いステップ列として説明してください。
• 再実行のコストが低いこと。 コマンド1つで実行でき、ツールのバージョンを再現でき、次のエージェントが関連する変更のたびに使う程度の短時間で終わるようにしてください。
• コードと歩調を合わせること。 各チェックが対象とするファイルや関数と、その検証内容を最後に確認したコミットを記録してください。対象コードがそのコミット以降に変更された場合、次のエージェントは検証内容を再確認する必要があると気づけます。

形式検証スキルを作成する

対象領域を明記し、いつ使うべきかを説明するフロントマター付きの、プロジェクト内スキルを作成します。スキル名には対象領域の名前を使い、verify や verify- で始まる名前は使わないでください。これらはドライバースキル /create-verification-skill が作成するものです。Claude Code では、.claude/skills/<area>/SKILL.md に配置します。フロントマターがないと、スキルは登録されません。次のエージェントがスキルだけを読めば、変更が検証対象のコードに触れているかどうかを判断し、チェックを実行し、本当のバグとモデリングの誤りを見分け、意図された変更に合わせて検証を更新できるようにしてください。カバレッジの記録と同期用コミットをスキルに記載し、検証が新しいコミット時点のコードを記述していると確認できた場合に限り、次のエージェントが同期用コミットを先に進めるよう指示してください。このリポジトリで実際に使われているコマンド、パス、名称を使い、プレースホルダーを残さないでください。

チェックが TLA+ モデルの場合は、次のエージェントに、すべての結果を pstack の /statechart スキルを使って読むよう指示してください。このスキルは、チェッカーが見つけた各不変条件違反を、最短経路として平易な言葉で示します。チェックに合格した場合、/statechart はシステムが状態間をどのように移動するかを図示します。/statechart は名前で参照してください。そのコマンド、オプション、ファイルパスはリリースやマシンによって異なるため、生成するスキルやスクリプトには一切コピーしないでください。

引き渡す前に検証する

生成したスキルを、次のエージェントが行うのと同じように、実際のコードで対象の性質を壊すスクラッチ変更を加えて、一度実行してください。問題を検出できなければなりません。その後、スクラッチ変更を取り除き、チェックが開始時と同じ状態に戻ったことを確認してください。つまり、合格しているか、報告する所見だけが残って不合格になっている状態です。一度も実行されていない形式検証スキルは、まだドラフトです。スキルが問題を見逃したり、手順が実行できなかったりした場合は、スクラッチ変更ではなく、スキルまたは検証を修正してください。

引き渡し

何を検証したか、どのツールをなぜ使ったか、検証の境界、チェックで見つかったことの平易な説明、実行方法、対象外の内容をユーザーに伝えてください。関連性の高い別の対象が見つかった場合に限り、2つ目の対象を提案してください。変更後に再確認されていない検証を最新の状態に戻す方法については、/maintain-formal-verification-skill を案内してください。