Enforce Code Correctness with Formal Invariants

invariant-guard forces a correctness-first discipline: write the function contract, loop invariant, termination argument, and edge cases before writing code, then verify the code maintains what was stated. Its premise is that the model already knows what a loop invariant is, that recursion needs a base case, and about empty lists and integer overflow, but ships subtle correctness bugs because it never writes these down before coding. "I know this algorithm" is called out as the exact rationalization that ships off-by-one and missing-postcondition bugs.

Its Iron Law is: no loop or recursion without a written invariant and termination argument. Five non-negotiable rules follow: every loop gets a one-line invariant stating what is true at the top of every iteration; every loop gets a one-line termination argument naming the quantity that strictly decreases or increases toward a bound; every recursion gets an explicit base case and a measure that strictly decreases each call; edge cases (empty input, singleton, all-equal, sorted/reversed, duplicates, boundary and overflow values, NaN and infinities, off-by-one indices, concurrent modification) are listed before writing, with expected behavior for each; and illegal states should be made unreachable through types (sum types, newtypes, non-empty list types, parse-don't-validate) rather than merely unhandled.

The pre-write protocol requires, in order, before non-trivial code: the function contract, one loop invariant per loop, one termination argument per loop or recursion, base cases and measure for recursion, an edge-case table, the types or asserts making illegal states unrepresentable, the code itself, and a self-check per loop. If any of the first six is missing, no code should be emitted.

Its worked trap is Boyer-Moore majority vote: a naive single-pass implementation returns a candidate even when no majority exists, failing on [1,2,3] and [2,2,1,1]. Writing the postcondition first ("returns x iff count(x) > n/2, else null") and the loop invariant second ("if a majority exists, it equals candidate at exit") exposes that the invariant is strictly weaker than the postcondition, meaning a second verification pass is required. The same pattern of "postcondition stronger than the natural loop invariant" recurs in Floyd's cycle detection (finding the meeting point, not the cycle start), find-any versus find-leftmost binary search, QuickSelect's partition postcondition, and DP table reconstruction.

Its canonical binary-search example shows the same trap: a naive implementation returns any match rather than the leftmost one:

function leftmost(a: number[], target: number): number {
  let lo = 0, hi = a.length - 1;
  while (lo <= hi) {
    const mid = (lo + hi) >> 1;
    if (a[mid] === target) return mid;       // returns ANY occurrence
    if (a[mid] < target) lo = mid + 1; else hi = mid - 1;
  }
  return -1;
}
// leftmost([1,2,2,2,3], 2) → may return 2, not 1

The skill supplies a table of canonical invariant and termination patterns for linear scans, two-pointer search, binary search, sliding window, BFS, DFS, divide and conquer, greedy with a priority queue, union-find, and in-place partitioning, plus an edge-case table by input shape (array, string, integer, float, map, tree/graph, stream, time/date, concurrent). Output discipline requires an // inv: comment per loop, a base-case-and-measure comment per recursion, handling or explicit delegation of every listed edge case, precondition assertions at entry, and preferring types over runtime checks. It names six rationalizations to watch for ("I traced it in my head", "tests will catch it", "the postcondition is implied", and similar) and a verification checklist to run before claiming correctness.

Use it when writing or reviewing algorithms where the obvious implementation is subtly wrong: postconditions stronger than the natural loop invariant, in-place mutation with read and write pointers, recursion with multiple parameters or accumulator state, off-by-one suspects with duplicates or boundary values, or iterative refinements that must terminate. It pairs with lemmaly, which should pick the algorithm first, and is loaded after the algorithm is chosen but before the loop body is written; for mathematical or probabilistic techniques it hands off to mathguard, and for concurrent code its invariants assume single-threaded execution unless explicitly extended.

It is explicitly not an automated prover: it requires the author to write invariants, it does not mechanically check them, and for trivial one-liners that obviously cannot fail, the protocol is unnecessary overhead.

Inputs are the algorithm or function to write or review, particularly ones involving loops, recursion, or in-place mutation. Outputs are the written contract, invariants, termination arguments, edge-case table, and type-level guards produced before the code, followed by the code itself annotated with // inv: comments and a closing self-check.

It is for developers and AI coding assistants writing or reviewing non-trivial algorithms, especially ones with a well-known "obvious" implementation that is subtly wrong.