We spend a lot of effort making code run and almost none making it argue. An invariant is the cheap proof tool that turns “I think this loop is right” into “I know it is” — and we already use them without naming them.

The series so far has been about making code simpler: flattening control flow , then reshaping conditions and their algebra . Simpler code is code we can reason about, and invariants are how we do the reasoning — Dijkstra’s teaching, in everyday JavaScript.

Why not just lean on tests? They earn their place — but they sample behavior, they don’t prove it. A green suite says the cases we thought of still pass, not that the code is right; coverage counts the lines we ran, not the cases we checked. That argument has a post of its own — TDD as religion .

Invariants are the other side of it. A real program is a complex system , too big to test exhaustively, and — outside rare efforts like seL4 or CompCert that consumed years of specialist work — too big to verify formally end-to-end. So when we need to know, we reason locally: pick a fact and show the code keeps it true wherever it matters. Such a fact is an invariant.

What is an invariant?

An invariant is a statement that is true at a particular point every time control reaches it — no matter which path got us there or how many times we have looped. The art is choosing a statement strong enough to be useful and simple enough to check.

An invariant can be materialized: an assert, an if/throw, or a check in a test. Mostly, though, it stays a virtual construct — a comment, or just a thought. An assert is where reasoning and testing meet: it records the invariant the argument proves and samples it at runtime, on whatever paths reach it.

The theory traces to Floyd–Hoare logic and Dijkstra’s predicate transformers — starting points for the math, not prerequisites for the rest of this post.

Straight-line code is the easy case: each statement just updates what we already know — the types, ranges, and relationships of our variables — so its invariant is nothing more than that running tally of facts, and changing a line forces a re-read only of the code below it. Branches and loops are where it gets real — many paths, repetition, the same point reached different ways — and that is where we need an invariant.

Let’s look at the two constructs that matter most: loops and conditions.

Loop invariants: before, during, after

The classic shape has three obligations. Pick a property P and show:

• Initialization — P holds before the first iteration.
• Maintenance — if P holds at the top of an iteration, the body leaves it holding at the bottom.
• At exit — P plus the exit condition gives us the result we wanted.

The small example everyone has written, with the invariant stated out loud:

let sum = 0;
// our `sum` represents summed values of an empty array: 0
for (let i = 0; i < a.length; ++i) {
  // invariant: `sum` equals the total of a[0 .. i-1]
  sum += a[i];
  // invariant: `sum` equals the total of a[0 .. i]
}
// on exit i === a.length, so `sum` is the total of a[0 .. length-1] -- the whole array

Nothing changed about the code. What changed is that the comment pins down why the loop is correct, and it tells us what would break it: an i that starts at 1, a <= in the test, a += that runs twice. It is also exactly as precise as its terms: for floats, “the total” means the left-to-right floating-point sum, nothing stronger.

One caveat. The invariant proves partial correctness: if the loop ends, the answer is right. It does not prove the loop ends at all. For that we need a second argument. We pick a quantity that strictly decreases and cannot drop below zero. Dijkstra called it the bound function; most people say loop variant. Here it is a.length - i. It falls by one each pass and stops at zero. So the loop terminates.

That clean ending — the invariant plus a single exit condition — assumes there is one way out. A break adds another: the exit condition becomes a set, one entry per exit, and the invariant has to combine with each of them to give a valid result. So an early break is something to reason through, not sprinkle in.

These show up everywhere once we look for them. Here is one from everyday code.

Collecting paginated reads

const fetchAll = async query => {
  const items = [];
  let cursor = null; // read() returns the first page for a null cursor
  do {
    // invariant: `items` holds every record of the pages read so far
    const page = await read(query, cursor);
    items.push(...page.items);
    cursor = page.next; // null only on the last page
  } while (cursor);
  // on exit the page just read was the last,
  // so `items` holds every record -- the whole result set
  return items;
};

The invariant is the ledger: items matches the pages read so far. The exit supplies the last fact — page.next is null only on the last page — so when the loop stops, the page just read was the final one, “read so far” is “all of them”, and items is the whole result set. The argument also tells us what would break it: forget the cursor = page.next and the loop still terminates — after the first page, with cursor never moved off null, returning one page as if it were everything. Nothing hangs, nothing throws; what broke is the exit’s premise that the loop stops only past the last page. A wrong answer is quieter than an infinite loop — stating the argument is how we notice.

