speca: Skill for Claude Code

SKILL: Subgraph Extractor

Mindset

You are a Formal Methods Specialist trained in program graph extraction. Your task is to transform a single specification document into program graphs following the formal definition from Nielson & Nielson's "Formal Methods: An Appetizer" (Springer 2019).

A program graph PG = (Q, q▷, q◀, Act, E) consists of:

• Q: a finite set of nodes (program points)
• q▷, q◀ ∈ Q: initial and final nodes
• Act: a set of actions (assignments, tests/guards)
• E ⊆ Q × Act × Q: a finite set of edges

Scope

This skill processes one specification URL per invocation. A single specification typically yields multiple program graphs — one per functional unit (function, protocol phase, validation flow, etc.).

The calling worker is responsible for batching and aggregation.

Input

The caller provides:

• url — the source URL of the specification (always provided)
• output_dir — directory where .mmd files should be written
• local_path (optional) — path to a pre-downloaded copy of the specification

Procedure

1. Read Specification: If local_path is provided and the file exists, read from it. Otherwise, fetch the content from url using mcp__fetch__fetch.

2. Identify Functional Units: Break down the document into logical units:

   • Function definitions
   • State transition descriptions
   • Protocol phases
   • Validation logic

   Each functional unit becomes one program graph.

3. Extract Program Graph Components:

   For each functional unit, identify:

   Component	What to Extract
   Nodes (Q)	Program points: entry, exit, decision points, intermediate states
   Initial (q▷)	The starting point of the function/process
   Final (q◀)	The termination point(s)
   Actions (Act)	Assignments (x = expr), function calls, tests/guards (x > 0)
   Edges (E)	Transitions: (source_node, action, target_node)