counterexample-to-test-generator

Automatically generates executable test cases from model checking counterexample traces. Translates abstract counterexample states and transitions into concrete test inputs, execution steps, and assertions that reproduce property violations. Use when working with model checker outputs (SPIN, CBMC, NuSMV, TLA+, Java PathFinder, etc.) and needing to create regression tests, validate bug fixes, or reproduce verification failures in executable test suites.

1.16x

Quality

85%

Does it follow best practices?

Impact

99%

1.16x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

100%

Reproducing a State Machine Bug Found by Formal Verification

NuSMV counterexample to Python test

Criteria

Without context

With context

pytest framework used

25%

100%

Setup phase present

87%

100%

Execution phase present

87%

100%

Assertion phase present

87%

100%

Traceability comments

100%

Concrete value mapping

100%

Property violation comment

100%

Mapping document produced

100%

Execution instructions provided

100%

Expected behavior documented

100%

Model checker format identified

100%

Non-default values documented

100%

97%

22%

Creating a Regression Test from a Memory Safety Violation

CBMC counterexample to C++ Google Test

Criteria

Without context

With context

Google Test framework

100%

Setup phase initializes CE state

87%

100%

Execution phase replays steps

87%

100%

Assertion phase targets violation

75%

100%

Traceability comments

80%

100%

Concrete values used

100%

Minimal complexity

62%

Property context comment

87%

100%

Mapping document produced

88%

100%

Execution instructions provided

50%

100%

Expected failure described

87%

100%

Model checker identified

100%

11%

Turning a Verification Trace into a Java Regression Test

JPF non-determinism and traceability

Criteria

Without context

With context

JUnit framework used

100%

Non-determinism documented

83%

100%

Setup phase initializes CE state

100%

Execution phase replays transitions

100%

Assertion phase targets violation

100%

JPF traceability comments

90%

100%

Concrete values used

100%

Property context comment

100%

Mapping document produced

100%

Execution instructions provided

100%

Expected failure described

100%

Model checker identified

100%

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

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

Table of Contents

Reproducing a State Machine Bug Found by Formal Verification Creating a Regression Test from a Memory Safety Violation Turning a Verification Trace into a Java Regression Test

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.