← Policy gallery

counterexample_triggers_fix

formal-reasoning reasoning pure_temporal formal-verificationbugsfixes

When a verification goal is refuted (counterexample found), a fix action should follow.

Formula

G(Verify ∧ refuted → F(EditFile))

Hover any operator or symbol for what it means.

Why it matters

Finding a bug via formal verification is only useful if the bug gets fixed. A refutation should lead to a code change.

Examples

passes Verify(refuted: capture bug) → AnalyzeCode → EditFile(fix)

fails Verify(refuted) with no subsequent edit

Use it

ponens policies add counterexample_triggers_fix --into ./trace.json
ponens trace check ./trace.json