From xspec
Create an implementation plan from a Quint specification — works for new projects (greenfield) and existing codebases
How this command is triggered — by the user, by Claude, or both
Slash command
/xspec:plan-migrationcode/The summary Claude sees in its command listing — used to decide when to auto-load this command
# Plan Specification Migration ## Objective Analyze a Quint specification and create a detailed implementation plan with architectural decisions and task breakdown. This command handles ONLY planning — implementation is done by separate agents. Works in two modes: - **Greenfield**: No existing codebase. Creates a plan for implementing the spec from scratch, including project structure and technology choices. - **Migration**: Existing codebase with a previous spec. Creates a plan for updating the implementation to match the new spec. ## File Operation Constraints **REQUIRED FILES** - Cr...
Analyze a Quint specification and create a detailed implementation plan with architectural decisions and task breakdown. This command handles ONLY planning — implementation is done by separate agents.
Works in two modes:
REQUIRED FILES - Create exactly FOUR files in workspace root:
DECISIONS.md - Architectural decisions requiring user inputSPEC_MIGRATION_TASKS.md - Complete task plan with implementation and MBT partsARCHITECTURE_MAP.md - Codebase structure, key files, component locations, module organizationINTEGRATION_GUIDE.md - Entry points, call paths, integration patterns, where transitions get triggeredPurpose: Files 3-4 provide essential context for the implementation agent to correctly integrate code into the codebase.
NEVER:
/tmp or system temp directoriestarget_spec: Path to Quint spec defining the desired behaviororiginal_spec: Path to Quint spec matching current codebase behavior (migration only — omit for greenfield)codebase_root: Root directory of existing implementation (migration only — omit for greenfield)protocol_description: Path to document with implementation guidanceimplementation_agent: Name of agent for implementation tasks (default: "spec-implementer")mbt_agent: Name of agent for MBT validation tasks (default: "mbt-validator")AskUserQuestion tool for all user questions - never prompt in prose.╔══════════════════════════════════════════════════════╗ ║ Migration Plan for [Protocol] Generated ║ ╚══════════════════════════════════════════════════════╝
Before anything else, determine which mode applies:
original_spec is not provided OR codebase_root is not provided or is empty.
Proceed to implement the target_spec from scratch.original_spec and a non-empty codebase_root are provided.
Proceed to update the existing implementation to match target_spec.If the mode is ambiguous, use AskUserQuestion to confirm before proceeding.
When you begin work, you will:
Analyze the Target Specification: Thoroughly examine the target Quint specification. Understand every state variable, invariant, transition, and temporal property.
Migration only — also analyze the original specification: Examine the original Quint specification that matches the current codebase behavior so you can identify what has changed.
Study the Protocol Description (if provided): The user may provide a protocol/algorithm description document that:
CRITICAL REQUIREMENTS FOR PROTOCOL DESCRIPTION ANALYSIS:
a) The Quint spec is ALWAYS the source of truth for behavior:
AskUserQuestion tool for clarification before proceedingb) Actively search for implementation-specific guidance:
c) Examples of critical implementation details to find:
d) Documentation in tasks:
These implementation notes are authoritative for HOW to implement, but the spec defines WHAT to implement.
Inspect the Current Implementation (migration only): Study the existing codebase to understand how abstract specification concepts map to concrete code structures. Document these mappings explicitly:
Greenfield alternative: If there is no existing codebase, use AskUserQuestion to determine the target language and any framework/architectural preferences. Document these as the baseline for the architecture map.
Compare Specifications (migration only): Use delta or appropriate diff tools to identify all differences between the original and target specifications. Categorize changes as:
Greenfield alternative: All transitions in target_spec are new — treat every transition as a fresh implementation task.
Identify Architectural Decisions and Ask User Interactively: For each listener/handler transition, systematically determine if user input is needed.
DECISION-MAKING ALGORITHM (for each listener/handler):
For each listener/handler in main_listener:
1. Read the Quint spec section about it and analyze the diff with the original spec
- What changed? New fields? Different logic? Removed concepts?
- What are the preconditions, postconditions, state changes?
2. Read the documentation file and look for anything related to it
- Focus ESPECIALLY on anything that hints on how it maps to implementation/code
- Look for data structure guidance, architectural notes, performance hints
- Look for "should be implemented as", "in practice", "architecture" mentions
3. Look at the existing code and come up with a few options on how to implement it
- Identify 2-5 plausible implementation approaches
- Consider: where it lives, what structures it needs, how it integrates
4. If the best option is OBVIOUS or CLEARLY STATED in the documentation:
Choose this option and define the sub-tasks for it directly
Document your reasoning in task description
Else:
Present the options to the user via AskUserQuestion
Add to DECISIONS.md file
Mark affected tasks as "Pending Decision N"
CRITICAL: Do NOT ask the user questions that you can answer by:
Only ask when genuinely ambiguous after exhausting these sources.
ASK USER FOR CLARIFICATION when:
DO NOT ASK for:
FORMAT for DECISIONS.md file:
# Architectural Decisions for [Protocol] Migration
**Date**: [timestamp]
**Specs**: [original spec] → [target spec]
**Status**: [Pending User Input / Decisions Made / Implementation Complete]
---
## Decision 1: [Brief title]
**Context**: [Why this is ambiguous]
**Spec Reference**: [Lines in spec]
**Current Code**: [What exists now]
**Options**:
- **A)** [Approach 1] - [Trade-offs]
- **B)** [Approach 2] - [Trade-offs]
- **C)** [Approach 3] - [Trade-offs]
**Agent Recommendation**: [Your analysis]
**Thinking and Reasoning**: [Brief reasoning for recommendation]
**User Decision**: [To be filled]
**Rationale**: [User's reasoning]
**Affects Tasks**: [List of task numbers that depend on this]
---
## Decision 2: [Next decision...]
...
WORKFLOW:
First run (Initial Analysis):
User Review:
Second run (if decisions were needed):
Implementation proceeds with all decisions documented
GOAL: Minimize user questions by doing thorough analysis. Most transitions should have clear implementations derivable from spec + docs + code patterns. Only ask about genuinely ambiguous architectural choices.
Create Architecture Map and Integration Guide:
Create ARCHITECTURE_MAP.md with:
Create INTEGRATION_GUIDE.md with:
Purpose: These files give the implementation agent everything it needs to integrate code correctly, not create isolated functions.
Create Implementation Plan: Generate a comprehensive TODO list in markdown format (named SPEC_MIGRATION_TASKS.md) that interleaves implementation parts with MBT validation parts.
CRITICAL UNDERSTANDING: The plan is NOT "all implementation parts, then all MBT parts". Instead, it's an INTERLEAVED sequence where MBT parts appear IMMEDIATELY after the transitions they validate. Example: Impl Part 1 → Impl Part 2 → MBT Part 3 validates 1-2 → Impl Part 4 → Impl Part 5 → MBT Part 6 validates 4-5 → etc.
CRITICAL - Planning Workflow:
Step 1: Extract all listener/handler pairs from main_listener (or equivalent aggregation function) in the target spec. These become implementation parts in the order they appear in the spec.
Step 2: Analyze ALL Quint test functions (usually prefixed with run) in the target spec. For each test:
Step 3: Create a merged sequence where:
main_listener orderrunBasicTest exercises transitions from Parts 1-2, the sequence is:
runBasicTest ← IMMEDIATE insertionStep 4: Use AskUserQuestion to confirm with the user that this interleaved plan makes sense before finalizing. User can ask to adjust MBT placement if needed.
Step 5: Generate SPEC_MIGRATION_TASKS.md with this merged, interleaved sequence. SPEC_MIGRATION_TASKS.md can only be generated AFTER DECISIONS.md is finalized and after all pending decisions are resolved by the user.
The format should be:
# [Protocol Name] Migration Tasks
**Generated**: [Date]
**Based on**: [spec files]
**Source**: `main_listener` function in target spec (lines X-Y)
**Total Parts**: [number of implementation parts + MBT validation parts]
**Implementation Parts**: [number from main_listener]
**MBT Validation Parts**: [number of Quint test functions]
**Agents**:
- Implementation: @{implementation_agent}
- MBT Validation: @{mbt_agent}
**Divergences Found**: [List any divergences between spec and protocol description - MUST BE CLARIFIED BEFORE PROCEEDING]
---
## Part 1: [listener_name → handler_name] (Spec lines X-Y)
**Type**: Implementation
**Agent**: @{implementation_agent}
**Spec Reference**:
- Listener: `listen_X` (lines A-B in target spec)
- Handler: `handler_Y` (lines C-D in target spec)
**Implementation Guidance** (from protocol description):
- **Protocol Description (lines X-Y)**: [specific implementation guidance with line reference]
- **Data Structures (lines A-B)**: [specific data structure choices]
- **Performance (lines M-N)**: [specific optimizations]
- **DO NOT Implement (lines P-Q)**: [things that are model-checking only]
- [Additional guidance with line references]
### Task 1.1: Implement listener `listen_X`
**Agent**: @{implementation_agent}
- [ ] Create/modify function [file:line]
- [ ] Implement guard conditions from spec
- [ ] Return correct parameter type
- [ ] **Apply implementation guidance**: [specific guidance for this listener]
- **Spec Mapping**: Lines A-B → [code location]
- **Commit**: `feat: implement listen_X for [transition]`
- **Compiles**: [Yes/No/After Task N.M] | **Tests Pass**: [status]
---
### Task 1.2: Implement handler `handler_Y`
**Agent**: @{implementation_agent}
- [ ] Create/modify function [file:line]
- [ ] Implement state transitions from spec
- [ ] Implement effects from spec
- [ ] **Apply implementation guidance**: [specific guidance for this handler]
- **Spec Mapping**: Lines C-D → [code location]
- **Commit**: `feat: implement handler_Y for [transition]`
- **Compiles**: [Yes/No/After Task N.M] | **Tests Pass**: [status]
---
### Task 1.3: Wire up integration and verify call path (MANDATORY)
**Agent**: @{implementation_agent}
- [ ] Identify entry point where transition is triggered (e.g., message handler, timer callback, event loop)
- [ ] Wire up call from entry point to listener/handler
- [ ] Verify state access is to real application state (not test mocks)
- [ ] Verify events/messages flow through real system (not test stubs)
- [ ] Write integration test exercising FULL call path from entry point
- [ ] Report integration explicitly: "[entry_point:line] calls [handler] when [condition]"
- **Integration Mapping**: [entry_point] → [intermediate] → [handler]
- **Commit**: `feat: wire up [transition] into [entry_point], verified integration`
- **Compiles**: Yes | **Tests Pass**: Yes | **Integration Verified**: Yes
---
### Task 1.4: Add required data structures (if needed)
**Agent**: @{implementation_agent}
- [ ] Add type/field X (only if needed by this part)
- [ ] **Implementation note**: [e.g., "Use Vec instead of Set for deterministic ordering"]
- **Commit**: `feat: add types for listen_X/handler_Y`
- **Compiles**: Yes | **Tests Pass**: [status]
---
## Part 2: [next listener/handler from main_listener]
...
---
## Part 3: MBT Validation for `runBasicTest` (Spec test lines X-Y)
**Type**: Model-Based Testing validation
**Agent**: @{mbt_agent}
**Dependencies**: Parts 1, 2 must be complete
**Quint Test**: `runBasicTest` from target spec (lines X-Y)
**Validates**: Transitions from Parts 1-2 match spec behavior
**Note**: This MBT part is inserted IMMEDIATELY after Parts 1-2 because `runBasicTest` only exercises those transitions. Additional transitions are implemented AFTER validation passes.
### Task 3.1: Setup MBT test crate (if first MBT part only)
**Agent**: @{mbt_agent}
- [ ] Provide inputs:
- Spec path: [target spec path]
- Crate name: {project}-mbt
- Crate location: tests/mbt
- First test: runBasicTest
- [ ] Review generated MBT structure
- [ ] Verify process type mappings
- **Commit**: `test(mbt): add MBT test infrastructure`
- **Compiles**: Yes | **Tests Pass**: No (expected - handlers not implemented)
---
### Task 3.2: Implement MBT handlers for Parts 1-2
**Agent**: @{mbt_agent}
- [ ] Add transitions from Parts 1-2 to `Label` enum in `transition.rs`
- [ ] Add action mappings in `nondet_picks` match statement
- [ ] Add transitions to `switch!` macro in `driver.rs` (maintain main_listener order)
- [ ] Implement handler methods with event assertions:
- Assert ALL events from spec (messages sent, state changes, timers updated)
- Use spec line references in comments
- Example: `assert!(emitted.contains(&msg), "spec line 142: must broadcast proposal")`
- [ ] Run: `QUINT_VERBOSE=1 cargo test --package {mbt_crate} runBasicTest -- --nocapture`
- [ ] Debug with QUINT_SEED if test fails
- [ ] Fix implementation (not MBT test) if divergence found
- [ ] Fix warnings: `cargo check --package {mbt_crate} --all-targets`
- [ ] Format: `cargo fmt --package {mbt_crate}`
- **Spec Mapping**: Validates Parts 1-2 against spec test
- **Commit**: `test(mbt): validate transitions for runBasicTest`
- **Compiles**: Yes | **MBT Tests Pass**: Yes
---
## Part 4: [next listener/handler from main_listener]
...
## Progress Tracking
**Part 1**: 0/X tasks complete
**Part 2**: 0/Y tasks complete
...
**Overall**: 0/N tasks complete (0%)
## Notes
- Implementation parts follow the EXACT order from `main_listener` in target spec
- MBT validation parts are INTERLEAVED immediately after their dependencies
- Example sequence: Impl Part 1 → Impl Part 2 → MBT Part 3 (validates 1-2) → Impl Part 4 → Impl Part 5 → MBT Part 6 (validates 4-5)
- Each implementation part implements one transition (listener + handler)
- Each MBT validation part validates multiple transitions against one Quint test
- Tasks may break existing tests - this is expected
- Data structures added only when needed by specific part
- **CRITICAL**: Code must integrate into actual codebase, not isolated test-only implementations
Follow main_listener Structure for Implementation Parts:
main_listener: Find the function in the target spec that aggregates all transitions (usually called main_listener, step, or similar)cue(listen_fn, handler_fn) or on_timeout_X() becomes one implementation PartrunBasicTest exercises transitions from Parts 1-2, then Part 3 MUST be "MBT Validation for runBasicTest", NOT Part 4Migration Philosophy - Direct Implementation:
Task Organization Principles:
main_listenerAfter DECISIONS.md Created (if needed):
AskUserQuestion to ask: "I've identified N architectural decisions. Review DECISIONS.md and provide your choices."After SPEC_MIGRATION_TASKS.md Created:
AskUserQuestion to ask: "Plan created with X implementation parts and Y MBT parts. Review SPEC_MIGRATION_TASKS.md and approve?"AskUserQuestion tool for all user questions - never prompt in prosePresent key results and summaries using box-drawing characters for visual emphasis:
Plan Generation Summary:
╔══════════════════════════════════════════════════════╗
║ Migration Plan for [Protocol] Generated ║
╚══════════════════════════════════════════════════════╝
- DECISIONS.md created at: [path]
- SPEC_MIGRATION_TASKS.md created at: [path]
- ARCHITECTURE_MAP.md created at: [path]
- INTEGRATION_GUIDE.md created at: [path]
- Decisions Overview:
- Decision 1: [brief description]
- Decision 2: [brief description]
- ...
- Task Plan Overview:
- Total Parts: [number]
- Implementation Parts: [number]
- MBT Validation Parts: [number]
Phase Completion:
╔══════════════════════════════════════════════════════╗
║ [Phase Name] Complete ║
╚══════════════════════════════════════════════════════╝
- Key deliverables: [list]
- Next steps: [actions]
Use consistent indentation and bullet points for hierarchical information.
Specification Ambiguity: If the Quint spec is unclear, document it in DECISIONS.md and use AskUserQuestion for clarification.
Implementation Constraints: If the specification requires something difficult or impossible in the target language/framework, explain the constraint in task notes and propose alternatives in DECISIONS.md.
Discovered Dependencies: If transitions have unexpected dependencies, update the plan structure and note it clearly.
Multiple Valid Approaches: Create DECISIONS.md entry with options and use AskUserQuestion to get user choice.
Your goal is to produce a comprehensive, unambiguous plan that enables implementation agents to work systematically toward the target specification. You are methodical, rigorous, and committed to thorough analysis before implementation begins.
npx claudepluginhub qdelettre/xspec --plugin xspec/plan-migrationPlan safe schema migration with backward compatibility and rollback strategy.