create-formal-verification-skill

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

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

コードから対象を選ぶ

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

良い対象とは、コードが約束していることのうち、破られるとユーザーに害が及び、しかもその原因となるケースをテストで確認できることがほとんどないものです。リポジトリで最も重要な対象を選び、検証しやすさだけで選ばないでください。

問いに応じてツールを選ぶ

モデルチェッカー、証明支援系、SMT を利用する検証ツール、その他のツールの中から、最小のコストで問いに答えられるものを選びます。イベントが望ましくない順序で発生するかを調べる場合は、設計を小さなモデルで表すモデルチェッカーが通常適しており、あらゆる言語でのデフォルトは TLA+ です。メモリ安全性、オーバーフロー、データ構造の不変条件のように、コード自体があらゆる入力に対して正しく動作するかを調べる場合は、通常、コード上で動作する検証ツールが適しています。この言語で動作する検証ツールがなければ、その旨を伝え、関数の手書きモデルではなく、生成した入力で実際のコードをテストしてください。上限では不十分で、すべてのサイズで成り立つ必要がある特性は、証明が必要になる場合があります。リポジトリの開発者がインストールして実行できるツールを優先し、それを選んだ理由もユーザーに伝えてください。

優れたスキルの条件

• コードに忠実であること。 モデルや証明のすべての部分が、レビュアーが開いて確認できるコードに対応していること。検証で不可分な1ステップとして扱う処理は、コード上でも不可分な1ステップであること。名前はこのリポジトリから選ぶこと。
• 失敗を検出できること。 一度も失敗を確認したことのないチェックでは、何も証明できません。チェック対象のコードからチェックを削除したり、ステップの順序を入れ替えたりした壊れたバリアントで、各特性が失敗することを示してください。
• 検出結果をそのまま報告すること。 現在のコードが特性に違反している場合は、コードで使われている用語で反例を報告してください。合格させるために特性やモデルを弱めてはならず、ユーザーから依頼されない限り、プロダクトコードも変更しないでください。
• 範囲を正直に伝えること。 何を、どの上限と仮定の下で検証したか、何を対象外としたかを伝えてください。合格が保証するのはモデルまたは上限の範囲であり、システム全体ではありません。
• ツールなしでも読めること。 特性と、それが破られた場合の被害を、それぞれ平易な1文で述べてください。反例は、コード上の用語で短いステップの列として説明してください。
• 再実行が手軽であること。 コマンドは1つにし、ツールのバージョンを再現可能にして、次のエージェントが関連する変更のたびに使える短い実行時間にしてください。
• コードと歩調を合わせること。 各チェックが対象とするファイルと関数、および検証内容を最後に確認したコミットを記録してください。そのコミット以降に対象コードが変更されている場合、次のエージェントが検証を再確認する必要があるとわかるようにしてください。

verify スキルを作成する

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

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

引き継ぐ前に検証する

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

引き継ぎ

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