For a long time I dismissed loop invariants as an academic exercise. The textbook examples were always something like "after the kth iteration of this loop, the first k elements of the array are sorted", which felt like a tautology dressed up in formalism. I had never seen a working engineer write one in real code. Then I shipped a bug in a binary search implementation that took out a service for forty minutes, and the postmortem turned up something interesting: a one-line comment stating the loop invariant would have caught the bug at code review time. I did not write that comment. Nobody on the team did, because nobody had ever written one before. I have been a convert ever since.

This article is the working-engineer's case for loop invariants. Not the proof-of-correctness exercise from a 1985 textbook, but a practical tool for catching off-by-one bugs, fence-post errors, and the silent miscalculations that make a loop "almost work" on small inputs and fail on the boundaries.

What a loop invariant actually is

A loop invariant is a statement that is true at the start of every iteration of a loop. It must hold at three specific moments: before the loop runs the first time (initialisation), at the end of every iteration just before the next one starts (maintenance), and when the loop exits (termination). Together those three checkpoints prove the loop does what its author thinks it does.

The phrasing matters. A good invariant is a precise statement about the state of variables at iteration boundaries. "The array is sorted" is too vague. "After iteration k, the elements arr[0..k-1] are sorted and contain the smallest k elements of the original input" is precise; it tells you exactly what relationship between the loop counter and the array state holds at every step.

The three checkpoints, in order:

1. Initialisation. When the loop starts, the invariant is true. For most loops this is trivial; before iteration zero, the empty subarray is trivially sorted.
2. Maintenance. If the invariant is true at the start of an iteration, it is still true at the start of the next one. This is the heart of the proof; you assume the invariant, run one iteration, and check it still holds.
3. Termination. When the loop exits, the invariant combined with the exit condition tells you something useful about the final state. This is what proves the loop achieves its goal.

The pattern is exactly the same as induction. Initialisation is the base case; maintenance is the inductive step; termination is the conclusion you draw from the loop having run to completion.

A worked example: insertion sort

Here is the classical loop invariant for insertion sort, but written the way I actually want to see it in a code review.

def insertion_sort(arr):
    # Loop invariant: at the start of iteration i, arr[0..i-1] is sorted
    # and contains the original elements in some permuted order.
    for i in range(1, len(arr)):
        key = arr[i]
        j = i - 1
        # Inner invariant: arr[j+1..i-1] is the contiguous block of elements
        # that were greater than key and have been shifted right by one slot.
        while j >= 0 and arr[j] > key:
            arr[j + 1] = arr[j]
            j -= 1
        arr[j + 1] = key
    return arr

The two comments do real work. The outer invariant tells the reviewer what the loop is supposed to maintain across each pass. The inner invariant tells them what the inner loop has accomplished after each shift. If a reviewer reads the comment and then watches the code mutate the array, they can directly check whether the comment is still true after the iteration. If the code is wrong, the discrepancy between code and comment is the bug.

For this function: at termination, i = len(arr), so the outer invariant says arr[0..len(arr)-1] is sorted and is a permutation of the original. That is the definition of the function being correct.

The bug a one-line invariant would have caught

Here is the binary-search bug I shipped, simplified.

def find_first_geq(arr, target):
    lo, hi = 0, len(arr)
    while lo < hi:
        mid = (lo + hi) // 2
        if arr[mid] >= target:
            hi = mid
        else:
            lo = mid + 1
    return lo

The function is supposed to return the index of the first element >= target, or len(arr) if no such element exists. The intended invariant: at every iteration, arr[lo..hi-1] contains the answer if it exists. The exit condition lo == hi says we have narrowed the range to a single point (or zero elements, if no answer). Combined with the invariant, that point is the answer.

The bug I shipped was subtle: I had hi = mid + 1 in the first branch instead of hi = mid. Both pass simple tests where the answer is found early, but with hi = mid + 1 the invariant is violated and the loop fails to make progress. After the assignment, arr[lo..hi-1] still includes mid; the search range has not actually shrunk. Concretely, whenever the range narrows to two elements with arr[mid] >= target (so mid + 1 == hi), the update sets hi = mid + 1 = hi, which is a no-op, and the loop spins on the same range forever. In production this manifested as a small subset of queries hanging until the service hit its request budget and started shedding load.

