Enforce Code Correctness with Formal Invariants

invariant-guard fixes a specific failure mode: models know what a loop invariant is, know recursion needs a base case, know about empty lists and integer overflow - they just don't write these down before producing code, so they ship subtle correctness bugs that tests don't catch. The skill's iron law is that no loop or recursion gets written without a stated invariant and termination argument first; if the invariant can't be written in one sentence, the loop hasn't actually been designed yet.

Five non-negotiable rules apply to any non-trivial code: every loop gets a one-line invariant (what's true at the top of every iteration); every loop gets a one-line termination argument (the quantity that strictly decreases or increases toward a bound each iteration); every recursion gets an explicit base case, a strictly-decreasing non-negative measure, and a combination rule for how recursive results merge; every function gets its edge cases listed before writing code, not after (empty input, singleton, all-equal elements, sorted/reverse-sorted, duplicates, negative/zero/boundary values, integer overflow, NaN/Infinity/-0, off-by-one boundaries, concurrent modification); and illegal states should be made structurally unreachable rather than merely unhandled, preferring sum types over boolean-flag soup, newtypes for IDs that must not be swapped, non-empty list types, and parse-don't-validate at the boundary.

Before producing non-trivial code, the required message structure is, in order: the function contract (pre/postconditions, return value); loop invariants (one per loop); termination arguments (one per loop or recursion); base cases and measure (for recursion); an edge case table with expected behavior per applicable case; the types/asserts that make illegal states unrepresentable; the code itself; and a self-check per loop confirming the invariant holds at top, is preserved by the body, and its exit implies the postcondition. If any piece before the code is missing, no code should be emitted.

The canonical worked trap is Boyer-Moore majority vote: a naive single-pass implementation returns the voting candidate even when no majority exists, failing on inputs like [1,2,3]. Writing the function contract first ("returns x iff count(x) > n/2, else null") and the loop invariant separately ("if a majority exists, it equals candidate when the loop exits") exposes that these two statements are not equivalent - the loop guarantees only a conditional, not the postcondition itself, so a second verification pass is required. The same shape of trap - a natural loop invariant that's strictly weaker than the actual postcondition - recurs in Floyd's cycle detection (finding the meeting point doesn't tell you where the cycle starts), "find any match" vs. "find leftmost match" binary search (an early return abandons the search before reaching the true leftmost index), QuickSelect partition (an off-by-one in the partition invariant silently breaks the k-th-smallest guarantee), and DP with path reconstruction (the value table doesn't automatically give you the optimal path without separate invariants on the choice array). The general rule: write the postcondition first, the loop invariant second, and check the second implies the first - if not, a pass, check, or auxiliary state is missing.

A reference table maps common loop/algorithm shapes to their canonical invariant and termination argument - linear scan, two-pointer, binary search, sliding window, BFS, DFS/tree recursion, divide-and-conquer, greedy with a priority queue, union-find, and in-place partition - plus a default edge-case checklist organized by input type (array/list, string, integer, float, map/dict, tree/graph, stream/iterator, time/date, concurrent). Output discipline requires an // inv: comment per loop, a base-case/measure comment per recursion, explicit handling or delegation for every listed edge case, precondition assertions at function entry where cheap, and types preferred over runtime checks. It escalates to companion skills when appropriate: lemmaly if the algorithm itself hasn't been chosen yet, mathguard for probabilistic/FFT/geometric techniques needing epsilon-bounded postconditions, and explicit "single-threaded only" framing (or escalation) for concurrent code. A rationalizations table calls out exactly the excuses that ship these bugs ("I know this algorithm," "I traced it in my head," "tests will catch it," "the postcondition is implied"), a red-flags list names the moments to stop and write the invariant first, and a verification checklist gates any claim of correctness on every rule above actually being satisfied.

Use this skill when writing or reviewing algorithms where the obvious implementation is subtly wrong - postconditions stronger than the loop's natural invariant (Boyer-Moore, Floyd's cycle detection, leftmost binary search, QuickSelect), in-place mutation with read/write pointers, recursion with multiple parameters or accumulator state, off-by-one suspects with duplicates or boundary values, or iterative refinements that must terminate (fixed-point, Newton, EM). It pairs with lemmaly (algorithm selection) and mathguard (approximate/randomized math), loaded after the algorithm is chosen and before the loop body is written. It is not an automated prover - invariants must be authored, not mechanically checked, and should pair with property-based tests for stronger evidence; concurrency reasoning is out of scope by default; float/overflow specifics are language-dependent; and it deliberately adds overhead, so it's reserved for non-trivial loops, recursion, and in-place mutation rather than trivially-correct one-liners.

Developers and coding agents writing or reviewing algorithmic code with loops, recursion, or in-place mutation, who want a discipline that catches postcondition gaps and off-by-one bugs before they ship, not after tests (which only catch the examples someone thought of) fail to catch them.