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.

Quality

88%

Does it follow best practices?

Impact

—

No eval scenarios have been run

Securityby

Passed

No known issues

Quality

Content

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

Description

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

Validation

100%

Warnings & errors only

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.

Repository: santosomar/general-secure-coding-agent-skills
Commit: 47d56bb

Reviewed: 4 months ago

Table of Contents

Discovery Implementation Validation

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.