reverse-workflow

Reverse Workflow — Spec Extraction, Refinement, & Code Reconciliation

Overview

This skill orchestrates the full reverse engineering pipeline for formalizing existing code: Extract → Refine → Reconcile → (optionally) Verify → Prove → Generate → Test

Each phase invokes an existing skill, with automated handoff, error recovery, and a final session report summarizing all results.

この skill は既存コードを形式化するためのリバースエンジニアリング pipeline 全体をオーケストレートする。 各フェーズは既存スキルを呼び出し、フェーズ間の自動ハンドオフ、エラー回復、 最終セッションレポートの生成を行う。

┌─────────────┐     ┌──────────────┐     ┌──────────────┐     ┌──────────────┐
│ 1. EXTRACT  │────>│ 2. REFINE    │────>│ 3. RECONCILE │────>│ 4. VERIFY    │
│ 仮仕様抽出   │     │ 対話的磨き上げ │     │ コード照合     │     │ (既存スキル)  │
└─────────────┘     └──────────────┘     └──────────────┘     └──────────────┘
                          ▲  │                                      │
                          │  ▼                                      ▼
                     収束するまで                              既存フォワード
                     サイクルを回す                            パイプラインへ接続
                                                               (verify/prove/generate/test)

Trigger Conditions

Activate this skill when the user says any of:

• 「リバースワークフローで」「既存のコードから仕様を起こして」
• "Run reverse workflow", "extract and refine spec from code"
• 「コードの仕様を明確にしたい」「このコードを形式的に整理したい」
• "Reverse engineer this code", "formalize the existing implementation"
• 「既存コードをVDM-SLで仕様化して」「コードベースをリバースエンジニアリングして」
• Explicitly requests extraction, refinement, and/or reconciliation in sequence

Workflow Phases

┌──────────┐    ┌──────────┐    ┌────────────┐    ┌──────────┐    ┌──────────┐
│ 1.EXTRACT│───>│ 2.REFINE │───>│ 3.RECONCILE│───>│ 4.VERIFY │───>│ 5.PROVE  │
│ 抽出      │    │ 磨き上げ  │    │ 照合       │    │ 検証     │    │ 証明     │
└──────────┘    └──────────┘    └────────────┘    └──────────┘    └──────────┘
                      ▲ │
                      └─┘
                   収束ループ
                  (forward pipeline
                   に接続可能)

Execution Flow

Phase 0: Session Setup

1. Greet the user and explain the reverse workflow:

   「リバースワークフロー」では、既存のコードから形式仕様を起こし、 対話を通じて真の仕様を明確にして、最後にコードと仕様を照合します。 4～7つのフェーズを順番に実行します。途中でスキップや中断も可能です。

2. Emphasize the core principle:

   「コードから抽出した仕様は『仮の仕様』です。本当の仕様はあなたの頭の中にあります。」

3. Gather session parameters:

   • Project name: What is this codebase called?
   • Source code files/directories: Which files or directories should we analyze?
   • Source language: TypeScript, Python, Java, Go, or auto-detect?
   • Existing artifacts: Are there tests, documentation, or comments explaining behavior?
   • Target language for new code (if reconcile phase generates): TypeScript, Python, or both?
   • Connect to forward pipeline: After reconciliation, should we verify/prove/generate?
   • SMT verification: Include Z3 automated proving? (requires Z3 installed)

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

   project_name: <name>
   source_paths: [<paths>]
   source_lang: ts | py | java | go | auto
   provisional_spec_path: <to be determined>
   confirmed_spec_path: <to be determined>
   target_lang: ts | py | both
   forward_pipeline: true | false
   smt_enabled: true | false
   phases_completed: []
   

セッションパラメータを収集し、内部状態を初期化する。

Phase 1: Extract — Provisional Spec Extraction

Invoke: extract-spec skill

1. Follow the extract-spec SKILL.md flow
2. Analyze source code and extract structural information
3. Generate .provisional.vdmsl file with all items tagged [PROVISIONAL]
4. List all uncertainties and questions for the user

extract-specスキルの対話フローに従い、コード分析を実施する。

Handoff criteria → Phase 2:

• ✅ .provisional.vdmsl file generated
• ✅ Extraction report generated
• ✅ Questions list prepared
• ✅ User acknowledges provisional nature

Error recovery:

• If code is unparseable → Ask user to narrow scope to specific functions/classes
• If no types/functions found → Verify scope and ask user to point out key areas
• If user unsure about extraction → Proceed to Phase 2 to refine through dialogue

Phase report:

📋 Phase 1 Complete: Provisional Spec Extraction
- File: <project_name>.provisional.vdmsl
- Types extracted: <count>
- Functions/Operations: <count>
- State variables: <count>
- Questions for user: <count>
- Confidence level: <High|Medium|Low>

Phase 2: Refine — Dialogue-Driven Refinement

Invoke: refine-spec skill

1. Follow the refine-spec SKILL.md flow (may loop multiple times)
2. Present extracted items and ask clarifying questions
3. For each item, determine:
   • Confirmed: Correct as extracted, user agrees
   • Modified: Correct concept but needs adjustment
   • Removed: Not part of the true spec
   • Unresolved: Too unclear to resolve now; mark and continue
