Individual skill
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.
skills/smv-model-extractor/SKILL.md
Source commit 4f38503747e0617504bce5329283ef837d375c09
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- Yes
- Repository scan complete
- No
- Skill scan complete
- No
- Observed behavior
- Local scripts
- Last checked
- Nov 11, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 260
- Repository last updated
- Aug 21, 2026
- License
- Apache-2.0
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
- claude-skills Repository topic
- metaprogramming Repository topic
- software-development Repository topic
- software-engineering Repository topic
- claude Repository topic
- claude-code Repository topic
- data Derived category
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Browse files
SKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesSKILL.mdcore · 7,359 bytesreferences/extraction_patterns.mddoc · 6,440 bytesreferences/smv_syntax.mddoc · 3,396 bytesscripts/cfg_analyzer.pyruns · 5,523 bytesscripts/extract_model.pyruns · 3,169 bytesscripts/language_parser.pyruns · 7,744 bytesscripts/smv_generator.pyruns · 6,676 bytes
Read excerpt
# 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:
