Suppose that we have an infinite model. In that case exploration is not feasible. Instead we can find an inductive invariant, prove that it is inductive, then prove that it proves our invariants.
For example suppose we want to prove Inv. Then we discover some other invariant SysInv and show:
SysInv holds for all InitSysInv holds for all NextSysInv proves Inv