invariant

A condition that is required to be true at all times while a system runs.

An invariant is a promise the code makes to itself — for example, 'this routine never allocates memory' or 'this counter is never negative.' Because it must always hold, checking it is a powerful way to catch bugs: any violation means something is fundamentally broken. In microZeus, the reaper's no-allocation invariant held at zero violations across a run with a real model.