Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add ArabelaTso/Skills-4-SE --skill smv-model-extractorgit clone --depth 1 https://github.com/ArabelaTso/Skills-4-SEWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/arabelatso/skills-4-se/smv-model-extractor)<a href="https://agentmods.dev/skills/arabelatso/skills-4-se/smv-model-extractor"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/smv-model-extractor/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/arabelatso/skills-4-se/smv-model-extractor"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/smv-model-extractor.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector warn
SkillSpector: 1 finding, up to high
These are SkillSpector’s own severities. On a checked sample its high-severity flags on skills were ~96% false positives — a documented command, a public API, a “never do X” rule — so we show them as a caution to read, not a verdict. Why →
- high Memory Poisoning · line 3 Skill manipulates agent memory, state, or stored context. Memory corruption can alter personality, override safety rules, or cause unpredictable behavior.Fix: Protect agent memory and state from modification by untrusted content. Use read-only memory for critical instructions and validate all state changes.
What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00122 | $0.01691 |
| Opus 5 | $0.00061 | $0.00846 |
| Sonnet 5 | $0.00024 | $0.00338 |
| Haiku 4.5 | $0.00012 | $0.00169 |
Grade A, and why
smv-model-extractor scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 9d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 237 lines — stays where its author put it; the contents beside it link to each section on GitHub.
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:
# 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:
# 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
What ships with it
6 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 9d ago First seen · 237 lines · 122 tokens per session scan A d6ab2ea210f4
smv-model-extractor is a skill published in the GitHub repository ArabelaTso/Skills-4-SE (252 stars, last pushed 22d ago), licensed Apache-2.0. It adds 122 tokens to every session and 1,691 once invoked, about $0.0006 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-03.
Other skills, from other repositories
datalad
Retrieve, version, and publish scientific datasets with DataLad and git-annex, and capture computational provenance with datalad run, rerun, and containers-run. Use when cloning or fetching data from OpenNeuro, DANDI, datasets.datalad.org, or any DataLad dataset; when a file in a dataset reads as a broken symlink or a…
depmap
Query the Cancer Dependency Map (DepMap) for cancer cell line gene dependency scores (CRISPR Chronos), drug sensitivity data, and gene effect profiles. Use for identifying cancer-specific vulnerabilities, synthetic lethal interactions, and validating oncology drug targets.
latchbio-integration
Build, register, debug, and operate bioinformatics workflows on Latch using the Python SDK, CLI, Latch Data and Registry, Nextflow, Snakemake, programmatic execution, and Latch MCP. Use when authoring or deploying Latch workflows, configuring resources or interfaces, moving data, integrating Registry, or launching and…
ginkgo-cloud-lab
Submit and manage protocols on Ginkgo Bioworks Cloud Lab (cloud.ginkgo.bio), a web-based interface for autonomous lab execution on Reconfigurable Automation Carts (RACs). Use when the user wants to run protein expression and purification (cell-free, E. coli, or Pichia), HiBiT or A280 or LabChip quantification, IVT…
write-paper
Full-pipeline medical/scientific paper writing. 8-phase IMRAD workflow from outline to submission-ready manuscript. Supports original articles, case reports, case series, meta-analyses, AI validation studies, animal studies, and technical notes. Do NOT trigger for self-checking (use self-review instead).
sync-submission
Audit SSOT-to-submission drift and create journal submission manifests from canonical manuscript artifacts.