prove-invariant
Skill2 starsChanged 47 days agoMITView on GitHub
Derives a property the output must satisfy by necessity (symmetry, invariance, counting, an algebraic identity), gates the output on it, and mutation-tests the gate. Use when adding or reviewing tests for correctness-critical output, when a suite passes but the values may still be wrong, or when stored expectations (golden files, snapshots, asserted labels) are the only oracle. Triggers on 'all tests pass but', 'is this actually correct', regression suites for scientific or algorithmic output, and before trusting any newly written test. Not for changing an existing expected value (use change-asserted-value) or checking that a test can fail at all (use test-gate).
In this repository22 other files it gives its agents.
- bounded-goalsSkill
- change-asserted-valueSkill
- check-targetSkill
- cluster-failuresSkill
- councilSkill
- enumerate-firstSkill
- eval-loopSkill
- fable-reviewSkill
- gauntlet-loopSkill
- handoffSkill
- kickoffSkill
- promo-videoSkill
- refusal-censusSkill
- reuse-before-rerunSkill
- run-evalSkill
- run-gateSkill
- scientific-posterSkill
- spy-siteSkill
- test-gateSkill
- understand-before-mergeSkill
- verify-sourceSkill
- watching-background-jobsSkill
The file
We split this skill into the rules it gives an agent
2 rules. About 0 are common, 2 are distinctive, and 0 are very specific to this project.
≈0
Common · estimate
Many files like this have a rule of this kind.
≈2
Distinctive · estimate
This author's own choices. Worth a look.
0
Very specific
Tied to their project's names, files or tools. Probably skip.
- Common
- Distinctive
- Very specific
- Distinctive: line 31
Look for a transformation the answer must respect:
- Distinctive: line 61
Write both facts down. A gate whose limits are undocumented will be over-trusted by the next person, including you.
≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.
Files
prove-invariant
The rule
Find a property that must hold by necessity, independent of the implementation. Then gate on it, and mutation-test the gate.
Stored expectations only tell you the output has not changed. They cannot tell you it was ever right — and once committed, a wrong value looks exactly like the specification.
Why this exists
A stereo-descriptor suite was fully green, and had been for years. Adding one
property — reflection pairs mirror images, so across all permutations of a
constitution each index must carry as many -C labels as -A labels — exposed
five wrong values immediately. It needed no shuffling and ran in under a second,
where a 35,888-case sweep costing twelve seconds could not see them at all.
Separately, a naming system round-trips 100% of 1.1M outputs while emitting zero correct descriptors of the required class. Self-consistency is not correctness.
Where invariants come from
Look for a transformation the answer must respect:
| Source | Question to ask | Example |
| Symmetry | What operation maps the object to itself, or to a partner? | Reflection pairs enantiomers → label counts must balance |
| Invariance | What can I change that must not change the answer? | Input order, units, encoding, traversal order |
| Counting | Does a census match a known total? | Number of stereoisomers for a constitution |
| Round-trip | Does encode→decode return the original? | Weak on its own — see below |
| Algebraic | Is there an identity the output must satisfy? | Conservation, idempotence, monotonicity |
| Internal consistency | Must two outputs agree by construction? | Two encodings of the same structure must get the same label |
Procedure
- State the property in one sentence, as a necessity — "reflection is an involution on the permutation indices, so counts must balance."
- Implement it as a gate over a broad sample, not a handful of cases.
- Mutation-test it. On a scratch copy (see
test-gate), inject a violation or revert the fix, and confirm the gate fails. If it passes, the gate is blind to that bug: tighten it and repeat. A gate you have not seen fail is a gate you have not tested. - State necessary vs sufficient, out loud, in the test's own docs. Say what it cannot catch.
Necessary is not sufficient
Mirror balance proves the labels are self-consistent; a systematic swap of the two symbols would still balance. So a passing property narrows the space of possible bugs — it does not empty it. Pair every necessary-condition gate with at least one external oracle (a worked example from the specification) that pins the convention itself.
Write both facts down. A gate whose limits are undocumented will be over-trusted by the next person, including you.
Red flags
| Thought | Reality |
| "The whole suite is green" | Green against what it was told to expect. |
| "These values came from the reference implementation" | Then they encode its bugs too. |
| "Round-trip passes" | Round-trip cannot see class errors. |
| "I can't think of a property" | Try the symmetry row first — it is the most productive. |
| "The property passed, so we're correct" | Necessary, not sufficient. Say which. |
Does it work?
Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.
No reviews yet
People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.
- It worked
- Partly
- It didn't
Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.
Your trail
Files you open will collect here, so you can find them again.
Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.
Now do this for your own.
Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.