formal-verify

formal-verify

「コンパイルが通ること」よりも、アーキテクチャ上の意図が重要な場合にこのスキルを使用します。

このスキルでは、3 層の検証ループを実行します。

1. レイヤー 1：抽出した AST の事実と宣言的なルールに基づく構造検証
2. レイヤー 2：Z3Py プロトコル仕様および TLA+/Apalache 状態機械仕様に基づく振る舞い検証
3. レイヤー 3：複雑さ、一貫性、技術的完成度のヒューリスティックに基づく洗練度監査

各レイヤーは意図的に段階化されています。

• すべての編集：レイヤー 1 のみ。継続的なフィードバックを得られるほど高速です
• スライスのチェックポイント：レイヤー 1 と 2
• コミット前および手動の /verify：3 つすべてのレイヤー

クイックスタート

次のコマンドで対象プロジェクトをブートストラップします。

/verify --bootstrap

ブートストラップでは、次の 4 つのフェーズが実行されます。

1. 依存関係をインストールし、.verifier/ を作成する
2. ドキュメントとコードの構造からアーキテクチャ上のルールを検出する
3. 曖昧な点について、平易な英語でユーザーに質問する
4. 現在のコードベースに対して初期ルールを検証する

コマンド

• /verify すべてのレイヤーを詳細モードで実行し、統合レポートを出力します。
• /verify --bootstrap 依存関係をインストールし、.verifier/ を作成して、最初のルールセットを構成します。
• /verify --evolve アーキテクチャのドキュメントと既存の検証仕様の間にある乖離を確認します。
• /verify --grade レイヤー 3 のみを実行し、現在の洗練度を報告します。

検証の実行方法

レイヤー 1：構造

ランナーは Rust と Swift のソースファイルから事実を抽出し、次のような structural.yaml のルールをチェックします。

• 境界 Y を越えられるのはモジュール X のみ
• パターン Z に一致するモジュールは、インターフェイス W を実装する必要がある
• すべてのモジュールで、レガシー識別子を参照してはならない

構造チェックは最速であるため、デフォルトの PostToolUse フックです。

レイヤー 2：振る舞い

振る舞い検証では、状態遷移とプロトコルの契約を対象とします。

• 時相的性質、活性、インターリーブには TLA+/Apalache
• 契約、不変条件、境界をまたぐデータの保証には Z3Py 仕様ファイル

このレイヤーは、スライスのチェックポイントや、リスクの高いマージの前、または調整ロジックや言語間の契約に変更が加わるときに使用します。

レイヤー 3：洗練度

洗練度監査では、次の観点からコードを評価します。

• 複雑さ
• 一貫性
• 技術的完成度

評価と行単位の減点理由を出力するため、技術的に正しくするだけでなく、エージェントがコードを整理できます。

違反への対応

違反が見つかった場合は、対象に応じて出力を調整します。

• エージェント向けの出力：反例、診断、具体的な修正案
• 人間向けの出力：反例と診断のみ

同じ違反を 3 回試みてもエージェントが解決できない場合は、修正ループを停止し、次の情報とともにエスカレーションします。

• 元のルール
• 反例
• 試みた 3 回の修正
• 正しい修正を妨げていると思われる要因

対象リポジトリに作成されるプロジェクト構造

ブートストラップでは、次の構造が作成され、維持されます。

.verifier/
├── structural.yaml
├── elegance.yaml
├── specs/
├── facts/
└── reports/

• structural.yaml には、宣言的なレイヤー 1 のルールが保存されます
• elegance.yaml には、しきい値と評価方針が保存されます
• specs/ には、Z3Py および TLA+ の振る舞い仕様が保存されます
• facts/ には、抽出した AST の事実がキャッシュされます
• reports/ には、直近の検証結果が保存されます

対象プロジェクトでは、facts/ と reports/ を gitignore に追加してください。

運用ガイダンス

• 移行が完了したと報告する前に、/verify を実行してください。
• コードは正しいものの、まだ粗さが残っている場合は、/verify --grade を実行してください。
• アーキテクチャを意図的に進化させる場合、ルールや仕様を緩めるよりも更新することを優先してください。
• SKILL.md はオーケストレーションに集中させ、詳細な仕組みは以下のリファレンスから参照してください。

参考資料

• @references/layer1-structural.md 事実の抽出、Z3 エンコーディング、到達可能性、増分無効化について説明します。
• @references/layer2-behavioral.md TLA+/Apalache と Z3Py の使い分け、および仕様実行の契約について説明します。
• @references/layer3-elegance.md 指標ファミリー、評価、しきい値、Layer 3 のサブモジュール構成について説明します。
• @references/constraint-yaml-spec.md 構造ルールのスキーマ、セレクター、アサーション、事実パターン演算子について説明します。
• @references/bootstrap-process.md インストール、検出、ヒアリング、検証のブートストラップワークフローについて説明します。
• @references/agent-feedback-loop.md フックの統合、違反の注入、再試行、エスカレーションポリシーについて説明します。
• @references/spec-authoring-guide.md 平易な英語で記述されたアーキテクチャ上の意図を形式仕様に変換する方法について説明します。