counterexample-generator

Generate concrete counterexamples when formal verification, assertions, or specifications fail. Use this skill when debugging failed proofs, understanding why verification fails, creating minimal reproducing examples, analyzing assertion violations, investigating invariant breaks, or diagnosing specification mismatches. Produces concrete input values, execution traces, and state information that demonstrate the failure.

1.10x

Quality

73%

Does it follow best practices?

Impact

85%

1.10x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Fix and improve this skill with Tessl

tessl review fix ./skills/counterexample-generator/SKILL.md

Quality

Content

46%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

The body is well-structured and rich with concrete examples, but it is far too long and inlines reference-grade material (patterns, techniques, scenarios, templates) that should live in separate files. Workflow steps are sequenced but lack explicit validation checkpoints and a retry feedback loop.

Suggestions

Move the 7 Counterexample Patterns, the 4 Generation Techniques, the Common Scenarios, and the report templates into separate reference files (e.g., PATTERNS.md, TECHNIQUES.md, REPORT_TEMPLATE.md) and link to them from a concise SKILL.md overview.

Cut explanations of concepts Claude already knows (what a race condition / integer overflow / off-by-one error is) and reduce the 7 patterns + 5 scenarios to a few representative examples, since the scenarios restate the patterns.

Add explicit validation checkpoints and a feedback loop to the workflow — e.g., after Step 4, "If the counterexample does not reproduce the failure, return to Step 3 and adjust inputs" — and show concrete invocations for the SMT/symbolic-execution tools named in the Techniques section.

Dimension	Reasoning	Score
Conciseness	At ~840 lines the body is noticeably verbose: it explains concepts Claude already knows (race conditions, integer overflow, off-by-one) and repeats the same idea across 7 patterns, 4 techniques, 5 scenarios, 10 best practices, and a tools section, with the trailing "Common Counterexample Scenarios" largely restating earlier patterns.	2 / 5
Actionability	Mostly concrete and executable — real Python specs, counterexample values, and step-by-step traces — but the technique sections reference SMT solvers and symbolic execution without showing how to actually invoke them, and some blocks are illustrative traces rather than copy-paste tooling.	4 / 5
Workflow Clarity	A clear five-step sequence (Identify → Analyze → Generate → Execute/Trace → Present) is present and Step 4 verifies the counterexample against postconditions, but there are no explicit validation checkpoints between steps or a feedback loop (e.g., "if the counterexample does not reproduce, return to Step 3").	3 / 5
Progressive Disclosure	No bundle files exist and everything — 7 patterns, 4 techniques, 5 scenarios, report templates, tool lists — is inlined directly in SKILL.md with no references to separate files; hundreds of lines that clearly belong in reference files are not split out, despite reasonable header-level organization.	2 / 5
	Total	11 / 20 Passed

Description

100%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

The description is third-person, concise, and explicitly pairs a clear statement of capability with a rich "Use when..." trigger clause. It names concrete actions and the natural terms users would invoke, with minimal overlap risk.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions across the domain — "Generate concrete counterexamples", "creating minimal reproducing examples", "analyzing assertion violations", "investigating invariant breaks", "Produces concrete input values, execution traces, and state information" — giving comprehensive coverage rather than vague abstraction.	5 / 5
Completeness	Explicitly answers both what ("Generate concrete counterexamples... Produces concrete input values, execution traces, and state information") and when ("Use this skill when debugging failed proofs, understanding why verification fails...") with concrete trigger phrases.	5 / 5
Trigger Term Quality	Covers the natural vocabulary a verification practitioner would actually say — "failed proofs", "assertion violations", "invariant breaks", "specification mismatches", "minimal reproducing examples" — including synonyms and variations rather than only jargon.	5 / 5
Distinctiveness Conflict Risk	Targets a clear niche — counterexample generation for formal verification / specification failures — with distinct triggers that are unlikely to fire for unrelated skills, keeping conflict risk minimal.	5 / 5
	Total	20 / 20 Passed

Validation

93%

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 — 15 / 16 Passed

Validation for skill structure

Criteria	Description	Result
skill_md_line_count	SKILL.md is long (848 lines); consider splitting into references/ and linking	Warning

	Total	15 / 16 Passed

Repository: ArabelaTso/Skills-4-SE
Path: skills/counterexample-generator/SKILL.md
Commit: 4f38503

Reviewed: 9 days 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.