菜单
形式手法(Z3/全列挙/TLA+)で仕様と実装を検証し、反例・契約・確認質問の台帳を作る。仕様や実装の正しさを機械的に検証したいとき、docsとコードの食い違いを洗い出したいとき、設定の矛盾や並行処理・ライフサイクルの非決定性が絡むバグを疑うときに使う。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
| name | formal |
| description | 形式手法(Z3/全列挙/TLA+)で仕様と実装を検証し、反例・契約・確認質問の台帳を作る。仕様や実装の正しさを機械的に検証したいとき、docsとコードの食い違いを洗い出したいとき、設定の矛盾や並行処理・ライフサイクルの非決定性が絡むバグを疑うときに使う。 |
対象の仕様・実装を形式手法で検証し、反例（不変条件違反・時相性質違反）や仕様間の差分を機械的に洗い出す。最終成果物は「証明の山」ではなく、実装の主張・機械検査の結果・ドメインへの確認質問をまとめた台帳である。形式手法はバグを出すためだけでなく、仕様と認識を揃えるための共通言語として使う。
/formal <検証したい対象の説明やファイルパス> として起動する（本 skill は /formal としても直接呼び出せる）。
/formal wt.md と wtclean.md の worktree/branch/workspace/PR/未コミット/agent状態の遷移
/formal .config/claude/skills/wtclean/SKILL.md の安全条件
いきなりツールを持ち出さない。まず対象の性質を見極める:
| 対象の性質 | 手法 |
|---|---|
| 状態を持たない純粋述語・設定（条件の組合せ、ルール、契約） | Z3（SMT ソルバ。「この条件を満たす入力は存在するか?」に YES=実例付き / NO で答える。矛盾設定は UNSAT で検出） |
| 有限で決定的な状態遷移 | 素の全列挙（Python で直積を回す。外部ツール不要） |
| 非決定性・並行性・時相性質（順番・同時・クラッシュ・いつか必ず） | TLA+ / TLC（tlc コマンド） |
注記: 本リポジトリでは
nix/modules/dev-tools.nixのtlaplus18がtlcコマンドを直接提供する。Nix 外の環境では TLC はjava -jar tla2tools.jar等の JAR 経由起動になるため、その場合はtlcを適宜読み替える。
非決定性・並行性・時相性質が絡むかどうかは、対象に次のような問いを当てて判断する:
これらの問いに「Yes、考慮が要る」と答えるものが1つでもあれば TLA+ に倒す。
迷ったらまず全列挙で近似し、実際に手を動かして順序・タイミングが本質だと分かった時点で TLA+ に昇格する。最初から TLA+ に飛びつかない。
docs/*.md やスキル定義 md（例: .config/claude/skills/*/SKILL.md, .config/skills/*/SKILL.md）など、対象についての宣言的な仕様を読み、手順0で選んだ形式（Z3の述語定義、列挙スクリプトの状態/遷移定義、または TLA+ の VARIABLES/Next 等）に落とし込む。
コードを読み始める前に references/extraction.md の「宣言された仕様の在り処」「便利な問い」に目を通す — intent がどこに書かれているか、各述語・機構に何を機械的に問うべきかのチェックリストになる。
手順1とは独立に（docs を見ずに）、コード・スクリプトの実際の挙動だけを読み取って同じ形式に起こす。
references/extraction.md の「暗黙に決めている挙動」（default値・空/nilの扱い、エラー時の分岐、順序依存、信頼境界など）を手がかりに、ドキュメントに書かれていない挙動も拾う。
モデルの書き方（純粋関数への切り出し、不変条件の名前付け、反例志向、同値類と境界の列挙、契約と反例の区別）は references/modeling.md を参照。
同じ不変条件・時相性質を両モデル（ドキュメント仕様/コード実装仕様）にかけ、Z3・TLC・列挙スクリプトで反例探索する。
検査観点に迷ったら references/bug-catalog.md のバグパターンカタログ（純粋述語・設定系/並行・時間系/境界・信頼系）をチェックリストとして当てる。
反例トレースの状態名・アクション名を、抽象的な変数名のままにせず日本語のドメイン用語に訳し戻す。
ステップ表の形式で提示する:
| # | 何が起きたか | どの状態になったか | 破れた不変条件/性質 |
|---|---|---|---|
| 1 | ... | ... | ... |
反例（とステップ表）をユーザーに見せ、次のどれかの判定を仰ぐ:
修正はここでは行わない。ユーザーの判定が出た後、別タスクとして着手する。
herdr agent read や pane のログから得た実際の実行トレースを、モデルの遷移列として照合する。
最終成果物は証明の山ではなく台帳である。verification/<topic>/ に以下を置く:
*.tla / *.cfg（TLA+ を使った場合）*.smt2 / Z3 スクリプト（Z3 を使った場合）検査を書いて満足せず、効き続けているか確認する。詳細は references/hardening.md を参照。
対象が大きく作業者エージェントに委任する場合は、/wt のエージェント起動で --effort xhigh を使う（形式化・モデル検査は設計判断を要する難しいタスクのため）。
タスクの説明からブランチ名を自動生成し、herdr の worktree + workspace を立ち上げ、必要なら作業担当エージェントに委任する。ユーザーが新しい作業を始めたい・worktree を切りたい・「/wt」と言った時に使う。
学習ループ用の教師モード — セッションの内容や設計判断を、段階的な説明・チェックリスト・ クイズでユーザーが深く理解するまで伴走する理解ゲート。 ユーザーが「/learn」「理解ゲート通して」「これ教えて」「クイズ出して」などと言った時に使う。 また、リポジトリの CLAUDE.md が理解ゲートを規定している場合(例: hexhive)、 設計判断を含む PR のマージ前にこちらから発火を提案してよい。
エージェントセッションの意思決定・洞察・成果物を Obsidian の ResearchNotes に昇格させる(蒸留パイプライン層1)。 ユーザーが「セッションをまとめて」「記録して」「/session-log」と言ったときに使う。 また、設計判断・アーキテクチャ決定・重要な学びが生まれたセッションの区切り(タスク完了時・終了間際)には、こちらから記録を提案してよい。 生ログの全転写ではなく、対話で生まれた判断・設計・学びの厳選記録。
Question Behind the Question — 実装プランを出す前に、要望の下にある設計判断を1段掘り、 「本当に問うべき問い」の候補を提示する。 ユーザーが「/qbq」「問いから掘って」「本当に問うべきことは何?」などと言った時に使う。 また、インフラ・ワークフロー・アーキテクチャ系の相談で、要望の背後に未言語化の 設計判断がありそうな時は、実装プランを提示する直前に自発的にこの手順を提案してよい。
マージ済み PR に対応する worktree / workspace / ローカルブランチを安全に掃除する。/wt で作った worktree のライフサイクルの後始末。ユーザーが「worktree を掃除して」「片付けたい」「/wtclean」と言った時に使う。
herdr を介して、ユーザー・Claude Code・Copilot CLI・copilot-quorum の四者が pane 越しに対話するためのプロトコル。相手 pane の見つけ方、宛先プレフィックス付き メッセージ形式、送信・応答待ちの手順、ループ防止の原則を定める。 ユーザーが「Copilot と相談して」「quorum に合議させて」「他のエージェントに聞いて」 「隣の pane と話して」などと言った時、または他エージェントからの宛先付きメッセージ (【from→to】形式)を pane 上で検知した時に使う。 司令塔↔作業者プロトコル(herdr スキルの `agent send` / 上り報告)とは別物 — あちらは 上下関係の報告経路、こちらは対等な対話。既存プロトコルは変更しない。