Turn 'should never happen' into 'cannot happen' by defining owned inductive invariants and enforcing them at parse/construct/API/DB/lock/txn boundaries with a verification signal. Use when prompts mention invariants, impossible states, validation sprawl, cache/index drift, idempotency/versioning, retries/duplicates/out-of-order events, race/linearization bugs, loop correctness, or hardening another implementation workflow with invariant checks first.
Turn "should never happen" into "cannot happen" with minimal, high-leverage changes: pick owned, inductive invariants; enforce them at the strongest cheap boundary; prove via a concrete counterexample trace and a verification signal.
Use When (Signals)
Null/shape surprises, runtime validation sprawl, or input decoding scattered across the codebase.
Boundary refinement: raw -> parsed -> validated; only validated enters core.
Canonicalization: normalize early (case/whitespace/timezone/ID format) so equality and caching are stable.
Explicit absence: model optionality explicitly; avoid "sometimes null" in the core.
Cross-field coupling: combine coupled fields into one value to prevent illegal combinations.
Denormalization discipline: if you store derived facts, centralize writes or make them recomputed.
Concurrency & Protocol Correctness
Lock/txn invariants: P holds under lock or at commit; define where the linearization point is.
Monotonic metadata: versions/epochs/counters only increase; reject stale writes.
Idempotency: retries and duplicates are safe (idempotency keys, dedupe tables, "apply once").
Explicit state machines: enumerate states + allowed transitions; persist enough metadata to reject out-of-order events.
Coordination decisions: if P depends on global uniqueness or non-negativity under concurrent debits, choose coordination or redesign (partition/escrow).
Algorithms & Loop-Heavy Code
Loop invariants: assert what is preserved each iteration (partitioned regions, sorted prefix, conservation laws).
Variant/termination: name a decreasing measure; if you cannot, expect non-termination edges.
Representation invariants: hide internal structure behind an API; add a rep-check for tests/debug.
Differential testing: compare to a simple, slow reference implementation to catch corner cases.
Before/After Sketches (Language-Agnostic)
Boundary Refinement (Data)
Before: functions accept RawInput and validate ad hoc
After: parseRaw(...) -> ValidatedValue | Error
core functions accept ValidatedValue only
Idempotency + Versioning (Concurrency/Protocol)
Before: handle(event) mutates state directly (retries duplicate side effects)
After: if seen(event.id) return
if event.version <= state.version return (or reject)
apply(event) at a single atomic boundary (lock/txn/CAS)
Loop Invariant (Algorithm)
Before: comment says "array left side is partitioned"
After: assert(invariant(state)) inside loop
test: random arrays, shrink failing cases, compare to reference
Verification
Pick at least one signal and tie it to a specific invariant predicate.