formal: CSP toolchain selection (refines/cspmchecker) #1896
Conversation
❓ Code Generation Drift DetectionStatus: Automated by AE-Framework Codegen |
Quality Summary
|
Progress Summary
|
Generate Artifacts PreviewGenerated at: 2026-02-03T19:41:04.860Z
|
|
@artifacts/quality/comment-body.txt |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 467bc298f5
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
KvOnce Trace Validation
|
There was a problem hiding this comment.
Pull request overview
This pull request extends the CSP (Communicating Sequential Processes) verification infrastructure by adding automatic toolchain detection and support for FDR's refines command and the OSS cspmchecker tool. The changes move the CSP integration from "stub only" to "works when tools are available locally."
Changes:
- Extended
verify-csp.mjsto auto-detect and userefines(FDR) andcspmcheckertools with a fallback priority order - Updated the CSP sample to be a genuinely deadlock-free minimal example with FDR assertion
- Enhanced documentation with toolchain options, usage examples, and security warnings
Reviewed changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
spec/csp/sample.cspm |
Updated to deadlock-free example with synchronized parallel composition and FDR assertion |
spec/csp/README.md |
Added toolchain documentation in English and Japanese with usage examples |
scripts/formal/verify-csp.mjs |
Added auto-detection for refines/cspmchecker and --mode flag for assertions |
scripts/formal/tools-check.mjs |
Added detection and version reporting for refines and cspmchecker |
docs/quality/formal-tools-setup.md |
Updated CSP section with supported backends and priority order |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
❓ Code Generation Drift DetectionStatus: Automated by AE-Framework Codegen |
|
レビュー指摘への対応です。
Copilot Review Gate 対応として、該当スレッドは解決して再実行します。 |
|
@artifacts/quality/comment-body.txt |
CI Status Snapshot (2026-02-03T19:44:45.165Z)
|
変更内容
scripts/formal/verify-csp.mjs）を拡張CSP_RUN_CMD（shell）に加え、利用可能なら自動で以下を使用refines（--mode typecheck|assertions）cspmchecker（typecheck）spec/csp/sample.cspm）を「デッドロックしない最小例」に更新し、FDR の deadlock free assertion を同梱spec/csp/README.md: バックエンド優先順、FDR assertion 実行例、セキュリティ注意docs/quality/formal-tools-setup.md: CSP バックエンド候補を明記tools:formal:checkの CSP 表示を改善（refines/cspmcheckerの検出）目的
ISSUE#1890 の「ツール候補の整理と採用案（ローカル実行の現実解）」を確定し、
verify:cspを “設定があれば動く” から “ツールがあれば即動く” へ前進させます。使い方（ローカル）
pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheckrefinesがある場合）:pnpm run verify:csp -- --file spec/csp/sample.cspm --mode assertions関連ISSUE