model-guided-code-repair
Uses a model checker's counterexample trace to localize the fault in the model, propose a fix, and propagate that fix back to the source code. Use when a model checker (TLC, NuSMV, Spin) finds a violation and you need to turn the trace into a code change, not just understand it.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill model-guided-code-repair100
Quality
100%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
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 capability in formal verification debugging. It uses third person voice, lists concrete actions, includes domain-specific trigger terms that users would naturally use, and explicitly states both what the skill does and when to use it. The narrow focus on model checker counterexamples makes it highly distinctive.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'localize the fault', 'propose a fix', and 'propagate that fix back to the source code'. These are clear, actionable capabilities. | 3 / 3 |
Completeness | Clearly answers both what ('localize fault, propose fix, propagate to source code') and when ('Use when a model checker finds a violation and you need to turn the trace into a code change'). Explicit 'Use when...' clause with clear trigger conditions. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'model checker', 'counterexample trace', 'TLC', 'NuSMV', 'Spin', 'violation', 'trace', 'code change'. Good coverage of domain-specific terms users in this field would naturally use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification tools (TLC, NuSMV, Spin) and counterexample traces. Very unlikely to conflict with general debugging or code analysis skills due to specific domain terminology. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
100%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is an excellent skill that efficiently teaches a complex debugging workflow. It combines clear conceptual framing (the repair loop diagram), concrete methodology (backward trace walking), actionable mappings (model guard to code change table), and a complete worked example. The 'Do not' section adds valuable guardrails without being verbose.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude's competence with model checking concepts. Every section earns its place with no unnecessary explanations of what model checkers are or how they work. | 3 / 3 |
Actionability | Provides concrete, executable guidance with specific examples: the worked example shows exact state traces, guard conditions, and code changes. The mapping table from model guards to code changes is immediately actionable. | 3 / 3 |
Workflow Clarity | Clear 4-step sequence with explicit validation checkpoints. Step 3 explicitly covers re-checking with three possible outcomes and includes deadlock verification. The 'Do not' section reinforces validation requirements. | 3 / 3 |
Progressive Disclosure | Well-structured with clear sections, appropriate cross-reference to related skill (tlaplus-guided-code-repair), and content organized from general workflow to specific example to output format. No unnecessary nesting or monolithic walls. | 3 / 3 |
Total | 12 / 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.
- 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.