formal-agent-contracts

形式的エージェント契約を定義し、VDM-SL仕様と設計文書（プロトコル仕様）を生成するスキル

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をドキュメントにして」「仕様書をエクスポートして」「形式仕様を読みやすくして」 「非エンジニア向けの仕様書を作って」「仕様のドキュメントを生成して」

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: 「既存のコードから仕様を抽出して」「コードの仕様を形式化して」 「コードベースを分析して」「コードをリバースエンジニアリングして」

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).

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.