Once an invariant is explicit, we can capture it. Abstract a loop into a combinator and the invariant rides along: reduce captures the accumulation loop’s invariant shape, stated once and reused for every accumulation — the reducer we hand it still has to be right.

Invariants are also the foundation under the classics: every recursive algorithm rests on the fact its recursion preserves, and every dynamic programming table maintains an invariant per cell — “this entry answers this subproblem” — as it fills. Recursion combinators are invariants made reusable — I wrote about them long ago. For the underlying theory, see loop invariant .

if and block invariants

A branch follows the same discipline as a loop, but two cases are worth keeping apart.

A guard is an assertion. if (!user) return; barely branches the logic — it states a precondition for every line below it:

if (!user) return;
// invariant past this line: `user` is truthy -- every line below may assume it

That return is also an exit, so a function needs the same care a loop with break does: several returns mean several exits, and the function’s contract — what it takes and what it promises — must hold at each. State that contract once and we can reason about the body in isolation, then lean on it at every call site without re-opening the function.

A block has an invariant after it — one that does not depend on the condition. Whatever an if/else does inside, what matters downstream is the single fact true after it, the same on every path:

let greeting;
// `greeting` is `undefined`
if (typeof name === 'string' && name) {
  // `name` is a non-empty string
  greeting = `Hello, ${name}!`;
} else {
  // `name` has an unsupported value
  greeting = 'Hi, anonymous!';
}
// block invariant: `greeting` is a properly formatted string -- whichever branch ran

That last line is the payload. Code after the if leans on the block invariant, not on the branches.

Where does that compound fact come from? From the branches. Each branch establishes its own invariant. For the whole statement to have one, those invariants must line up: the same fact on every branch, or complementary facts that compose into one. Both branches here make greeting a valid string — the same fact — so the compound invariant is that. When the branches establish unrelated facts, there is no compound to state, and that is the signal to reformulate. (When they differ only in a value — as these do — the whole if collapses to a ternary: same invariant, less code. The long form stays on the page only so we can see the branches.)

Every block leaves an invariant

The examples above are instances of one rule, and the rule is the point of the post: any block — a loop, an if, a switch, a function, a braced group of statements — can be characterized by the invariant it leaves behind. If we can’t state that invariant, the block is doing too much; reformulate it until we can. A switch makes this vivid:

let rate;
switch (tier) {
  case 'gold':   rate = 0.2; break;
  case 'silver': rate = 0.1; break;
  default:       rate = 0;
}
// block invariant: `rate` is a defined discount for any `tier`

Here the cases are complementary: each handles one tier, and the default completes the cover, so together they compose one block invariant — rate is defined for any tier. Drop the default and the cover has a hole; an unknown tier leaves rate undefined and the compound breaks. The fix is restoring the missing case so the invariant holds again — the invariant told us the block was incomplete.

Modern languages bake this in

We don’t always track these by hand — a good type system does some of it for us.

TypeScript narrows types along branches. Write if (item instanceof Gizmo) and inside the block item is a Gizmo, checked by the compiler. That is the branch invariant, tracked for us. We can also name our own: a type predicate (x is Gizmo) teaches the compiler our check, and an assertion signature (asserts x is Gizmo) is a materialized invariant the rest of the code may then lean on.

It can enforce the whole-block invariant too. Over a discriminated union, assign the unhandled value to never in the default and the compiler rejects any case left unhandled — the incomplete cover from the switch above, turned into a compile error. The hole moves — a typed tier cannot be unknown, but the union can grow a member nobody handles — and the check closes it:

type Tier = 'gold' | 'silver';

const rate = (tier: Tier): number => {
  switch (tier) {
    case 'gold':   return 0.2;
    case 'silver': return 0.1;
    default: {
      const _exhaustive: never = tier; // add 'bronze' and this stops compiling
      return 0;
    }
  }
};

Rust makes the check mandatory. A match must be exhaustive — cover every variant, or add a _ arm — or the program does not compile. Where TypeScript lets us opt in, Rust’s compiler insists the branches compose into a whole.

Why this pairs with simpler control flow

Invariants are cheap to state only when control flow is simple. A flat loop has one invariant; a loop with a couple of breaks and a flag variable has a different fact true at each exit:

let found = false, result = null;
for (let i = 0; i < items.length; ++i) {
  if (items[i].ok)    { result = items[i]; found = true; break; }
  if (items[i].fatal) break;  // give up
}

