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:

• 「統合ワークフローで開発したい」「一気通貫で」「エンドツーエンドで」
• "Run the full workflow", "end-to-end development"
• 「定義から生成まで」「全フェーズ実行して」
• "Define and generate code for an agent"
• Explicitly requests multiple phases in sequence

Workflow Phases

┌──────────┐    ┌──────────┐    ┌──────────┐    ┌──────────┐    ┌──────────┐
│ 1.DEFINE │───>│ 2.VERIFY │───>│ 3.PROVE  │───>│ 4.GENERATE│───>│ 5.TEST  │
│          │    │          │    │ (optional)│    │          │    │          │
└──────────┘    └──────────┘    └──────────┘    └──────────┘    └──────────┘
     │               │               │               │               │
     ▼               ▼               ▼               ▼               ▼
  .vdmsl         PO list        SMT results     TS/Python        Test
   file         + report        + proofs         code           report

Execution Flow

Phase 0: Session Setup

1. Greet the user and explain the integrated workflow briefly:

   「統合ワークフロー」では、エージェントの契約定義から実装コード生成まで、 5つのフェーズを順番に実行します。途中でスキップや中断も可能です。

2. Gather session parameters:

   • Agent name: What agent are we defining?
   • Starting point: New definition, existing .vdmsl file, or natural language spec (MD)?
     • If existing .vdmsl file: skip to Phase 2 (Verify)
     • If natural language MD file: invoke import-natural-spec first to convert to VDM-SL
   • Target language: TypeScript, Python, or both?
   • SMT verification: Include Z3 automated proving? (requires Z3 installed)

3. Initialize session state (track mentally, no files needed):

   agent_name: <name>
   vdmsl_path: <to be determined>
   target_lang: ts | py | both
   smt_enabled: true | false
   phases_completed: []