Model-Guided Code Repair

A counterexample trace says "here's a sequence of steps that breaks your property." The repair question is: which step shouldn't have been allowed? Strengthen that step's guard, and the trace is blocked.

For TLA+-specific repair, → tlaplus-guided-code-repair. This skill is the general workflow across checkers.

The repair loop