形式検証の検査を作る

テストは、誰かが思いついた場面を確かめる。この検査は、範囲を決めて、その範囲の順序を全部たどる。目的は「証明した」と言うことでなく、実物で起きる不具合を見つけ、見つからなかった範囲を正直に示すこと。

1. 対象を選ぶ

壊れると被害が大きく、テストが届きにくい約束を、コードと履歴から選ぶ。検証しやすい所を選ばない。git log で同じ処理の修正が続いた所、コメントに「〜の間に受けた」「途中で止まると」とある所が候補。

2. 約束を文にする

約束を 1 文ずつ、コードの言葉で書く。それぞれ、破れたときの被害も 1 文で書く。定義をなぞるだけの性質（can_x の結果が can_x と同じ）は書かない。次を含める。

• 順序をまたぐ性質: 「どの段で死んでも、再開すると〜」「A の後に B が起きても〜」。
• 1 回の実行の外: 記録・ロック・ファイルは実行の後に残る。再開・再試行・同時の起動・前の記録へ戻ることを、3 回程度の連鎖で書く。1 回の実行だけを写すと、ここの不具合が見つからない。
• いつかは終わる: どの状態からも止まれる、待ち続けない。

3. モデルを書く

既定は、対象の言語の標準機能で書く明示状態の全探索（幅優先で、状態を集合に入れてたどる）。追加の依存が要らず、次の担当が読めて、そのまま試験に置ける。状態数が回らない、活性を厳密に調べたいなど、理由があるときだけ TLA+ などの道具を使う。全入力の保証が要るなら Dafny・Verus・Lean などの検証器を選ぶ。選んだ理由を書く。

• モデルの各動作に、対応するコードの場所を書く。コードで 1 段でない処理を、モデルで 1 段にしない。
• 時刻・シグナル・途中の死は、どの段にも起こせるようにする。
• 省いたものを一覧にする。 外部のプロセス・CLI・OS の振る舞いは、省くとその性質の合格が無効になる。子プロセスが受けたシグナルを伝え直す、包むプロセスが先に終わる、など。省いた振る舞いに触れる性質の合格には、「確かめていない」と添える。

4. 実物と突き合わせる

モデルと実コードを、同じ場面で動かして比べる（必須）。偽の子プロセスや一時ディレクトリで、モデルの主な分岐を実コードに通し、結果の違いが 0 になるまで、どちらが誤りかを調べて直す。突き合わせていないモデルの合格は、コードについて何も言えない。

5. 落ちるのを見る

合格した性質ごとに、コードの判定を 1 か所外した版をモデルに作り、その性質が落ちることを示す。一度も落ちていない性質は合格と書かない。

6. 反例を不具合にする

反例は疑いで、まだ不具合ではない。コードの言葉の短い手順に直し、実物で再現する（偽の子で起きるなら、それも書く。本物の CLI の振る舞いに拠るなら本物でも確かめる）。性質やモデルを弱めて反例を消さない。モデルの誤りなら、どこが実物と違ったかを書いて直す。コードを直すかは依頼に従う。

7. 同じ範囲をレビューと分ける

この検査はレビューの代わりにならない。入力の形・文字コード・環境の例外は、モデルの外に残る（揺れの一覧で確かめるなら create-property-test-skill）。届ける前の審査は interrogate で別に通す。

8. 残す

対象のリポジトリに、次を残す。

• 検査は 1 コマンドで回る形で、既存の試験に置く（1 分以内を目安にする）。超えるなら、普段の範囲と広い範囲に分ける。
• 冒頭に、約束、範囲（上限）、省いたもの、対象の関数の一覧、確認した commit を書く。対象のコードを変えた担当は、モデルを見直してから commit を進める。ハッシュで機械的に検出する仕組みは、見直しの漏れが実際に起きるまで足さない。
• 対象に繰り返し使う手順が要るなら、create-verification-skill の形で verify-<対象> に書く。

返す形

何を確かめたか、道具とその理由、範囲と上限、省いたもの、見つけた不具合（手順と再現の結果）、落ちるのを見た壊し方、突き合わせの結果、再実行の 1 コマンド。「検証済み」と 1 語で書かない。