I don't think the utility of invariants is restricted to proving program correctness, as is suggested by a number of commenters in this thread. Instead, they identify some underlying structure in your problem, and that structure can be exploited to simplify your method of calculation.
Another great example of exploiting a (not-really-loop) invariant to design an algorithm is Sean Parent's implementation of a generic 'gather' algorithm, which takes advantage of the fact that the set of objects below/above the gathering point is unchanged, allowing you to split the problem into two easier sub-problems. Here's his explanation and implementation (video should be linked to 16:50):