kotaroyamame
13 verified skills13 total stars
extract-spec
Extract a provisional VDM-SL specification from existing source code. This is NOT the true spec — it is a scaffold for dialogue to uncover the user's real intent. Triggered by: "extract spec from code", "reverse engineer the specification", "extract-spec", "code to spec", "formalize the existing code". Japanese: 「既存のコードから仕様を抽出して」「コードの仕様を形式化して」 「コードベースを分析して」「コードをリバースエンジニアリングして」
development1
formal-methods-guide
Provide reference knowledge on VDM-SL and formal methods. Triggered by "VDM-SL syntax", "how to write types", "what is a pre-condition", "what is an invariant", "meaning of proof obligations", "what are formal methods", or "formal specification". Also responds to Japanese: 「VDM-SLの文法」「事前条件とは」「形式手法とは」等。 Referenced as background knowledge by other skills (define-contract, verify-spec).
testing1
generate-tests
VDM-SL仕様と設計文書（PROTOCOL.md）から自動的にテストを生成するスキル
testing1
skills/integrated-workflow
# Integrated Workflow — End-to-End Formal Agent Development ## Overview This skill orchestrates the full formal development pipeline for multi-agent systems: **Define → Verify → Prove → Generate → Test** in a single guided session. Each phase invokes an existing skill, with automated handoff, error recovery, and a final session report summarizing all results. 各フェーズは既存のスキルを呼び出し、フェーズ間の自動ハンドオフ、エラー回復、 最終セッションレポートの生成を行います。 ## Trigger Conditions Activate this skill when the user says any of: - 「
development1
refine-spec
Refine a provisional VDM-SL specification through dialogue with the user, uncovering the true specification that exists in the user's mind. The provisional spec (from extract-spec) serves as a scaffold for questions. Triggered by: "refine the spec", "review the provisional spec", 「仕様を磨きたい」「仮仕様をレビューして」「コードの意図を確認したい」「仕様を確認して」
testing1
define-contract
形式的エージェント契約を定義し、VDM-SL仕様と設計文書（プロトコル仕様）を生成するスキル
tools1
export-human-spec
Generate a human-readable natural language specification document (Markdown) from a VDM-SL formal specification. Translates types, invariants, pre/post-conditions, and operations into clear prose that domain experts, project managers, and non-technical stakeholders can understand and review — without needing to learn VDM-SL. Use this skill whenever the user wants to: generate documentation from a VDM-SL spec, create a readable specification, export a spec for human review, convert VDM-SL to natural language, create a requirements document from formal specs, or produce a specification that non-engineers can read. Japanese triggers: 「VDM仕様から自然言語仕様を作りたい」「人間が読める仕様書を生成して」 「VDM-SLをドキュメントにして」「仕様書をエクスポートして」「形式仕様を読みやすくして」 「非エンジニア向けの仕様書を作って」「仕様のドキュメントを生成して」
testing1
generate-code
Generate TypeScript/Python code scaffolds from VDM-SL specifications. Triggered by "generate code from the spec", "convert to TypeScript", "generate Python code", "create a scaffold", "generate implementation template", "create type definitions from VDM", or "generate agent code". Also responds to Japanese: 「仕様からコードを生成して」「TypeScriptに変換して」等。 Generates runtime verification code for pre-conditions, post-conditions, and invariants.
development1
import-natural-spec
Import a natural language specification document (Markdown) and interactively convert it to a VDM-SL formal specification. Reads the MD file, identifies requirements, flags ambiguities, and guides the user through a dialogue to fill gaps — producing a complete .vdmsl file. Use this skill whenever the user wants to: convert a requirements document to VDM-SL, import a spec from Markdown, formalize a natural language specification, turn a requirements doc into a formal spec, or create VDM-SL from an existing document. Japanese triggers: 「自然言語仕様をインポートしたい」「要件定義からVDMを作りたい」 「MDファイルからVDM仕様を生成して」「要件書を形式仕様に変換して」 「仕様書をVDM-SLにしたい」「ドキュメントからエージェント契約を作りたい」
testing1
reconcile-code
Reconcile existing code with the confirmed VDM-SL specification. Compare spec vs code item-by-item, generate a diff report, produce code fixes prioritized by Finding category, and auto-generate tests. Triggered by: "reconcile code with spec", "fix code to match spec", 「仕様とコードを照合して」「コードを仕様に合わせて」「差分を出して」「コードを直して」
development1
reverse-workflow
Orchestrate the full reverse engineering pipeline: Extract provisional spec from existing code, refine through dialogue to uncover the true spec, then reconcile code with the confirmed spec. Optionally connects to the forward pipeline (verify → prove → generate → test). Triggered by: "reverse workflow", "extract and refine spec from code", "formalize existing code", "reverse engineer the specification", 「リバースワークフローで」「既存コードから仕様を起こして」「コードの仕様を明確にしたい」 「このプロジェクトを形式仕様で整理したい」「既存コードをリバースエンジニアリングして」
development1
smt-verify
Convert VDM-SL proof obligations (POs) to SMT-LIB and verify them with the Z3 solver. Triggered by "prove POs", "verify with SMT", "check with Z3", "auto-verify proof obligations", "prove the spec is correct", or "find counterexamples". Also responds to Japanese: 「POを証明して」「SMTで検証して」「Z3で確認して」等。 Used as the next step after PO generation with verify-spec, or for end-to-end PO generation + SMT verification.
testing1
verify-spec
VDM-SL仕様の型チェック、構文検証、証明責務生成を実行するスキル
testing1