Invariant Ace

Mission

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.

• Redundant stored facts drift (cache/index/denormalized columns) or "fix-up" code runs often.

• Flags/states explode; impossible combinations appear; "unreachable" is reachable.

• Races, duplicate/out-of-order events, retries, partial failures, or "exactly once" assumptions.

• Idempotency keys, monotonic version/epoch checks, stale writes, or linearization questions are central.

• Loop/algorithm correctness depends on comments or intuition; tricky indexing/arithmetic/termination.

• "Should never happen" branches show up in logs or error trackers.

Routing Priority

• If a task has invariant/protocol cues and also asks for broad implementation ($tk , $fix , $work ), run this skill first to lock invariants, then execute edits.

• If you cannot name state owner + transitions, switch to clarification/discovery before implementation.

Core Model (Fast Definitions)

• Invariant: predicate P(state) intended to hold for all reachable states in a scope.

• Inductive: true initially AND preserved by every allowed transition in that scope.

• Owner: the single module/type/transaction/lock/actor that controls all mutations needed to preserve P.

• Precondition/postcondition: caller obligation vs operation guarantee; do not mislabel these as invariants.

• Derived property: recomputable fact; avoid storing it as "must match" unless you centralize updates.

• Safety vs liveness: invariants are safety ("nothing bad"); keep progress ("eventually") separate.

Immediate Scan

• State owner: where does the truth live (type/module/service/table)?

• State boundary: where does raw data enter (API/DB/file/queue)?

• Allowed transitions: list operations/events that mutate the state (including retries and concurrency).

• Failure today: one concrete trace (inputs + transitions + schedule) that reaches a bad state.

• Protection level: hope -> runtime -> construction-time -> type/compile-time -> persistence/protocol/atomicity.

• Pain tag(s): data | concurrency/protocol | algorithm/loop (often multiple).

Protection Ladder

Choose the cheapest strong layer that makes the violation hard or impossible.

• Hope-based: comments, assumptions, "unreachable".

• Runtime: scattered guards/validators near use sites.

• Construction-time: parse/validate once at boundaries; core code only handles refined values.

• Type/compile-time: illegal states are unrepresentable (ADTs, typestates, opaque wrappers).

• Persistence: schema/constraints/transactions enforce invariants at rest.

• Concurrency boundary: locks/actors/CAS/txns define where invariants must hold (under lock, at commit, at linearization).

Protocol (Counterexample-Driven)

Declare scope + owner.

• Write "P holds when/where": always | after construction | under lock | at txn commit | after message apply.

• If you cannot name an owner, the invariant will drift; pick a choke point first.

List transitions and try to break P.

• For each transition (and retry/out-of-order variants), attempt a counterexample trace.

• If P fails, decide: bug vs wrong scope vs missing state vs wrong owner.

Make P inductive (or downgrade it).

• Weaken P, move it to pre/postconditions, or add auxiliary state (version/epoch/status/idempotency key) until it closes under transitions.

Run a coordination check (concurrency/distributed).

• Ask: can two individually-valid concurrent transitions merge into a P-violating state?

• If yes, you need coordination (lock/txn/consensus) OR you must redesign the invariant/operation (partition, escrow, monotone merges, idempotency).

Encode enforcement at the strongest cheap boundary.

• Prefer: parser/decoder + smart constructors + narrow/opaque types + centralized mutation.

• Avoid: N scattered validators, duplicated truths without a single writer, and "fix-up" routines on every read.

Add observability if full enforcement must be staged.

• Add cheap tripwires (assert/log/metric) and quarantine paths (reject/dead-letter/compensate).

• Record replayable context (transition name, IDs, versions), not raw secrets.

Verify with the right harness.

• Data: fuzz/property tests on parsers/constructors.

• State machines: stateful/model-based tests (sequences).

• Concurrency: stress + schedule perturbation; assert at quiescent points.

• Protocols: small model checking/simulation for drops/dupes/reorder.

• Algorithms: invariant assertions in loops + differential tests vs reference.

Compact Mode (Fast Path)

Use this when the task is small or time-boxed.

• Counterexample: one concrete failing trace (<=5 transitions).

• Invariants: 1-2 predicates with explicit owner + scope.

• Enforcement Boundary: one chosen choke point (parse/construct/API/DB/lock/txn).

• Verification: one signal tied to one predicate.

Escalate to full protocol if any of the above is ambiguous or non-inductive.

Invariant Record (Use This Format)

• Predicate: P(state) (precise, checkable)

• Owner: module/type/service/table/lock/txn

• Holds: always | after construction | under lock | at commit | after apply

• Maintained by: transitions that must preserve P

• Enforced at: parse/construct/API/DB/lock/txn/protocol

• Counterexample to avoid: minimal trace that breaks it today

• Verification: property/stateful/stress/model/differential

Patterns by Pain

Data Modeling & Input Validity

• 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.

• Property/fuzz: parsers, constructors, normalization.

• Stateful/model-based: sequences over operations; check invariants after each step.

• Concurrency stress: N threads + jitter; assert invariants at quiescent points.

• Protocol simulation: reorder/duplicate/drop + crash/restart; assert safety invariants.

• Model checking (optional): small state + exhaustive exploration for protocols.

• Differential/reference: algorithm output equals reference for randomized inputs.

• Runtime tripwires: assertions/logging/metrics for staged rollout.

Research Anchors (Mental Models, Not Requirements)

• Hoare/Floyd/Dijkstra: invariants as proof objects; weakest preconditions.

• ADT/rep invariants (Liskov-style): abstraction function + local reasoning.

• Abstract interpretation: over-approx reachable states; inferred invariants.

• Dynamic invariant mining (Daikon-style): candidate generation; falsify with counterexamples.

• Separation logic / framing: invariants tied to ownership; interference-aware reasoning.

• Rely-guarantee & linearizability: concurrency invariants under schedules.

• TLA+/Alloy mindset: protocols as transitions + invariants; counterexample traces.

• Coordination avoidance / CRDT laws: when invariants require coordination vs merge-safe design.

Output Contract (Required Headings)

Use these exact headings in the final response for this skill:

• Counterexample

• Invariants

• Owner and Scope

• Enforcement Boundary

• Seam (Before -> After)

• Verification

• Observability (optional)

Deliverable Checklist

• Counterexample: minimal breaking trace (include schedule/retry if relevant).

• Invariants: 1-5 predicates with owner + scope ("holds when").

• Enforcement Boundary: boundary/type/API/DB/lock/txn/protocol choice + why.

• Seam (Before -> After): minimal structural change that makes violations hard.

• Verification: property/stateful/stress/model/differential tied to at least one predicate.

• Observability (optional): tripwires/quarantine/metrics if rollout must be staged.

Cross-Coordination

• If broader failures emerge, lean on the Unsoundness checklist.

• If stronger invariants dent ergonomics, reference the Footgun guardrails.

Measurement (seq)

Track adoption and compliance with seq :

seq skill-trend --root ~/.codex/sessions --skill invariant-ace --bucket week seq skill-report --root ~/.codex/sessions --skill invariant-ace
--sections "Counterexample,Invariants,Owner and Scope,Enforcement Boundary,Seam (Before -> After),Verification,Observability (optional)"
--sample-missing 5