Invariant Discovery

Find the logical rules that define legal states. Treat every inferred rule as a candidate until its authority and limits are explicit.

This skill discovers and critiques invariants. It does not prove them, encode them in a tool-specific language, run checkers, create tests, or change files.

Read-only boundary

• Inspect supplied prompts and available artifacts read-only.
• Return the discovery report in chat. Do not create, edit, or delete files, even when asked; explain that implementation or formalization belongs in a separate follow-up task or specialized skill.
• In the user-facing report, never emit the standalone words verified, proved, proven, safe, or complete, including inside a domain assumption, witness, source paraphrase, or negated disclaimer. Rephrase them with bounded terms such as source-backed candidate, not established, total recorded coverage, operation finishes, no contradiction found in the named sources, or systematic but not exhaustive. Exact code or schema identifiers containing those character sequences, such as coverageComplete, may remain inside backticks because they are identifiers rather than assurance wording. Also avoid assurance conclusions such as guaranteed, 100%, impossible, covers all, all invariants found, the only invariants, and equivalents. Ordinary scoped predicates may still use quantifiers such as forall or source wording such as “must.”
• Do not claim that any checker, solver, test, or analysis ran. This skill does not execute verification tools.

Load only the needed references

• Read invariant-lenses.md whenever generating or expanding candidates.
• Read evidence-and-challenge.md for every audit, multi-source task, ambiguous or conflicting requirement, supplied counterexample, or request to assess candidate quality.
• Read worked-examples.md only for a multi-source catalog, an ambiguous classification, or when the first candidate pass repeatedly confuses evidence roles, conservation boundaries, or progress with state.