Individual skill
counterexample-debugger
Debug 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.
skills/counterexample-debugger/SKILL.md
Source commit 4f38503747e0617504bce5329283ef837d375c09
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- No
- Repository scan complete
- No
- Skill scan complete
- Yes
- Observed behavior
- Not checked yet
- Last checked
- Nov 6, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 259
- Repository last updated
- Aug 21, 2026
- License
- Apache-2.0
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
- claude-skills Repository topic
- metaprogramming Repository topic
- software-development Repository topic
- software-engineering Repository topic
- claude Repository topic
- claude-code Repository topic
- engineering Derived category
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Browse files
SKILL.mdcore · 7,575 bytesreferences/examples.mddoc · 10,129 bytesreferences/nitpick_guide.mddoc · 5,260 bytesreferences/quickchick_guide.mddoc · 7,128 bytes
Read excerpt
# Counterexample-Guided Proof Debugger
Analyze counterexamples from Nitpick or QuickChick to explain proof failures and suggest corrections to specifications or proofs.
## Workflow
### 1. Receive Counterexample Information
Identify what information is provided:
- **Counterexample output**: From Nitpick or QuickChick
- **Failed theorem**: The statement that couldn't be proven
- **Proof attempt**: Any partial proof or tactics tried
- **Context**: Definitions and lemmas involved
