Agent skill · Data & Analytics

smv-model-extractor

Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking. Use when users need to: (1) Generate SMV models from program code for verification, (2) Extract state-transition models from protocol implementations, (3) Analyze control flow and data flow to construct formal models, (4) Create models for checking safety and liveness properties, (5) Convert imperative code to declarative state machines. Particularly effective for protocol implementations, concurrent systems, and control logic with clear state transitions.

majiayu000github.com/majiayu000GitHub ↗
claude-codeMIT
Install
npx skills add majiayu000/claude-skill-registry --skill smv-model-extractor --agent claude-code

Same command for any agent — swap --agent for codex, cursor, copilot.

Facts
Files in the skill folder: 2
SKILL.md size: 7 KB
Bundled scripts: none
Path: skills/ai-ml/smv-model-extractor/SKILL.md
Open the folder on GitHub →
Where it comes from
Stars: 534
Language: HTML

Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.

From the SKILL.md

# SMV Model Extractor Automatically extract abstract finite-state models from source code for formal verification with NuSMV model checker. ## Overview This skill transforms imperative programs (C/C++, Java, Python) into declarative SMV models suitable for model checking. It analyzes control flow, data flow, and program variables to construct states and transitions, applying appropriate abstraction to make models tractable while preserving properties of interest. ## Workflow ### 1. Analyze Source Code Read and understand the program structure: ```bash # For single file python3 scripts/extract_model.py program.c -o model.smv # For multiple files python3 scripts/extract_model.py file1.c file2.c file3.java -o model.smv # For entire directory python3 scripts/extract_model.py src/*.py -o model.smv ``` The extractor automatically: - Detects programming language from file extensions - Parses source code into AST - Identifies functions, control structures, and variables - Builds control flow graph (CFG) ### 2. Apply Abstraction The skill uses **medium abstraction** by default (balanced approach): **Data abstraction:** - Booleans → preserved as boolean - Integers → bounded to small ranges (

What's inside
Steps it walks through
  1. Overview
  2. Workflow
  3. 1. Analyze Source Code
  4. 2. Apply Abstraction
  5. 3. Generate SMV Model
  6. 4. Add Verification Properties
  7. 5. Run Model Checker
  8. Common Use Cases
  9. Protocol Implementation
  10. Concurrent System
  11. State Machine
  12. Advanced Options
  13. Focus on Specific Functions
  14. Track Specific Variables
Ships with 1 file
  • metadata.json
Commands it runs
For single file
python3 scripts/extract_model.py program.c -o model.smv
For multiple files
python3 scripts/extract_model.py file1.c file2.c file3.java -o model.smv
For entire directory
python3 scripts/extract_model.py src/*.py -o model.smv
Low abstraction (more detail, larger state space)
python3 scripts/extract_model.py program.c -o model.smv --abstraction low
Medium abstraction (recommended, balanced)
python3 scripts/extract_model.py program.c -o model.smv --abstraction medium
More from claude-skill-registry
All skills →
descriptive-statisticsSummarizing and visualizing data through measures of center, spread, shape, and position. Covers…Data & Analyticsperplexity-researcher-reasoning-proHighest level of research and reasoning capabilities for complex decision-making with significant…OtherretroBrutally honest engineering retrospective. Analyzes git history for what actually happened — not…Data & AnalyticsanalyzeUniversal multi-perspective analyzer for any topic, file, idea, or decision. Extract key points…Otherarize-prompt-optimizationINVOKE THIS SKILL when optimizing, improving, or debugging LLM prompts using production trace data…Data & Analyticscellxgene-contextGuide for integrating CellxGene Census single-cell data with ENCODE bulk experiments. Use when…Data & Analytics
About this skill
What does the smv-model-extractor skill do?

Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking. Use when users need to: (1) Generate SMV models from program code for verification, (2) Extract state-transition models from protocol implementations, (3) Analyze control flow and data flow to construct formal models, (4) Create models for checking safety and liveness properties, (5) Convert imperative code to declarative state machines. Particularly effective for protocol implementations, concurrent systems, and control logic with clear state transitions.

How do I install it?

Run `npx skills add majiayu000/claude-skill-registry --skill smv-model-extractor --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.

Where does this skill come from?

From majiayu000/claude-skill-registry, a repository with 534 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.

Is a popular skill a good skill?

Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.

Keep going
All skills →
The full catalog, by category and by tool.
Open Source Radar →
The repositories these skills come from, watched daily.
The people behind them →
Makers and builders across the ecosystem.