Agent 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.

Apache-2.0Auto-check passed

Install Smv Model Extractor

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/smv-model-extractor .claude/skills/smv-model-extractor && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Paste into Claude Code

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .claude/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .agents/skills && cp -r skills-src/skills/smv-model-extractor .agents/skills/smv-model-extractor && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .agents/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/skills/smv-model-extractor .cursor/skills/smv-model-extractor && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .cursor/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/ArabelaTso/Skills-4-SE.git --path skills/smv-model-extractor

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/skills/smv-model-extractor .gemini/skills/smv-model-extractor && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .gemini/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .github/skills && cp -r skills-src/skills/smv-model-extractor .github/skills/smv-model-extractor && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .github/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE smv-model-extractor --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/skills/smv-model-extractor .opencode/skills/smv-model-extractor && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "smv-model-extractor" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/smv-model-extractor into .opencode/skills/smv-model-extractor/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "smv-model-extractor", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: smv-model-extractor
GitHub stars: 253
Token cost: ~1.8k tokens
SKILL.md length: 551 words
Files: 7 (incl. scripts, references)
Skills in repo: 170
Repo updated: Aug 21, 2026
First seen: Oct 9, 2026
Licence: Apache-2.0

At a glance

Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking.

Works in 5 steps: Analyze Source Code → Apply Abstraction → Generate SMV Model → …
Generate SMV models from program code for verification
SKILL.md covers Overview, Workflow, Common Use Cases and Advanced Options, plus 4 more sections
Runs Python scripts from its folder; calls python3

What it does

Smv Model Extractor is an agent skill from ArabelaTso/Skills-4-SE. 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…

Its SKILL.md is about 1.8k tokens, which your agent loads only when the skill is triggered. The skill folder holds 8 other files, including scripts and reference files (for example `references/extraction_patterns.md`, `references/smv_syntax.md` and `scripts/cfg_analyzer.py`).

It works with C++, Java and Python. The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

Generate SMV models from program code for verification
Extract state-transition models from protocol implementations
Analyze control flow and data flow to construct formal models
Create models for checking safety and liveness properties

Example prompts

“/smv-model-extractor”

Requirements

Python 3

Workflow steps

5 steps, taken from the step headings in SKILL.md.

Analyze Source Code
Apply Abstraction
Generate SMV Model
Add Verification Properties
Run Model Checker

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

Tool permissions
Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.
From allowed-tools in the SKILL.md frontmatter.
Runs code
Ships 4 files in scripts/ (Python), which the agent can run.
Shell commands in SKILL.md call:
- python3
From the folder's file list and the shell code blocks in SKILL.md.
Network
No URLs in SKILL.md.
From URLs in SKILL.md, links to its own repository left out.
Credentials
Names no API keys, tokens, secrets or passwords.
From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Smv Model Extractor loads about 1.8k tokens when it runs, and up to ~4.3k if it reads all its reference files. Until then it costs about 154 tokens; SKILL.md has 551 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it: ~154
When it runs · the whole SKILL.md, loaded when a task matches: ~1.8k
With references · SKILL.md plus every file in references/, read only if the agent opens them: ~4.3k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); the scripts in this folder are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 551 words, ~1,838 tokens.

