counterexample-to-test-generator
Converts a model checker counterexample trace into an executable test case in the source language, so the bug found in the model is reproducible (and regression-guarded) in the real code. Use when TLC/NuSMV/Spin finds a violation and you want a failing test before writing the fix.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill counterexample-to-test-generator90
Quality
88%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
100%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 an excellent skill description that clearly defines a specialized capability in the formal verification domain. It uses third person voice, provides specific tool names as trigger terms, and explicitly states both what the skill does and when to use it. The description is concise yet comprehensive for its niche audience.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists specific concrete actions: 'Converts a model checker counterexample trace into an executable test case in the source language' with clear purpose 'so the bug found in the model is reproducible (and regression-guarded) in the real code.' | 3 / 3 |
Completeness | Clearly answers both what ('Converts a model checker counterexample trace into an executable test case') AND when ('Use when TLC/NuSMV/Spin finds a violation and you want a failing test before writing the fix'). | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'counterexample trace', 'executable test case', 'TLC', 'NuSMV', 'Spin', 'violation', 'failing test'. These are domain-specific but exactly what users in this niche would mention. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification tools (TLC/NuSMV/Spin) and counterexample-to-test conversion. Unlikely to conflict with general testing or code generation skills due to specific model checker terminology. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
77%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a strong, actionable skill that provides concrete guidance for translating model checker traces into executable tests. The worked example is excellent and the troubleshooting table adds significant value. Minor improvements could be made in conciseness (trimming philosophical framing) and progressive disclosure (separating extended examples).
Suggestions
Trim the opening paragraph's philosophical framing - Claude understands the value proposition without 'proof that the bug exists' elaboration
Consider moving the full worked example to a separate EXAMPLES.md file, keeping just a condensed version inline
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is mostly efficient and provides valuable information, but includes some explanatory text that could be tightened (e.g., the opening philosophical framing, some table explanations). The worked example is appropriately detailed but the surrounding prose could be leaner. | 2 / 3 |
Actionability | Provides fully executable code example in Go, concrete step-by-step process, clear mapping tables, and a specific output format template. The worked example shows exactly how to translate a TLC trace into a deterministic test. | 3 / 3 |
Workflow Clarity | Clear 6-step sequence with explicit validation (step 6: 'If the test passes, your model doesn't match your code'). Includes troubleshooting table for when reproduction fails, and explicit 'Do not' section prevents common errors. The workflow handles the feedback loop of model-code mismatch. | 3 / 3 |
Progressive Disclosure | Content is well-structured with clear sections and tables, but is somewhat monolithic. References to related skills (bug-reproduction-test-generator, program-to-tlaplus-spec-generator) are mentioned inline but the document could benefit from clearer separation of the worked example into a reference file for longer traces. | 2 / 3 |
Total | 10 / 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.