If I had written the invariant as a comment: # Invariant: arr[lo..hi-1] still contains the answer if any; arr[hi..] is past the answer; arr[..lo-1] is too small, the broken assignment would have stuck out. After if arr[mid] >= target: hi = mid + 1, the new range arr[lo..hi-1] still includes mid, even though mid was just confirmed to be a candidate. The body claims to narrow the search range; the assignment does not. Reading the comment alongside the assignment, the mismatch is obvious in a way it never is when you only read the code. Code review would have caught it.

How I use invariants in code review

I do not write invariants for every loop. That would be exhausting and most simple loops do not benefit from them. The cases where I always ask for an invariant comment are:

• Binary search and any divide-and-conquer that maintains a window of "still-possible" indices. These functions are notorious for off-by-one bugs and subtle directional asymmetries.
• Two-pointer and sliding-window code where the relationship between the two pointers (and their state) is non-obvious. "Right pointer always sits on the next character to absorb; left pointer sits on the leftmost character still in the window" is a useful sentence to write.
• Loops that mutate a data structure as they iterate, where the invariant explains what subset has been processed and what state it is in.
• Any loop with a non-trivial exit condition (more complex than i < len(arr)), because the invariant combined with the exit condition is what proves the function is correct.

When I write the invariant, I write it as a comment immediately above the loop. One sentence is usually enough. If I cannot fit it in one sentence, that is itself a sign that the loop is doing too much and might want to be split into two.

The phrasing trick that makes invariants useful

The mistake I made early on was writing invariants that were either trivially true ("the array exists") or restatements of the loop body ("we have iterated i times"). Those are useless. The two phrasings that make invariants do work:

The first phrasing: describe what each portion of the data structure represents at iteration boundaries. "Elements arr[0..i-1] are sorted; elements arr[i..] are unprocessed" partitions the array into known and unknown regions, and the loop body's job is to grow the known region by one. After the loop, the known region is everything.

The second phrasing: describe a relationship between variables. "acc holds the sum of arr[0..i-1]" is a relationship between two state variables (acc and i) and one piece of input data (the prefix of arr). Loop iterations preserve the relationship by updating both sides.

When you read a loop with one of these phrasings as a comment, your eye naturally checks: does the code body preserve this? If acc is supposed to hold the sum of the prefix and the body says acc += arr[i]; i += 1, yes. If the body says acc = arr[i]; i += 1, no. The phrasing makes the bug visible.

The three failure modes invariants catch

In my own code reviews, the three patterns I have caught with invariant analysis:

1. Off-by-one on the loop boundary. The invariant says "arr[0..i-1] processed" but the loop runs for i in range(len(arr) + 1) or terminates at i = len(arr) - 1. The exit-condition mismatch is visible the moment you write the invariant down.

2. Wrong update direction. Two-pointer code where the invariant says one pointer should not regress, but a branch advances both pointers when one should stay still. Without the invariant, "advance both" looks symmetric and pleasant. With the invariant, it is clearly wrong.

3. State drift across iterations. A running accumulator (sum, max, frequency map) that is supposed to mirror the prefix of input, but a branch forgets to update it. The invariant acc reflects arr[0..i-1] is silently violated; the invariant comment forces you to re-justify it after every assignment.

A loop invariant is the comment your future self needs

I want to make a small philosophical point. Code is read more than it is written, and loops are some of the densest code there is. A loop invariant is not just a proof technique; it is a comment that tells the future reader (probably you, six months from now) what the loop is trying to do. It is also a contract that lets a code reviewer disprove the loop without simulating it.

The bug that started this article got me a forty-minute outage and a bad night of sleep. The fix was three characters. The diff that prevented it forever after was one comment line. That ratio is the argument for invariants. They are cheap to write, they communicate intent precisely, and they turn the bug from "you have to simulate the loop in your head to catch it" into "you have to compare the code against one sentence in English and notice the mismatch". One of those review modes scales; the other does not. I have seen too many off-by-one bugs to believe the textbook framing is just academic. It is the cheapest correctness tool I have, and I keep it in my back pocket for any loop that has even mild boundary subtlety.