| name | formal |
| description | 形式手法(Z3/全列挙/TLA+)で仕様と実装を検証し、反例・契約・確認質問の台帳を作る。仕様や実装の正しさを機械的に検証したいとき、docsとコードの食い違いを洗い出したいとき、設定の矛盾や並行処理・ライフサイクルの非決定性が絡むバグを疑うときに使う。 |
形式手法による検証 (Z3 / 全列挙 / TLA+)
対象の仕様・実装を形式手法で検証し、反例（不変条件違反・時相性質違反）や仕様間の差分を機械的に洗い出す。最終成果物は「証明の山」ではなく、実装の主張・機械検査の結果・ドメインへの確認質問をまとめた台帳である。形式手法はバグを出すためだけでなく、仕様と認識を揃えるための共通言語として使う。
使い方
/formal <検証したい対象の説明やファイルパス> として起動する（本 skill は /formal としても直接呼び出せる）。
/formal wt.md と wtclean.md の worktree/branch/workspace/PR/未コミット/agent状態の遷移
/formal .config/claude/skills/wtclean/SKILL.md の安全条件
手順
0. トリアージ（このスキルの核）
いきなりツールを持ち出さない。まず対象の性質を見極める:
| 対象の性質 | 手法 |
|---|
| 状態を持たない純粋述語・設定（条件の組合せ、ルール、契約） | Z3（SMT ソルバ。「この条件を満たす入力は存在するか?」に YES=実例付き / NO で答える。矛盾設定は UNSAT で検出） |
| 有限で決定的な状態遷移 | 素の全列挙（Python で直積を回す。外部ツール不要） |
| 非決定性・並行性・時相性質（順番・同時・クラッシュ・いつか必ず） | TLA+ / TLC（tlc コマンド） |
注記: 本リポジトリでは nix/modules/dev-tools.nix の tlaplus18 が tlc コマンドを直接提供する。Nix 外の環境では TLC は java -jar tla2tools.jar 等の JAR 経由起動になるため、その場合は tlc を適宜読み替える。
非決定性・並行性・時相性質が絡むかどうかは、対象に次のような問いを当てて判断する:
- どの順番で起きても大丈夫か?
- 同時に来たらどうなるか?
- クラッシュ後はどうなるか?
- いつか必ず〜するか?（liveness）
これらの問いに「Yes、考慮が要る」と答えるものが1つでもあれば TLA+ に倒す。
迷ったらまず全列挙で近似し、実際に手を動かして順序・タイミングが本質だと分かった時点で TLA+ に昇格する。最初から TLA+ に飛びつかない。
1. ドキュメント宣言仕様の形式化
docs/*.md やスキル定義 md（例: .config/claude/skills/*/SKILL.md, .config/skills/*/SKILL.md）など、対象についての宣言的な仕様を読み、手順0で選んだ形式（Z3の述語定義、列挙スクリプトの状態/遷移定義、または TLA+ の VARIABLES/Next 等）に落とし込む。
コードを読み始める前に references/extraction.md の「宣言された仕様の在り処」「便利な問い」に目を通す — intent がどこに書かれているか、各述語・機構に何を機械的に問うべきかのチェックリストになる。
- 各制約には出典（ファイルパスと該当の文）を必ず記録する
- 書いていないことを憶測で補わない。ドキュメントに明記されていない挙動は「不明」として扱う
2. コード実装仕様の形式化
手順1とは独立に（docs を見ずに）、コード・スクリプトの実際の挙動だけを読み取って同じ形式に起こす。
references/extraction.md の「暗黙に決めている挙動」（default値・空/nilの扱い、エラー時の分岐、順序依存、信頼境界など）を手がかりに、ドキュメントに書かれていない挙動も拾う。
- 対象のコード・シェルスクリプト・herdr コマンド呼び出し等を実際に読み、そこに書かれている通りの遷移だけをモデル化する
- ドキュメントの記述で答え合わせをしない（先入観でモデルが歪むのを防ぐため）
モデルの書き方（純粋関数への切り出し、不変条件の名前付け、反例志向、同値類と境界の列挙、契約と反例の区別）は references/modeling.md を参照。
3. モデル検査で反例を挙げる
同じ不変条件・時相性質を両モデル（ドキュメント仕様/コード実装仕様）にかけ、Z3・TLC・列挙スクリプトで反例探索する。
検査観点に迷ったら references/bug-catalog.md のバグパターンカタログ（純粋述語・設定系/並行・時間系/境界・信頼系）をチェックリストとして当てる。
- 不変条件違反・時相性質違反があれば反例トレースを得る
- 加えて仕様間差分も検出する: docs では許されるが code では起きない遷移、その逆（code では起きるが docs には書かれていない遷移）
4. 反例のドメイン翻訳
反例トレースの状態名・アクション名を、抽象的な変数名のままにせず日本語のドメイン用語に訳し戻す。
ステップ表の形式で提示する:
| # | 何が起きたか | どの状態になったか | 破れた不変条件/性質 |
|---|
| 1 | ... | ... | ... |
5. ドメインエキスパートへの提示
反例（とステップ表）をユーザーに見せ、次のどれかの判定を仰ぐ:
- 仕様バグ（モデル化した不変条件・性質そのものが間違っている）
- 実装バグ（コードが仕様を満たしていない）
- ドキュメントバグ（ドキュメントの記述が実装と食い違っている）
修正はここでは行わない。ユーザーの判定が出た後、別タスクとして着手する。
トレース検証（herdr 連携）
herdr agent read や pane のログから得た実際の実行トレースを、モデルの遷移列として照合する。
- 実トレースの各ステップが、モデル上のいずれかの遷移に対応するか確認する
- モデルに存在しない挙動（どちらのモデルの遷移でも説明できない状態変化）を検出したら、モデルと現実の乖離として手順5に回す
- trace-checking の詳しい位置づけ（抽象モデルと実挙動を繋ぐ最も強い一手である理由）は references/hardening.md を参照
成果物: 台帳
最終成果物は証明の山ではなく台帳である。verification/<topic>/ に以下を置く:
*.tla / *.cfg（TLA+ を使った場合）*.smt2 / Z3 スクリプト（Z3 を使った場合）- 列挙スクリプト（全列挙で済ませた場合）
- レポート md — 次の3部構成にする:
- 実装の主張（モデル化した仕様・不変条件、出典付き）
- 機械検査の結果 — 2種類を区別して管理する
- 反例 → バグ or 仕様の食い違い → Issue / 確認質問へ
- 契約（成立を証明できた性質）→ 回帰ガードとしてロック。将来どちらかが変わったら赤くなる
- ドメインへの確認質問（手順5でユーザーに投げるもの）
検証を効いている状態に保つ
検査を書いて満足せず、効き続けているか確認する。詳細は references/hardening.md を参照。
- self-check 化: 期待判定（VIOLATE / OK）との assert を持たせ、CI で回る回帰ガードにする
- broken-variant テスト: わざと壊した実装で検査が赤になることを確認する（検査が load-bearing である証明）
- 依存の宣言的固定: ソルバー・モデル検査器を nix 等で1ファイルに宣言し、誰でも同じ結果を再現できるようにする
- 人間可読出力 + 機械可読 exit code: デモ用と CI 用を両立させる
/wt 経由での委任
対象が大きく作業者エージェントに委任する場合は、/wt のエージェント起動で --effort xhigh を使う（形式化・モデル検査は設計判断を要する難しいタスクのため）。
references/
- bug-catalog.md — 形式手法が炙り出すバグパターンのカタログ（純粋述語・設定系/並行・時間系/境界・信頼系）
- extraction.md — コードからモデルを作るときに見る視点（宣言された仕様の在り処、暗黙の挙動、便利な問い）
- modeling.md — 何を仕様として書き出すか（純粋関数、不変条件、反例志向、同値類と境界、契約と反例の区別）
- hardening.md — 検証を効いている状態に保つ工夫と model↔code のギャップの詰め方（trace-checking を含む）