4. Build Findings Report:
   • Bugs discovered in the code
   • Gaps between code and intended behavior
   • Refinements to the specification
   • Intentional design decisions (code is correct as-is)
   • Technical debt items
5. Generate confirmed .vdmsl (no [PROVISIONAL] tags)

refine-specスキルの対話フローに従い、仕様の明確化を実施する。

Convergence cycles: This phase may loop multiple times until:

• All [PROVISIONAL] items are classified (Confirmed/Modified/Removed/Unresolved)
• User feels confident about the specification
• No new questions emerge from previous round

収束するまで複数回ループする場合がある。

Handoff criteria → Phase 3:

• ✅ All [PROVISIONAL] items classified
• ✅ Findings Report generated (bugs, gaps, refinements, intentional, debt)
• ✅ Confirmed .vdmsl file generated (no [PROVISIONAL] tags)
• ✅ User approves confirmed specification

Error recovery:

• User very unsure about an item → Mark [UNRESOLVED] and continue with rest
• New questions surface during refinement → Document and address in next loop
• Conflicting evidence → Present all interpretations, let user choose

Phase report:

📋 Phase 2 Complete: Specification Refinement
- Confirmed items: <count>
- Modified items: <count>
- Removed items: <count>
- Unresolved items: <count> (marked [UNRESOLVED])
- Convergence rounds: <count>
- Findings Report:
  - Bugs: <count>
  - Spec gaps: <count>
  - Refinements: <count>
  - Intentional: <count>
  - Technical debt: <count>

Phase 3: Reconcile — Code Alignment & Fix Generation

Invoke: reconcile-code skill

1. Read confirmed .vdmsl specification
2. Read source code
3. Compare specification against code:
   • Does code implement all specified operations?
   • Do pre/post-conditions match code behavior?
   • Are invariants enforced in the code?
   • Are there type mismatches?
4. Generate diff report:
   • Operations that don't match spec
   • Missing runtime checks
   • Potential bugs in code
5. Generate code fixes:
   • Add contract checks (pre/post/invariant)
   • Fix logic bugs if identified
   • Add missing operations (as stubs if needed)
6. Generate auto-generated tests based on confirmed spec
7. Validate fixes (run tests if runtime available)

reconcile-codeスキルの対話フローに従い、コード照合を実施する。

Handoff criteria → Phase 4 (Forward Pipeline):

• ✅ Diff report generated
• ✅ Code fixes generated (or identified for manual application)
• ✅ Auto-generated tests created
• ✅ User reviews and approves fixes

Error recovery:

• Fix conflicts with other code → Present alternatives or mark for manual review
• Tests fail → Diagnose and adjust fixes
• Missing functionality too complex → Generate stub with TODO and explanation

Phase report:

📋 Phase 3 Complete: Code Reconciliation
- Diff report: ✅ Generated
- Code fixes: <count> issues identified
  - Type mismatches: <count>
  - Missing contracts: <count>
  - Logic bugs: <count>
- Auto-generated tests: <count>
- Tests status: ✅ All passing  (or ⚠️ <N> failing)

Phase 4: Verify — Forward Pipeline Entry (Optional)

Invoke: verify-spec skill (from integrated-workflow)

Skip condition: User chose forward_pipeline: false in Phase 0, or user says "stop here". If skipped, proceed directly to Session Report.

1. Run VDMJ on the confirmed .vdmsl file (syntax check → type check → PO generation)
2. Explain each error or PO in natural language
3. Categorize POs by urgency (Critical, Standard, Info)

既存のverify-specスキルを使用して、確認済み仕様を検証する。

Handoff criteria → Phase 5:

• ✅ Syntax check: PASSED
• ✅ Type check: PASSED
• ✅ POs generated and explained

Error recovery:

• Syntax/type errors found → show errors with fix suggestions → return to Phase 2 for spec correction
• After fix → re-run Phase 4

Phase report:

📋 Phase 4 Complete: Specification Verification
- Syntax check: ✅ PASSED
- Type check: ✅ PASSED
- Proof Obligations: <total_count>
  - Critical: <count>
  - Standard: <count>
  - Info: <count>

Phase 5: Prove — SMT Automated Proving (Optional)

Invoke: smt-verify skill (from integrated-workflow)

Skip condition: User chose smt_enabled: false in Phase 0, or Z3 is not available. If skipped, proceed directly to Phase 6 or Session Report.

1. Convert each PO to SMT-LIB format
2. Run Z3 on each .smt2 file
3. Report results per PO (unsat → proved, sat → counterexample, unknown → undetermined)

既存のsmt-verifyスキルを使用して、PO を Z3 で証明する。

Handoff criteria → Phase 6:

• ✅ All POs processed (proved, counterexample, or unknown)
• ⚠️ If counterexample found: warn user and offer to return to Phase 2 to fix spec

Error recovery:

• Counterexample found → explain the violation → offer to return to Phase 2 to fix the spec
• Z3 timeout → note as "unresolved" and continue

Phase report:

📋 Phase 5 Complete: SMT Automated Proving
- Total POs: <count>
  - ✅ Proved: <count>
  - ⚠️ Counterexample: <count>
  - ℹ️ Unknown/Timeout: <count>

Phase 6: Generate & Test (Optional)

Invoke: generate-code skill (from integrated-workflow)

Skip condition: User chose not to generate new code in Phase 0. If skippe

Content truncated.