Practical guide
Prove an invariant beyond a bounded search
Checking a few transitions can find a bug. Induction adds an argument that a property continues to hold beyond the searched prefix.
The base and step have separate jobs
The base checks the property over the selected initial prefix. The step assumes it over a sequence of states and asks whether the next transition can violate it. Together, discharged obligations can establish an unbounded invariant. Kind2 documentation explicitly requires both base and step; the step engine alone is insufficient.
Illustrative model: a bounded counter
Initial: count = 0
Transition:
if count < 3: next_count = count + 1
otherwise: next_count = 0
Property: 0 <= count <= 3
Initialization satisfies the bound. From a nonnegative count below three, incrementing reaches at most three; from three, reset reaches zero. This gives a one-step inductive argument for the stated integer model. It is mathematical reasoning, not a reported solver run or a claim about unspecified machine arithmetic.
A failed step may reveal a missing invariant
The step can consider property-satisfying states that initialization never reaches. A counterexample there may show the property is not inductive in its present form without showing a real execution bug. Inspect the missing reachable-state relationship. Increasing k or adding a justified strengthening invariant may help. An unsupported assumption can instead hide the problem.
Identify the actual analysis path
Kind2 provides multiple techniques. A Proof command checking contract realizability is not synonymous with k-induction over production code. Name the transition system, property, engine and result. For direct analysis of a compatible Kind2 model, the documented invocation enables both engines:
kind2 --enable BMC --enable IND model.lus
Keep the conclusion at the modeled scope
A successful argument concerns the initial states and transition relation supplied to the tool. It does not establish that code has identical arithmetic, scheduling or environmental behavior. Retain source correspondence and tests for those boundaries. Unknown or exhausted resources leave the claim undecided; neither is a proof nor necessarily a reachable counterexample.
Follow the evidence
Write the initialization and preservation argument for one property you want to prove.
Review one inductive claim. Bring the transition model and property so we can assess initialization, preservation and the assumptions behind the intended conclusion.