Skills Reference

Trigger phrases:

Workflow steps:

1. Gather agent information — name, role, inputs, outputs, relationships
2. Generate type definitions — map natural language to VDM-SL types
3. Define operations and contracts — capture pre/post/inv through questions
4. Generate the VDM-SL specification — complete module with all definitions
5. Review and iterate — present spec for user validation

Built-in templates:

• Transform Agent — stateless input/output conversion
• CRUD Agent — create, read, update, delete with state
• Pipeline Agent — sequential data processing stages
• Mediator Agent — orchestrates multiple sub-agents
• Validation Agent — input validation and sanitization
• Design Document Template (v2.0.0) — Phase 2 protocol/API design documents
• Hybrid Decision Agent (v2.0.0) — score-based compound decisions

Trigger phrases:

Workflow steps:

1. Locate VDM-SL files — find .vdmsl files in workspace
2. Syntax and type checking — run VDMJ with error reporting
3. Generate proof obligations — run VDMJ with -p flag
4. Interpret and explain — translate each PO to plain language
5. Categorize POs — rank by urgency (critical / standard / info)
6. Suggest next steps — offer to proceed to SMT verification

Trigger phrases:

Workflow steps:

1. Accept POs — from verify-spec output or direct input
2. Generate type declarations — map VDM-SL types to SMT-LIB sorts
3. Generate auxiliary definitions — invariants, pre/post as define-fun
4. Convert PO expressions — transform VDM-SL logic to SMT-LIB formulas
5. Negate and check-sat — reflexive verification: assert(not PO)
6. Execute Z3 — run solver on each .smt2 file
7. Interpret results — unsat=proved, sat=counterexample, unknown=timeout

Trigger phrases:

Workflow steps:

1. Read VDM-SL file — parse specification
2. Confirm target language — TypeScript, Python, or both
3. Transform types — map VDM-SL to target language types
4. Generate type definitions — interfaces/dataclasses with invariants
5. Generate contract code — validation functions for pre/post/inv
6. Generate operation stubs — function scaffolds with contract wrappers
7. Output files — save to generated/ directory

Trigger phrases:

Workflow steps:

1. Read the VDM-SL spec and design documents — catalog invariants, contracts, protocol rules
2. Generate type invariant tests
3. Generate pre/post-condition tests
4. Generate protocol tests from the design documents: message-type/payload consistency and state transitions (PROTOCOL.md), API signatures (API-SIGNATURES.md)
5. Generate boundary value tests
6. Output test files — Jest/Vitest compatible

Trigger phrases:

Workflow steps:

1. Parse the spec — identify persistent state: record types, quote unions, state components, invariants, atomic operations
2. Confirm target DBMS (PostgreSQL/MySQL/SQLite) and naming conventions
3. Apply mapping rules R1–R18: record→table, map state→keyed table, quote union→ENUM/CHECK, invariant→CHECK/UNIQUE/FK/trigger, atomic→transaction boundary
4. Generate DEVIATIONS.md (retrenchment table) — record each infidelity with a concrete compensation (trigger / app-layer contract check / contract test)
5. Generate TRACEABILITY.md — map every invariant and operation contract to its enforcement point; no unaccounted invariant allowed
6. Validate the DDL (executable check for SQLite / psql / Docker) and completeness

Trigger phrases:

Workflow steps:

1. Read the spec and split it into modules
2. Collect complexity signals per module (reusing a verify-spec PO report if available)
3. Assign tiers via the scoring rubric (fast paths: types-only → light; any implicit definition → never light)
4. Present the routing table for user confirmation with per-row overrides
5. Write model-routing.json (next to the spec) and MODEL-ROUTING.md

Trigger phrases:

Workflow steps:

1. Session setup — gather agent name, starting point, target language, SMT toggle
2. Phase 1: Define — invoke define-contract for VDM-SL generation
3. Phase 2: Verify — invoke verify-spec for syntax/type/PO checks
4. Phase 3: Prove (optional) — invoke smt-verify for Z3 proving
5. Phase 4: Generate — invoke generate-code for TS/Python scaffolds
6. Phase 5: Test — invoke generate-tests for contract tests, then run them
7. Session report — comprehensive summary of all phases

Trigger phrases:

Workflow steps:

1. Identify the concept — match user question to reference material
2. Provide explanation — plain language with VDM-SL examples
3. Link to context — connect to the user's current specification

Trigger phrases:

Workflow steps:

1. Read and parse the MD document — identify structure, headings, lists, tables
2. Classify requirements — map each to types, constraints, operations, or rules
3. Detect ambiguities — vague quantifiers, undefined terms, missing error cases, boundary conditions
4. Interactive resolution — present ambiguities in priority order, resolve through dialogue
5. Generate VDM-SL — produce tagged specification with [REQ-nnn] traceability
6. Gap analysis — forward/backward/completeness checks
7. Connect to pipeline — recommend verify-spec or refine-spec as next step

Trigger phrases:

Workflow steps:

1. Read VDM-SL specification — catalog types, state, operations, invariants
2. Ask about output preferences — audience, language, format, detail level
3. Translate each construct — types→definitions, pre→prerequisites, post→guarantees
4. Structure the document — overview, glossary, data model, operations, business rules
5. Quality checks — completeness, faithfulness, readability, consistency
6. Save and present — output as Markdown, suggest next steps