invariant-inference
Installation
SKILL.md
Invariant Inference
A loop invariant is what stays true every time you hit the loop head. Verifiers need it stated; programmers rarely state it. This skill guesses it from evidence.
Two routes to an invariant
| Route | How it works | Good at | Bad at |
|---|---|---|---|
| Dynamic (Daikon-style) | Run the code, record state at loop head, generalize patterns | Concrete relationships in traces | Generalization — might be coincidence |
| Static (template-based) | Guess invariants of form ax + by ≤ c, solve for a,b,c |
Sound by construction | Limited to the template shapes |
Do both: dynamic finds candidates fast; static checks them.
Dynamic — the observe-and-generalize loop
- Instrument. At every loop head, dump all local variable values.
- Run on a bunch of inputs. The more diverse, the better.
- Mine patterns across the dumps. What's true at every observation?
- Filter for inductiveness. A pattern true by coincidence won't survive the inductive check.