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

81%

Does it follow best practices?

Impact

96%

1.26x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

92%

33%

Resource Pool Safety Violation

Structured repair output format

Criteria

Without context

With context

Property formalization

30%

100%

Counterexample trace narrative

60%

70%

Root Cause Analysis section

100%

Repair Strategy section

62%

100%

Minimality justification

20%

100%

Behavior Preservation section

75%

100%

Changes Made with line numbers

60%

Validation Results section

75%

100%

Changes marked in code

90%

100%

Correct fix applied

100%

No unrelated changes

33%

83%

100%

10%

Concurrent Counter Race Condition

Minimal synchronization repair

Criteria

Without context

With context

Single change location

100%

No new functions

100%

Narrowest scope fix

100%

Unrelated code untouched

100%

Original variable names preserved

100%

Correct synchronization applied

100%

Control flow preserved

100%

Changes annotated

100%

Minimality stated in report

100%

Validation confirms fix

80%

100%

96%

15%

Network Connection Protocol Liveness Violation

Counterexample-guided test generation

Criteria

Without context

With context

Counterexample translated

70%

100%

States mapped to code locations

60%

100%

Precise root cause

100%

Counterexample path test

100%

Edge case test

100%

Regression tests for happy paths

100%

Correct fix in repaired.py

100%

Repair minimality justified

100%

Changes Made with line numbers

50%

60%

Validation Results references tests

30%

100%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Resource Pool Safety Violation Concurrent Counter Race Condition Network Connection Protocol Liveness Violation

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.