invariant-ace_skill

Overview

This skill turns "should never happen" into "cannot happen" by defining owned, inductive invariants and enforcing them at strong, cheap boundaries. It focuses on picking a single owner, proving inductiveness with a concrete counterexample trace, and encoding enforcement at parse/construct/API/DB/lock/txn boundaries with a verification signal.

How this skill works

Inspect where truth is owned, enumerate all transitions (including retries and concurrent schedules), and produce a minimal counterexample that demonstrates the failure. Select 1–2 checkable predicates, assign a single owner and scope, choose the strongest affordable enforcement layer, and add a verification harness (property/stateful/stress) tied to the predicate.

When to use it

• When "should never happen" branches appear in logs or error trackers.
• When validation is scattered or derived facts (cache/index) drift.
• When idempotency, versioning, retries, duplicates, or out-of-order events are causing bugs.
• When races, linearization, or protocol correctness are unclear.
• When loop or algorithm correctness depends on intuition rather than assertions.

Best practices

• Name the owner and scope before designing invariants; if owner is unclear, pause for discovery.
• Keep invariants inductive: ensure true initially and preserved by every transition (including retries).
• Enforce at the strongest cheap boundary (parse/constructor/opaque type or txn/lock), avoid scattered runtime checks.
• Prefer narrow, opaque types and smart constructors so core code sees only validated state.
• Add a single verification signal per predicate (property tests, stateful tests, concurrency stress).

Example use cases

• Normalize and validate incoming JSON at parse time so core functions receive ValidatedValue only.
• Add idempotency key table + atomic apply in a txn to prevent duplicate side effects from retries.
• Introduce a monotonic version field and reject stale writes at commit to preserve non-decreasing invariants.
• Assert loop invariants inside complex algorithms and add differential tests against a reference implementation.
• Centralize denormalized column writes under a single owner and enforce via DB constraint + transaction.