Download SKILL.mdSave it as .claude/skills/smv-model-extractor/SKILL.md (or your agent's skills folder). This skill also uses 6 other files; get the full folder from GitHub.

name: smv-model-extractor
description: 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.

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 (0..3)
Pointers → abstracted to null/valid
Arrays → abstracted to size properties
Enums → preserved as enumerated types

Control abstraction:

Preserve branching (if/else, switch)
Preserve loops (while, for)
Merge sequential statements
Keep function boundaries

Abstraction levels:

bash

# 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

# High abstraction (minimal states, protocol phases only)
python3 scripts/extract_model.py program.c -o model.smv --abstraction high

3. Generate SMV Model

The extractor produces:

model.smv - Complete NuSMV model with:
- MODULE main declaration
- VAR section (state variables)
- ASSIGN section (initial values and transitions)
- Comments explaining structure
model_mapping.txt - Human-readable explanation:
- How program states map to SMV states
- Which variables are tracked
- Transition conditions
- Functions analyzed

Example output structure:

smv

-- SMV Model automatically extracted from source code
MODULE main

VAR
  pc : {s0, s1, s2, s3};  -- program counter
  flag : boolean;
  count : 0..3;

ASSIGN
  init(pc) := s0;
  init(flag) := FALSE;
  init(count) := 0;

  next(pc) := case
    pc = s0 & !flag : s1;
    pc = s1 : s2;
    pc = s2 & count < 3 : s3;
    pc = s3 : s0;
    TRUE : pc;
  esac;

  next(count) := case
    pc = s2 & count < 3 : count + 1;
    TRUE : count;
  esac;

4. Add Verification Properties

After model generation, add temporal logic specifications to verify:

Safety properties (things that should never happen):

smv

-- No buffer overflow
SPEC AG (count <= 3)

-- Mutual exclusion
SPEC AG !(process1_critical & process2_critical)

Liveness properties (things that should eventually happen):

smv

-- Eventually reach goal state
SPEC AF (pc = s3)

-- Request eventually granted
SPEC AG (request -> AF grant)

See smv_syntax.md for complete SMV syntax reference.

5. Run Model Checker

Verify the model with NuSMV:

bash

# Check all specifications
NuSMV model.smv

# Interactive mode
NuSMV -int model.smv

# Generate counterexample if property fails
NuSMV -dcx model.smv

Common Use Cases

Protocol Implementation

Scenario: User has implemented a network protocol and wants to verify correctness.

Approach:

Extract model from protocol implementation
Identify protocol states (handshake, data transfer, teardown)
Add properties: message ordering, no deadlock, eventual completion
Verify with NuSMV

See: extraction_patterns.md for detailed protocol patterns.

Concurrent System

Scenario: Multi-threaded program with shared resources.

Approach:

Extract models for each thread
Model shared variables and locks
Add mutual exclusion properties
Verify no race conditions or deadlocks

See: extraction_patterns.md

Show full SKILL.md (218 more words)Show less

State Machine

Scenario: Program with explicit state variable and transitions.

Approach:

Direct mapping of program states to SMV states
Extract transition conditions
Verify reachability and liveness properties

See: extraction_patterns.md

Advanced Options

Focus on Specific Functions

When codebase is large, focus extraction on relevant functions:

bash

python3 scripts/extract_model.py program.c -o model.smv \
  --focus-functions connect disconnect send_message

Track Specific Variables

Explicitly specify which variables to include in state:

bash

python3 scripts/extract_model.py program.c -o model.smv \
  --track-vars connection_state buffer_count retry_limit

Tips

Start simple: Extract model for single function first, then expand
Check mapping file: Review model_mapping.txt to understand state correspondence
Iterate abstraction: If model checking is too slow, increase abstraction
Add properties incrementally: Start with simple safety properties, then add liveness
Use counterexamples: When property fails, NuSMV provides trace to debug

Common Issues

State explosion: Model has too many states, verification is slow or fails.

Solution: Increase abstraction level, focus on specific functions, bound integer ranges tighter

Over-abstraction: Model is too abstract, properties are trivially true/false.

Solution: Decrease abstraction level, track more variables, preserve more control flow

Missing transitions: Model has deadlocks not present in original program.

Solution: Check transition conditions, ensure all cases are covered, model external events

References

smv_syntax.md: Complete NuSMV syntax reference with examples
extraction_patterns.md: Detailed patterns for protocols, concurrency, state machines

Scripts

extract_model.py: Main extraction script (orchestrates entire process)
cfg_analyzer.py: Control flow graph analysis module
smv_generator.py: SMV model generation module
language_parser.py: Multi-language parser (C/C++, Java, Python)

Files

SKILL.md and 6 other files (scripts, references) in skills/smv-model-extractor of ArabelaTso/Skills-4-SE.

SKILL.md
references/extraction_patterns.md
references/smv_syntax.md
scripts/cfg_analyzer.py
scripts/extract_model.py
scripts/language_parser.py
scripts/smv_generator.py

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Smv Model Extractor next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Smv Model Extractor compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Smv Model Extractor this skillArabelaTso/Skills-4-SE	253	—	~1.8k	Automated safety check: Pass	Apache-2.0	1 mo ago
Fory Releaseapache/fory	4.6k	—	~2.9k	Automated safety check: Pass	Apache-2.0	yesterday
CodeQL Security Scantrailofbits/skills	7.4k	—	~4.6k	Automated safety check: Notes	CC-BY-SA-4.0	2 days ago
Fory Version Bumpapache/fory	4.6k	—	~1.1k	Automated safety check: Pass	Apache-2.0	yesterday
Fory Performance Optimizationapache/fory	4.6k	—	~2.2k	Automated safety check: Pass	Apache-2.0	yesterday
MCP Debuggerdebugmcp/mcp-debugger	172	—	~3.8k	Automated safety check: Pass	MIT	2 days ago

Similar skills

Fory Release
apache/fory
Prepare an Apache Fory release candidate from a clean release branch, including the version bump, RC tag, JVM staging, ASF source artifacts, SVN upload, and vote email.
4.6k GitHub stars~2.9k tokensUpdated yesterday
Auto-check passed
CodeQL Security Scan
trailofbits/skills
Official
Scans a codebase for vulnerabilities with CodeQL's data flow and taint tracking in run-all or important-only modes, including data extensions for project-specific sources and sinks.
7.4k GitHub stars~4.6k tokensUpdated 2 days ago
SecurityAuto-check: notes
Fory Version Bump
apache/fory
Bump Apache Fory release or post-release development versions across Java, Kotlin, Scala, Python, Rust, Go, C++, C, Dart, JavaScript, Swift, integration tests, examples, and source docs.
4.6k GitHub stars~1.1k tokensUpdated yesterday
MobileAuto-check passed
Fory Performance Optimization
apache/fory
Run profile-driven bottleneck optimization across Apache Fory implementations (Java, C++, Python/Cython, Go, Rust, Swift, C, JavaScript/TypeScript, Dart, Kotlin, Scala).
4.6k GitHub stars~2.2k tokensUpdated yesterday
MobileAuto-check passed
MCP Debugger
debugmcp/mcp-debugger
A skill your agent uses when investigating a bug, failing test, or unexpected runtime behavior and the mcp-debugger MCP server is available — drives real step-through debuggers (breakpoints, stack…
172 GitHub stars~3.8k tokensUpdated 2 days ago
DevelopmentAuto-check passed
Dbg
theodo-group/debug-that
Debug applications using the dbg CLI debugger. An agent skill from theodo-group/debug-that.
158 GitHub stars~2.5k tokensUpdated yesterday
DevelopmentAuto-check passed

Questions about Smv Model Extractor

What does Smv Model Extractor do?

Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking. Smv Model Extractor is an agent skill from ArabelaTso/Skills-4-SE. Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking.

When should I use Smv Model Extractor?

Smv Model Extractor fits situations like: generate SMV models from program code for verification; extract state-transition models from protocol implementations; analyze control flow and data flow to construct formal models; create models for checking safety and liveness properties.

How do I install Smv Model Extractor in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a claude-code`. Or copy the skill folder (skills/smv-model-extractor in ArabelaTso/Skills-4-SE) into .claude/skills/smv-model-extractor in your project. Claude Code loads it when a task matches its description.

How do I install Smv Model Extractor in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a codex`. Or copy the skill folder (skills/smv-model-extractor in ArabelaTso/Skills-4-SE) into .agents/skills/smv-model-extractor in your project. Codex loads it when a task matches its description.

Can I use Smv Model Extractor in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractor -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/smv-model-extractor, .gemini/skills/smv-model-extractor, .github/skills/smv-model-extractor and .opencode/skills/smv-model-extractor in your project.

What does Smv Model Extractor need to run?

Going by SKILL.md and its folder, Smv Model Extractor needs Python for the scripts in its folder and the command-line tools its instructions call (python3). Our summary lists: Python 3.

Does Smv Model Extractor access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Smv Model Extractor safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. The check reads SKILL.md only: the scripts in the folder are not scanned, so read them before running anything.

What licence does Smv Model Extractor use?

Smv Model Extractor is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Smv Model Extractor use?

About 1.8k tokens (SKILL.md is roughly 7.4k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 2.5k tokens, read only when the agent opens those files.

What are the alternatives to Smv Model Extractor?

Skills that share tags, products or a category with Smv Model Extractor: Fory Release (apache/fory, 4.6k stars), CodeQL Security Scan (trailofbits/skills, 7.4k stars), Fory Version Bump (apache/fory, 4.6k stars) and Fory Performance Optimization (apache/fory, 4.6k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Smv Model Extractor?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 170 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.

Install Smv Model Extractor

Facts

At a glance

What it does

When your agent uses it

Example prompts

Requirements

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

SMV Model Extractor

Overview

Workflow

1. Analyze Source Code

2. Apply Abstraction

3. Generate SMV Model

4. Add Verification Properties

5. Run Model Checker

Common Use Cases

Protocol Implementation

Concurrent System

State Machine

Advanced Options

Focus on Specific Functions

Track Specific Variables

Tips

Common Issues

References

Scripts

Files

Compare with similar skills

Similar skills

More from ArabelaTso/Skills-4-SE

Related

Questions about Smv Model Extractor