Agent Claude Code
IC3/PDR generalization step — given one counterexample-to-induction (CTI), propose ONE new invariant conjunct that blocks it and is as weak as possible. Dispatched by /lean4-ic3. Stateless, single-shot, no file edits.
14 28d ago A 58 tokens
Apache-2.0