formal: CSP 導入検討（並行/プロトコル検査） #1890
Description
背景
ae-framework では TLA+/TLC, Alloy, Apalache, SMT(z3/cvc5), Kani を中心に形式的手法のスモークテスト/CI 統合を進めている。
並行・通信・プロトコル（デッドロック/進行性/プロセス合成）に対しては、CSP 系の導入が有効候補。
目的
- CSP（プロセス代数）で並行/プロトコル仕様を記述し、機械的検査（少なくともデッドロック/発散/トレース整合）を ae-framework の形式検査パイプラインに統合する。
進捗
- Phase 0/CI導線（stub + 集約 + docs）は PR formal: add SPIN/CSP/Lean runners + CI integration #1894 で実装済み。
- ツール候補/採用案（ローカル実行の現実解）と
verify:cspの自動バックエンド選択は PR formal: CSP toolchain selection (refines/cspmchecker) #1896 で対応。
スコープ
- 仕様置き場:
spec/csp/ - ランナー:
scripts/formal/verify-csp.mjs（non-blocking で summary 出力） - CI:
.github/workflows/formal-verify.ymlにverify:cspジョブ追加（run-formalラベル/dispatch で実行） - 集約:
formal-aggregate.ymlでcsp-summary.jsonを取り込み、PR/Step Summary に反映
ツール選定（採用案）
- 推奨（実務標準/高機能）: FDR
refines（商用）--mode assertionsで assertion（例: deadlock free）を実行可能。- CI への常時導入はライセンス/配布形態の観点で要検討（Phase 1以降）。
- OSS（最低限の型検査）:
cspmchecker（libcspm）- CSPM のパーサ/型検査が主目的で、refinement/モデル検査は対象外。
- 代替（要調査）: HST, PAT 等（CI での安定導入や言語互換の観点で判断）。
導入方針
- Phase 0: “動く導線” を最小で作る（サンプル仕様 + 非ブロッキング実行 + summary 生成）。
- Phase 1: CI へ統合（キャッシュ/差分実行/成果物の標準化）。
- Phase 2: 実ドメイン（例: KvOnce など）に適用し、検査観点（デッドロック/ライブネス等）を増やす。
TODO（詳細）
- CSP ツール候補を調査し、採用案を決定（CI 利用可否、ライセンス、インストール手段、再現性）
-
spec/csp/README.mdを追加（記法、実行方法、期待成果物） -
spec/csp/sample.cspmに最小サンプルを追加 -
scripts/formal/verify-csp.mjsを追加- 期待入力:
.csp/.cspm（ツールに依存） - 出力:
artifacts/hermetic-reports/formal/csp-summary.json - ステータス: ran/tool_not_available/file_not_found/failed 等の正規化
- 期待入力:
-
scripts/formal/tools-check.mjsに CSP ツール検出を追加 -
.github/workflows/formal-verify.ymlにverify-cspジョブ追加-
verify-csp実行（non-blocking） - artifact upload（
formal-reports-csp）
-
-
formal-aggregate.ymlにcsp-summary.jsonの取り込みと表示を追加 - ドキュメント更新
-
docs/quality/formal-runbook.md -
docs/quality/formal-full-run.md -
docs/quality/formal-tools-setup.md
-
受け入れ基準
- CI（Formal Verify）で
verify:cspが実行され、csp-summary.jsonが artifact として取得できる。 -
formal-aggregateが CSP の結果を present/ran/ok（または status）として集約表示できる。