smv-model-extractor
Extracts an SMV (NuSMV/nuXmv) finite-state model from code or state-machine descriptions, for CTL/LTL model checking of reactive systems. Use when verifying hardware-adjacent or embedded logic, when the state space is naturally finite and small, or when CTL branching-time properties are needed.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill smv-model-extractor89
Quality
86%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
85%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is a well-crafted technical skill description that clearly defines its purpose and use cases. It excels at specificity and completeness with explicit 'Use when' triggers. The main weakness is that trigger terms are heavily technical jargon, which may not match how users naturally phrase requests for formal verification help.
Suggestions
Add more natural language trigger terms like 'verify state machine', 'formal verification', 'check temporal properties', or 'prove correctness' to improve discoverability
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists specific concrete actions: 'Extracts an SMV model from code or state-machine descriptions' and 'CTL/LTL model checking of reactive systems'. Names specific tools (NuSMV/nuXmv) and techniques. | 3 / 3 |
Completeness | Clearly answers both what ('Extracts an SMV model...for CTL/LTL model checking') and when ('Use when verifying hardware-adjacent or embedded logic, when the state space is naturally finite and small, or when CTL branching-time properties are needed'). | 3 / 3 |
Trigger Term Quality | Includes technical terms like 'SMV', 'NuSMV', 'nuXmv', 'CTL/LTL', 'model checking', 'reactive systems', but these are domain-specific jargon. Missing more natural user phrases like 'verify state machine', 'check properties', or 'formal verification'. | 2 / 3 |
Distinctiveness Conflict Risk | Highly distinctive with specific niche: SMV/NuSMV/nuXmv model extraction for formal verification. The combination of finite-state models, CTL/LTL, and hardware-adjacent logic creates a clear, non-conflicting domain. | 3 / 3 |
Total | 11 / 12 Passed |
Implementation
87%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a high-quality skill that efficiently teaches SMV model extraction with concrete, executable examples and clear comparison to TLA+. The worked example is particularly strong, showing both source code and resulting SMV model. The main weakness is the lack of an explicit extraction workflow with validation steps—the process is demonstrated but not sequenced.
Suggestions
Add an explicit numbered workflow section (e.g., '1. Identify state variables → 2. Map transitions → 3. Bound infinite domains → 4. Run NuSMV to validate syntax → 5. Check properties') with validation checkpoints
Include a brief validation step showing how to run NuSMV/nuXmv to verify the model compiles and check properties (e.g., `nuXmv -int model.smv`)
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude's competence with programming concepts. Every section adds value—comparison tables, code patterns, and worked examples without explaining basic concepts like what enums or switch statements are. | 3 / 3 |
Actionability | Provides fully executable SMV code examples, concrete code-to-SMV translation tables, and a complete worked example with both source C code and resulting SMV model. The extraction patterns are copy-paste ready. | 3 / 3 |
Workflow Clarity | While the extraction process is implicit through the worked example and tables, there's no explicit step-by-step workflow with validation checkpoints. The 'Do not' section provides guardrails but lacks a clear sequence for the extraction process itself. | 2 / 3 |
Progressive Disclosure | Content is well-organized with clear sections (when to use, shape, extraction patterns, worked example, bounding strategies, anti-patterns, output format). For a skill of this size (~100 lines), the structure is appropriate without needing external file references. | 3 / 3 |
Total | 11 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.