create-formal-verification-skill

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

Claude Code では、このスキルに従う前に、セッションごとに一度 Claude Code アダプターを読んでください。pstack スキルで使われている Cursor の名前を Claude Code に対応づけています。

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

コードから対象を選ぶ

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

適切な対象とは、コードが保証していることであり、それが破られるとユーザーに害が及び、しかもそれを破るケースにテストがほとんど届かないものです。検証が最も簡単なものではなく、リポジトリ内で最も重要な対象を選んでください。

問いに合わせてツールを選ぶ

問いに答えられるツールのうち、最もコストの低いものを選んでください。モデルチェッカー、証明支援系、SMT ベースの検証ツール、またはその他のツールが候補です。イベントが不適切な順序で発生する可能性を調べる場合は、設計を小さくモデル化したモデルチェッカーが適していることが多く、言語を問わず TLA+ がその場合の標準的な選択肢です。メモリー安全性、オーバーフロー、データ構造の不変条件のように、コード自体がすべての入力に対して正しく動作するかを調べる場合は、コード上で実行する検証ツールが適していることが多いです。その言語で実行できる検証ツールがない場合は、その旨を伝え、関数の手作りモデルではなく、生成した入力で実際のコードをテストしてください。上限を設けず、あらゆるサイズで成立しなければならない性質には、証明が必要な場合があります。リポジトリの開発者がインストールして実行できるツールを優先し、それを選んだ理由をユーザーに伝えてください。

優れたスキルの条件

• コードに忠実であること。 モデルや証明の各要素が、レビュアーが確認できるコードを指している必要があります。検証で分割不能な1ステップとして扱うものは、コード上でも分割不能な1ステップである必要があります。名前にはこのリポジトリで使われているものを使用してください。
• 失敗を検出できること。 失敗を確認したことのないチェックでは何も証明できません。チェックが対象とするコードの壊れた派生版で、各性質が失敗することを示してください。たとえば、チェックを削除したり、ステップの順序を入れ替えたりします。
• 検出結果をそのまま報告すること。 現在のコードが性質を破っている場合は、コードで使われている用語で反例を示して報告してください。チェックが通るまで性質やモデルを弱めないでください。また、ユーザーに頼まれない限り、製品コードを変更しないでください。
• 検証範囲を正直に示すこと。 何をどのような上限と仮定のもとで検証したか、何が対象外かを明記してください。検証の成功が保証するのはモデルまたは上限までであり、システム全体ではありません。
• ツールなしでも読めること。 性質と、それが破られた場合の害を、それぞれ平易な一文で説明してください。反例は、コードで使われている言葉による短い手順の列として説明してください。
• 再実行のコストが低いこと。 1つのコマンドで実行でき、ツールのバージョンを再現でき、次のエージェントが関連する変更のたびに使えるほど実行時間が短いこと。
• コードの変更に追随すること。 各チェックが対象とするファイルと関数、および検証内容を最後に確認したコミットを記録してください。そのコミット以降に対象コードが変更された場合、次のエージェントが検証内容の再確認が必要だと分かるようにしてください。

verify スキルを作成する

対象領域を示し、どのような場合に使うかを記載したフロントマター付きの、プロジェクトローカルなスキルを作成してください。フロントマターがないと、スキルは登録されません。スキルだけを読んだ次のエージェントが、変更が検証対象のコードに影響するかどうかを判断し、チェックを実行し、実際のバグとモデル化の誤りを見分け、意図した変更に合わせて検証を更新できるようにしてください。カバレッジの記録と同期コミットをスキルに記載し、検証内容が新しいコミットのコードを正しく記述していることを確認した後にのみ、次のエージェントが同期コミットを進めるよう指示してください。このリポジトリで実際に使われているコマンド、パス、用語を使い、プレースホルダーは残さないでください。

チェックが TLA+ モデルの場合は、すべての結果を pstack の /statechart スキルで確認するよう、次のエージェントに伝えてください。このスキルは、チェッカーが検出した各不変条件違反について、最短の経路をわかりやすい言葉で示し、変更によってどの違反が修正されたかを明らかにします。チェックに合格した場合は、システムの状態遷移を図にします。/statechart という名前で参照してください。そのコマンド、オプション、ファイルパスはリリースやマシンによって変わるため、生成するスキルやそのスクリプトには一切記載しないでください。

引き継ぐ前に検証する

実際のコードで対象の性質に違反する一時的な変更を加え、次のエージェントと同じように、生成したスキルに一度従ってください。チェックで違反を検出できなければなりません。その後、一時的な変更を取り消し、チェックが元の状態に戻ったことを確認してください。つまり、合格するか、報告する所見だけが残る状態にします。一度も実行されていない verify スキルは草案です。スキルで違反を検出できない場合や、手順の一部が実行できない場合は、一時的な変更ではなく、スキルまたは検証を修正してください。

引き継ぎ

何を検証したか、どのツールを使い、その理由は何か、検証の範囲、チェックで何が見つかったか（わかりやすい言葉で）、実行方法、対象外の事項をユーザーに伝えてください。近い対象が見つかった場合に限り、次の検証対象を提案してください。変更後に再確認されていない検証を整合させるには、/maintain-formal-verification-skill を参照するようユーザーに案内してください。