formal

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部構成にする:
  1. 実装の主張（モデル化した仕様・不変条件、出典付き）
  2. 機械検査の結果 — 2種類を区別して管理する
     • 反例 → バグ or 仕様の食い違い → Issue / 確認質問へ
     • 契約（成立を証明できた性質）→ 回帰ガードとしてロック。将来どちらかが変わったら赤くなる
  3. ドメインへの確認質問（手順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 を含む）