メニュー
Code analysis for formal verification. Use when: (1) investigating a system implementation to identify what to model in TLA+, (2) performing bug archaeology on a codebase, (3) producing a modeling brief that guides spec generation.
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
SOC 職業分類に基づく
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
直接コマンドでは確認用 Prompt が省略されます。実行前にソースを確認してください。
npx skills add https://github.com/specula-org/Specula --skill code-analysisコマンドは1行のまま表示されます。コピー前に横へスクロールして全体を確認してください。
ローカルで確認しますか？SkillsMP が現在取得できるファイルをダウンロードできます。
SKILL.md を表示中
TLA+ spec generation from a modeling brief. Use when: (1) turning code analysis findings into a TLA+ specification, (2) generating model checking and trace validation specs, (3) producing instrumentation mappings for trace collection.
Writing target-specific modeling guidance for Specula. Use when: (1) the user is setting up Specula on a new target system, (2) the user asks to write or revise a guidance file, (3) the user wants to add scenario hypotheses, scope guidance, or production-incident context to a target's pipeline runs.
Final reporting for Phase 4a results. Classify severity in bug-severity.md, then write a concise human-readable findings fragment for summary.md.
| name | code-analysis |
| description | Code analysis for formal verification. Use when: (1) investigating a system implementation to identify what to model in TLA+, (2) performing bug archaeology on a codebase, (3) producing a modeling brief that guides spec generation. |
Read guide.md for the full workflow methodology.