At the bottom, what holds depends on which exit fired — a hit, a fatal abort, or a clean exhaustion. Three facts where we wanted one, and the found flag papers over the gap without closing it: a fatal abort and a clean exhaustion leave the same found === false, so a difference the loop seemed to care about is not even representable downstream. No single invariant to lean on; every line below re-asks which case it is in.

The cure is the rule from above — reformulate until the invariant is stateable. Give the loop a boundary and let the contract be the single fact:

const firstUsable = items => {
  for (const item of items) {
    if (item.ok) return item;    // the hit
    if (item.fatal) return null; // give up
  }
  return null;                   // exhausted
};
// contract: the first ok item, unless a fatal one precedes it; null otherwise
const result = firstUsable(items);
// single fact: `result` is the item to use, or null

The three exits are still there, but each return now answers to the function’s contract — the same obligation several returns carried in the guard section — and downstream sees one fact: result is the item or null. The flag is gone because it encoded nothing result does not. Fatal and exhausted still look the same to the caller — but now the contract says so, “null otherwise”, a decision on record rather than an accident of a flag. And if a caller ever does need to know why nothing was found, that is a new contract to state, not a flag to bolt back on.

So the tactics from the earlier posts are not just aesthetic — flatter flow and simpler conditions are what make a correctness argument fit in our heads.

Jumps are the sharpest case. Used carelessly, a break or continue multiplies the exits to reason about. Used with discipline, each one can be placed so the loop’s invariant still holds where it lands — a later post makes that argument for break, continue, and even a well-mannered goto.

How it pays us back

A test and a proof differ in when they pay. A test runs on the inputs we chose and reports on those alone, so it runs again on the next ones, and again, forever. A proof covers every input and every path that reaches the line — the runs we never tried included — and it is made once, as the code is written; re-running it proves nothing new. The proof is banked at writing time and pays back on every run after.

There is also a definition of done. We wrote a function; instead of verifying the invariants in its loops and branches, we run it on some inputs and check the outputs — N times. Is N enough? A thousand? Who knows — no count of samples closes the question: unless the tests are aimed at the code’s actual structure — its branches and paths — a suite is a Monte Carlo run on our own code. The obligations of an invariant are finite and listable: initialization, maintenance, the exits — and for a function that fits on a screen, with its few loops and handful of branches, the whole list is short; linearized flow keeps it shorter still. Often that is fewer invariants than tests, covering everything rather than sampling. Check them all and we are done — and we know we are done.

A test also sees the function from outside: input in, output out. Even a green suite says only “it works” — nothing about how; the implementation and its cost are invisible to it. Invariants live inside. They state what the loop maintains, and the bound function states how fast the work shrinks — the seed of a complexity argument. That is knowledge about the algorithm itself, not just its answers.

Can the argument itself be wrong? Of course — the same way a test can check the wrong thing. That is no reason to drop the method: mathematics has worked this way all along, by proofs, not by tests. No paper announces “we tried the formula 1,875 ways and it held” — it argues, the argument gets checked, and a flawed proof is answered by a better proof. The craft is to get better at arguing. (The longer case for that stance is TDD as religion .)

The proof comes due again when a premise moves: a rewrite of that code, or a change in the contracts it assumes. And staleness cuts both ways — a stale test goes green on wrong code; a stale invariant comment misleads the next reader with no red light at all, since nothing runs it. What the proof keeps is locality: every block carries its own invariant, so we know where the re-argument starts — the block we changed. Finding everyone who leaned on its old guarantee is the harder half, and the next section is about it.

Paying the piper

Invariants have a real weakness, and it is tooling. State one and almost nothing tracks it. The type system catches the thin slice it can encode — change a string to a number and tsc lights up every caller — but most invariants aren’t types: a range, an ordering, “non-empty past this line.” Rewrite what a function guarantees rather than what it returns, and nothing flags the callers that leaned on the old guarantee; we hunt them by hand. In the mainstream there is no reasoner that re-checks our code, and the code depending on it, for the contradictions a change induces, and no way to ship a function with its invariants attached so a consumer could verify against them. The outliers exist — Eiffel ships contracts with the code, Dafny and SPARK verify them statically — but they stayed niches.

