Enforce Code Correctness with Formal Invariants

A correctness discipline skill for algorithmic code: before writing any loop or recursion, state the invariant, termination argument, and edge cases, then verify the code maintains them. Its "Iron Law":

NO LOOP OR RECURSION WITHOUT A WRITTEN INVARIANT AND TERMINATION ARGUMENT

is enforced through a mandatory pre-write protocol: a function contract (pre/postconditions), one loop invariant per loop, one termination argument per loop or recursion, a base case and measure for recursion, an edge-case table, and a note on which illegal states were made unrepresentable via types - all before the code itself, followed by a self-check confirming each loop's invariant holds at top, is preserved by the body, and implies the postcondition at exit. It works through two fully worked traps - Boyer-Moore majority vote and leftmost-match binary search - showing a naive implementation that passes casual testing but fails on specific inputs because the loop's natural invariant is strictly weaker than the required postcondition, then the corrected version with an added verification pass. It supplies a reference table of canonical invariant/termination pairs for ten loop and algorithm shapes (linear scan, two-pointer, binary search, sliding window, BFS, DFS, divide and conquer, greedy with priority queue, union-find, in-place partition), an edge-case checklist across nine input shapes (array, string, integer, float, map, tree/graph, stream, time/date, concurrent), and a table of six common rationalizations for skipping the protocol paired with why each one is wrong.

Use it when writing or reviewing algorithms where the obvious implementation is subtly wrong: a postcondition stronger than the loop's natural invariant, in-place mutation with read/write pointers, recursion with multiple parameters or accumulator state, off-by-one-prone code with duplicates or boundary values, or iterative refinements that must terminate (fixed-point, Newton, EM). Load it after the algorithm has already been chosen, not before - if the algorithm choice itself is unclear, use lemmaly first; if the technique is mathematical (probabilistic, FFT, geometry), escalate to mathguard instead, since its invariants use epsilon-bounds rather than equality; and if three or more optimization attempts have already failed tests, the skill's own guidance is to escalate to complexity-cuts rather than keep patching.

Input is a request to write or review non-trivial code containing loops, recursion, or in-place state mutation. Output, before any code, is a function contract, per-loop invariants, termination arguments, recursion base cases and measures, an edge-case table, and a note on illegal-state encoding - followed by code containing // inv: comments per loop and base-case/measure comments per recursion, plus a closing self-check that each invariant holds at entry, is preserved, and implies the postcondition at exit.

Pairs with two sibling skills named in the source: lemmaly (algorithm selection, loaded before invariant-guard) and mathguard (approximate or randomized algorithms with epsilon-bounded postconditions); escalates to complexity-cuts when repeated optimization attempts fail tests without a missing-contract diagnosis.

Engineers and coding agents writing or reviewing algorithmic code - anyone about to implement a loop, recursion, or in-place mutation who needs a forcing function against shipping example-correct but behavior-wrong code.