What Is a Loop Invariant? The Concept Behind Correct Loops

Binary search is four lines. You've probably written it twenty times. And somewhere in your commit history, there is a version with a subtle bug that only surfaces on even-length arrays, or when the target is the last element, or under conditions you never thought to test.

The code wasn't wrong. You were. You wrote the loop without stating what it was supposed to maintain. Loop invariants fix that.

Say It in One Sentence

A loop invariant is a property about your program's state that holds true before the loop starts, at the beginning of every iteration, and when the loop terminates.

That's the whole definition. What makes invariants powerful is the three-condition framework for proving they hold. That's where the real thinking happens, and also where most people close the tab because it sounds like a math class.

Every Correct Loop Satisfies Three Conditions

Cormen, Leiserson, Rivest, and Stein (CLRS, the algorithms textbook you definitely finished) codify loop invariant proofs into three properties:

Initialization. The property holds before the first iteration. Your base case.

Maintenance. If the property holds at the start of any iteration, it still holds at the start of the next one. Your inductive step.

Termination. When the loop exits, the invariant combined with the exit condition gives you exactly the result you wanted.

The structure is identical to mathematical induction. CLRS says so explicitly. Verify all three conditions and you have a correctness proof, not just a test that happened to pass.

The three-condition loop invariant proof framework showing Initialization, Maintenance, and Termination

Insertion Sort Proves the Pattern

Here is insertion sort:

def insertion_sort(arr: list[int]) -> None:
    for j in range(1, len(arr)):
        key = arr[j]
        i = j - 1
        while i >= 0 and arr[i] > key:
            arr[i + 1] = arr[i]
            i -= 1
        arr[i + 1] = key

The invariant for the outer loop: at the start of iteration j, the subarray arr[0..j-1] contains the original first j elements in sorted order.

Check it:

Initialization (j = 1): arr[0..0] is one element. One element is trivially sorted. Holds.
Maintenance: The inner loop inserts arr[j] into its correct position in arr[0..j-1], shifting larger elements right. After insertion, arr[0..j] is sorted. Holds for the next iteration.
Termination (j = n): The invariant says arr[0..n-1] is sorted. That's the entire array. Done.

This is why CLRS opens with insertion sort. The invariant is easy to state in plain English, and each condition is easy to check. Once you see the pattern, you can apply it anywhere.

Binary Search Is Where It Actually Bites

Binary search is the loop invariant that matters most in coding interviews. Almost every off-by-one bug in binary search is an invariant failure wearing a disguise.

You pick mid + 1 vs mid based on vibes. Something breaks on even-length arrays. You spend twenty minutes poking at boundary conditions until your test cases pass. Then you ship it and call it done.

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

The invariant: if target exists in the array, it must be at some index in arr[lo..hi].

Initialization: lo = 0, hi = n - 1 covers the entire array. Trivially true.
Maintenance: When arr[mid] < target, we know target isn't at mid or below, so lo = mid + 1 preserves the invariant. Symmetric for hi = mid - 1.
Termination: lo > hi means the search space is empty. The invariant guarantees that if target were present, it would be in that empty range. It isn't. Return -1.

The invariant tells you that you've already checked mid and eliminated it. Write lo = mid instead and you'd never shrink the search space. The loop runs forever on certain inputs.

For what it's worth: Java's standard library shipped (low + high) / 2 for the midpoint in Arrays.binarySearch(). That expression overflows for large arrays. It sat in production for nine years before Joshua Bloch caught it in 2006 and wrote a blog post about it. Java. Standard. Library. Nine years. Without an invariant to check against, the bug looked completely fine.

The boundary bug and the full Java story are in the binary search off-by-one guide. For the complete invariant treatment, see Binary Search: One Invariant to Rule the Search Space.

Every Off-by-One Error Is a Broken Loop Invariant

Worth stating directly. When you choose between while i < n and while i <= n, you're choosing between two different invariants. The question is never which one feels right. The question is which one your loop body preserves and which one gives you the right state at termination.

Most off-by-one errors come from one of two places. Either the invariant was never stated, so there was no way to check it was being maintained. Or the loop body came first and the boundary conditions were tweaked until tests passed.

That's guessing. Dressed up as iteration.

Write the invariant before writing the loop body. It forces you to specify what "correct state" means before you write code that's supposed to produce it. Slower at the start. Much faster once you realize you're not spending 45 minutes debugging boundary conditions by feel.

Two Pointers and Sliding Window Have Invariants Too

They're just rarely stated explicitly, which is why people memorize these patterns as templates instead of understanding them.

The two-pointer technique on a sorted array maintains this invariant: every pair with both indices left of left sums to less than the target, and every pair with both indices right of right sums to more. That's why you can advance each pointer without backtracking. The invariant guarantees you haven't skipped a valid pair.

The sliding window technique maintains a different one: the window [left, right] always satisfies whatever constraint you're optimizing for. Advancing right expands the window. When the constraint breaks, advance left until it holds again. By the time right reaches the end, you've considered every valid window.

Knowing these invariants is what lets you write these patterns from scratch. You're not copying a template. You're following a property your loop must maintain.

What the Interviewer Is Actually Asking

When an interviewer says "walk me through why this is correct," they want you to state and verify a loop invariant. They won't use that language.

The answer is three sentences. What property does your loop maintain? Why does each iteration preserve it? What does the property tell you when the loop exits? Answer those three questions and you have a correctness argument that sounds rigorous, because it is.

You don't need to say "by the loop invariant." That's unnecessarily formal for a 45-minute interview. But saying the invariant out loud, before you write the first line of the loop body, is what separates code you can defend from code you're hoping is correct. Interviewers can tell the difference. They've seen both many times.

Put it on the whiteboard. Say it to the interviewer. Write it as a comment at the top of the function. It doesn't matter where it lives. What matters is that you stated the property before you wrote code that's supposed to maintain it.

If you want to drill this under real interview pressure, SpaceComplexity runs voice-based mock interviews where you explain your reasoning out loud in real time, including why your loop terminates and handles edge cases. Knowing something and explaining it live are different skills. The gap is wider than you think.

Invariants Generate Algorithms, Not Just Verify Them

Here's the less obvious use, and honestly the more satisfying one once it clicks.

You can design a loop by starting from the invariant you want, then figuring out what the body must do to maintain it.

Take the partition step in quicksort. You want to rearrange elements around a pivot. Instead of working out the right swaps from intuition, state the invariant first: at each iteration, all elements at indices less than i are strictly smaller than the pivot, and all elements between i and j haven't been examined yet. The loop body writes itself. If the current element at j is smaller than the pivot, swap it to position i and advance both pointers. Otherwise, just advance j.

You haven't memorized the algorithm. You've derived it. You started with a property you wanted to be true and worked backward to code that makes it true. This is how the people who designed these algorithms actually thought about them. Invariant first. Code second. It's a slower start. The debugging stage is dramatically faster.