The nearest tool is property-based testing: QuickCheck and its descendants (fast-check in JS, Hypothesis in Python) take a stated invariant and hammer it with generated inputs — sampling rather than proof, but the invariant is doing the work. Yet it is barely on the radar. Across 659 sessions on the published schedules of eight major Python and JS conferences this year — PyCon US and EuroPython included — exactly one covers property-based testing and none cover invariants or formal correctness. Nor is this year special: across eleven years and 1,007 PyCon US talks, property-based testing made the title three times; invariants, formal methods, and correctness — never. Testing at large holds a steady 4% of the slots throughout. (Hypothesis did run as a hands-on tutorial three years in a row — the interest exists at the margin; the headline slots go elsewhere.)

On the teams I have worked with, nothing beyond extensive testing — automated suites plus human testers — was ever in play. That says less about the tools than about the habit: the invariant is the part nobody reaches for. In the languages most of us use, stating invariants is manual work.

This is the job I’d hand an AI agent — the reasoner we’re missing, run across each change and everything it touches. My hopes were high; so far the agents lean the other way, reaching for plausible tests sooner than sound reasoning — ten tests for every feature, a pile that proves nothing and grows faster than anyone will maintain it. So that’s a bet on where the tooling should head, not where it is.

Summary

An invariant is just a fact we promise stays true. Stating it — before the loop, across each iteration, on each branch — converts a guess about correctness into something we can check. The goal is code written correct, not code that looks about right with the bugs ironed out later; we need all the help we can get — tests included — and invariants are the harder, stronger tool we keep leaving on the table. We don’t need formal methods to get the benefit; for anything non-trivial we find the invariant and confirm it holds — as an assert, or a comment, whatever the team prefers — on top of the simple control flow that makes it true. We have all been doing this for years without the name: a working system does not get built without reasoning about it, and there is no reasoning without some fact held fixed. Now that fact has a name and a job — the only change is to use it on purpose.

The functional view

An addendum for the curious. The invariants above stand on their own; this is the foundation they rest on.

Mathematical assertions are always general in the sense that they are applicable to many —often even infinitely many— cases […] Besides general, mathematical assertions are very precise. […] A tradition of more than twenty centuries has taught us to present these general and precise assertions with a convincing power that has no equal in any other intellectual discipline.

— Edsger W. Dijkstra, On the Interplay Between Mathematics and Programming (EWD641)

That is the case for reasoning over sampling. An invariant is a mathematical assertion about a program — general, precise, and only as convincing as the argument behind it. The footing for that kind of assertion is functional programming (FP) — seeing code as values produced, not state mutated, something I poked at in JavaScript years ago. Its pure functions are the core: a function whose output is defined solely by its inputs and that has no detectable (in context) side effects — it doesn’t update globals, doesn’t mutate its inputs, and so on. FP sees a program as a composition of functions, so we can reason about its correctness recursively.

Purity buys properties worth naming. An unused result can be dropped: a call whose value the logic never needs is safe to remove. That is what licenses the condition simplifications from reshaping conditions — and leaning on short-circuit evaluation to skip a call: the language guarantees the skip; purity guarantees the skip changes nothing. A call with side effects cannot be quietly dropped, even when its value goes unused. And independent calls may run in any order, even in parallel. Each property is itself an invariant about the call — nothing it touches changes underneath us. Purity pays off for the other tool, too: with no hidden inputs, a pure function is as testable as code gets — a test exercises the behavior itself, not behavior tangled with its environment. Still sampling, not proof, but a clean sample with nothing to mock away.

In reality we deal with impure constructs: statements that mutate variables, and interactions with all sorts of external state (files, streams, databases, APIs). How can FP help?

A pure function can still have local variables that are mutated internally, as long as they are not reused between invocations. For example, wrap the sum loop we opened with in a function and it is pure, yet it mutates its internal sum and loop index i.

This is the link back to invariants: even ordinary mutation has a pure reading — treat each assignment as creating a new value that happens to reuse the name (compilers do exactly this and call it SSA ), and nothing mutates under us. Shared and external state resists the renaming — a file, a socket, a variable another closure also writes — but local, linear mutation reads cleanly. So at every point some fact about those values is true, and stays true. That fact is the invariant — a name for what holds at a given line. When changes are localized like this, invariants are what we use to argue correctness.

Coding tactics posts

The series so far, in order:

• Code linearization — flatten the control flow.
• Logical optimizations — reshape the conditions.
• Boolean algebra — the algebra underneath them.
• TDD as religion — why a green suite is not a proof.
• Loop and if invariants — this post.

More installments are on the way: structured jumps, two exotic uses of goto, and what “premature” optimization really costs.