counterexample-generator
From the author
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.
Install
npx skills add ArabelaTso/Skills-4-SE --skill counterexample-generator -a claude-code
Installs to .claude/skills/counterexample-generator/ · Each command fetches the skill straight from GitHub with the open skills CLI.
Byte-identical to the scanned commit, with the repository’s licence and a SOURCE.txt.
Want your agent to suggest skills while you type? See how to use skills from your IDE.
Safety checks on SKILL.md
No warnings.
Why 83
aiqbench computes the trust score from public signals. It is not a security audit, so read a skill before you install it.
Similar skills
Closest to this one by what they do and when they are used.
- counterexample-explainerArabelaTso/Skills-4-SEExplain why counterexamples violate specifications by analyzing formal specifications (temporal logic, invariants, pre/postconditions, code contracts), informal requirements (user stories, acceptance criteria), test specifications (assertions, property-based tests), and providing step-by-step traces showing state changes, comparing expected vs actual behavior, identifying root causes, and assessing violation impact. Use when debugging test failures, understanding model checker output, explaining runtime assertion violations, analyzing static analysis warnings, or teaching specification concepts. Produces structured markdown explanations with traces, comparisons, state diagrams, and cause chains. Triggers when users ask why something failed, explain a violation, understand a counterexample, debug a specification, or analyze why a test fails.Testing★ 258
- counterexample-debuggerArabelaTso/Skills-4-SEDebug proof failures using counterexamples from Nitpick (Isabelle) or QuickChick (Coq) to identify specification errors, missing preconditions, and proof strategy issues. Use when: (1) A proof attempt fails and you need to understand why, (2) Counterexamples are generated by Nitpick or QuickChick, (3) Specifications may be incorrect or incomplete, (4) Theorems need validation before proving, (5) Missing preconditions or lemmas need identification, or (6) Proof failures need explanation and correction suggestions. Supports both Isabelle/HOL and Coq equally.Engineering★ 258
- error-explanation-generatorArabelaTso/Skills-4-SEExplains test failures and provides actionable debugging guidance. Use when tests fail (unit, integration, E2E), builds fail, or code throws errors. Analyzes error messages, stack traces, and test output to identify root causes and suggest concrete fixes. Handles pytest, jest, junit, mocha, vitest, selenium, cypress, playwright, and other testing frameworks across Python, JavaScript/TypeScript, Java, Go, and other languages.Testing★ 258
- issue-report-generatorArabelaTso/Skills-4-SEAutomatically generate clear, actionable issue reports from failing tests and repository analysis. Analyze test failures to understand expected vs. actual behavior, identify affected code components, and produce well-structured Markdown reports suitable for GitHub Issues or similar trackers. Use when a test fails, when debugging issues, or when the user asks to create an issue report, generate a bug report, or document a test failure.Testing★ 258
- generate-testscoco-research/cocoUse when asked to generate tests for a file, module or component, to raise coverage, or to bootstrap a suite for untested code. Detects the project's test framework and conventions first, then writes unit, integration and edge-case tests.Testing★ 784
- specification-generatorArabelaTso/Skills-4-SEGenerate formal specifications including preconditions, postconditions, invariants, and contracts from code or requirements. Use this skill when documenting APIs, creating formal verification annotations, defining function contracts, specifying class invariants, writing design-by-contract code, or preparing code for formal verification. Supports multiple specification languages including JML, ACSL, Dafny, Eiffel contracts, and documentation annotations.Planning★ 258
Ratings & reviews
—
no reviews
Tried this skill? Rate it to help others. Sign in
Discussion
Join the discussion. Sign in