model-guided-code-repair
Automatically repair code violations of temporal properties using model-checking counterexamples as guidance. Use when working with formal verification results, temporal logic property violations (LTL, CTL), model checking counterexamples, or when asked to repair property violations, fix counterexamples, repair temporal properties, fix model checking violations, or repair code based on counterexamples. Applicable to concurrent systems, state machines, synchronization issues, safety/liveness properties, and resource management violations.
87
81%
Does it follow best practices?
Impact
96%
1.26xAverage score across 3 eval scenarios
Passed
No known issues
Quality
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 niche in formal verification and temporal property repair. It provides comprehensive trigger terms covering both technical terminology and user-friendly action phrases, explicitly states when to use it, and is highly distinctive from other potential skills. The description uses proper third-person voice throughout.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'repair code violations of temporal properties', 'using model-checking counterexamples as guidance'. Also specifies applicable domains: concurrent systems, state machines, synchronization issues, safety/liveness properties, resource management violations. | 3 / 3 |
Completeness | Clearly answers both what ('Automatically repair code violations of temporal properties using model-checking counterexamples') AND when with explicit 'Use when...' clause covering multiple trigger scenarios and applicable domains. | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms users would say: 'formal verification', 'temporal logic', 'LTL', 'CTL', 'model checking', 'counterexamples', 'repair property violations', 'fix counterexamples', 'repair temporal properties', 'fix model checking violations'. Includes both technical terms and action-oriented phrases. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche focusing on formal verification and temporal logic - very unlikely to conflict with general code repair or debugging skills. The specific terminology (LTL, CTL, model checking, counterexamples) creates clear boundaries. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
62%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This skill provides a well-structured workflow for model-guided code repair with clear sequential steps and validation checkpoints. However, it lacks concrete executable examples - the 'Common Scenarios' section describes approaches abstractly rather than showing actual counterexample traces and corresponding code repairs. The content would benefit from specific before/after code examples demonstrating the repair process.
Suggestions
Add a concrete worked example showing an actual counterexample trace, the original code, and the repaired code with specific line changes
Include a sample counterexample format (e.g., from SPIN or CBMC) to make the 'Analyze Input' step more actionable
Move the 'Tips for Effective Repairs' section to a separate reference file or remove it - these are generic best practices Claude already knows
Add specific code snippets for common repair patterns (e.g., adding a mutex, inserting a guard condition) rather than just describing them
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is reasonably efficient but includes some unnecessary elaboration. Phrases like 'This skill enables automatic repair' and explanatory sections could be tightened. The 'Tips for Effective Repairs' section contains generic advice Claude already knows. | 2 / 3 |
Actionability | The workflow provides clear steps and structure, but lacks concrete executable examples. No actual code snippets showing repairs, no specific counterexample format examples, and the 'Common Scenarios' section describes rather than demonstrates with real code. | 2 / 3 |
Workflow Clarity | The 7-step sequential workflow is clearly numbered with explicit outputs at each stage. Validation is explicitly addressed in step 6 with two options, and the process includes feedback loops ('Iterate if needed'). The workflow is well-structured for a complex multi-step process. | 3 / 3 |
Progressive Disclosure | The content is well-organized with clear sections, but it's somewhat monolithic. The 'Integration with Model Checkers' section could reference external tool-specific guides. No external file references are provided for detailed scenarios or examples that could reduce the main document length. | 2 / 3 |
Total | 9 / 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.
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- 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.