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.

1.26x

Quality

69%

Does it follow best practices?

Impact

96%

1.26x

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/model-guided-code-repair/SKILL.md

Quality

Content

56%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 a well-structured, clearly sequenced repair workflow with a useful output template, but it is hampered by redundancy across sections, no inline executable code or tool commands, and an orphaned reference file that duplicates inlined content without being linked.

Suggestions

Link references/temporal_logic_patterns.md from the relevant workflow step (e.g., step 3/4 or a 'Reference' section) and trim the inlined 'Common Scenarios' repair strategies that duplicate it, so SKILL.md stays an overview pointing to detail.

Replace the vague 'Execute the model checker on the repaired code' with concrete per-tool commands (e.g., SPIN/NuSMV/CBMC invocations) or point to the reference for runnable examples.

Collapse 'Tips for Effective Repairs' into the workflow steps it duplicates (minimality, structure preservation, side effects) to remove redundancy and tighten the body.

Dimension	Reasoning	Score
Conciseness	Mostly efficient and free of basic-concept padding, but the 'Tips for Effective Repairs' and 'Common Scenarios' sections restate minimality, structure-preservation, and repair-strategy points already covered in the workflow, so it could be tightened; not a 4 due to this redundancy.	3 / 5
Actionability	Concrete workflow steps, named repair strategies, and a copy-pasteable output-format template give actionable guidance, but the body contains no executable code or actual tool commands (validation says 'Execute the model checker' without specifics), leaving key execution details missing.	3 / 5
Workflow Clarity	A clear seven-step sequence with an explicit validation step (step 6, two options) and per-step Output markers; falls short of 5 because the error-recovery feedback loop is only a single 'Iterate if needed' tip rather than an integrated validate-fix-retry cycle.	4 / 5
Progressive Disclosure	Good section structure, but the existing references/temporal_logic_patterns.md bundle file is never linked from the body while violation patterns and repair strategies that overlap it are inlined, so references are not signaled and content that could be deferred is inline.	3 / 5
	Total	13 / 20 Passed

Description

82%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 a strong, explicit what-and-when statement with distinct formal-verification triggers and minimal conflict risk. Its only weakness is that the action vocabulary is essentially a single 'repair' verb repeated in several phrasings rather than multiple distinct concrete actions.

Dimension	Reasoning	Score
Specificity	Names the domain (temporal properties, model checking) and a concrete core action ('repair code violations ... using model-checking counterexamples as guidance'), but the remaining verbs are repetitions of 'repair/fix' rather than additional distinct concrete actions, so it is not comprehensive enough for a 4.	3 / 5
Completeness	Clearly answers 'what' ('Automatically repair code violations of temporal properties using model-checking counterexamples as guidance') and 'when' with an explicit 'Use when ...' clause listing concrete trigger phrases, matching the 5 anchor.	5 / 5
Trigger Term Quality	Strong keyword coverage with natural synonyms users would say ('repair property violations', 'fix counterexamples', 'fix model checking violations', LTL/CTL, formal verification); falls just short of a 5 because the terms are somewhat repetitive rephrasings rather than a broad set of distinct natural variants.	4 / 5
Distinctiveness Conflict Risk	Occupies a clear niche (model-guided repair of temporal-property violations via counterexamples) with highly specific formal-verification triggers, making conflict with other skills minimal.	5 / 5
	Total	17 / 20 Passed

Validation

100%

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

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Path: skills/model-guided-code-repair/SKILL.md
Commit: 4f38503

Reviewed: 19 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.