[rayslava]

• Ship an agent skill for #[spec] under plugins/anodized, packaged as a plugin for both Claude Code and Codex from one directory. Installs with claude plugin marketplace add anodized-rs/anodized, with no publishing step.
• Lead the skill with what other contract systems get wrong here: there is no old(), no implicit output binding, conditions cannot mutate, and 0.6 broke from 0.5. A model that knows this crate at all is likely to know the pre-0.6 syntax.
• Generate the clause, qualifier, item-kind, and cfg tables from anodized-core, so they cannot drift from the parser. The keyword classification matches Keyword without a wildcard arm, so a new clause breaks the build until it is documented.
• Compile every Rust example in the skill, and in REFERENCE.md, which is not doctested and had drifted: a bare ensures cannot see the return value, and *output no longer type-checks.
• Repair those examples, and replace two comparisons that the type already guaranteed.
• Add CLAUDE.md, symlinked as AGENTS.md the way README.md already is, and a CI job that lints and tests the new skill-tools crate.
• Depends on [anodized-core] fix: honor a condition's cfg without printing #192: the skill documents #[cfg] on a condition, which only behaves as described once that is merged.

[mkovaxx]

Might be worth adding some precision here. It is logically sound to make a precondition stronger or a postcondition weaker, but not the other way around.

[rayslava]

Good catch — "relax" was doing too much work, and the precision it needs turned out to be more than one direction.

Strengthen-pre / weaken-post are the edits that keep the triple true without re-examining the body, but that only settles a postcondition failure. A precondition failure does not make the spec false of the code, since preconditions are obligations on callers, so when the clause is simply too strong (requires: x > 0 where the body handles x >= 0) weakening it is the correct repair — which is what the triage bullet above already implied by "fix the precondition if it was wrong". The guidance is now split by which check fired, and weakening is flagged as a new claim about the body that has to be verified rather than assumed.

Two wrinkles that defeat applying any of this from the message alone, both now in the text. maintains is checked on entry and again on exit and reports as precondition failed one way and postcondition failed the other, so a precondition failed may be naming an invariant — and weakening that relaxes the exit guarantee too, so it is not the safe edit. And only anodized_print puts the failing expression in the message; under anodized_panic alone you get the bare text with a location pointing at the attribute, which identifies the function but not the clause.

Also worth recording, since it cuts against the intuition that the sound directions are the safe ones: weakening a genuine precondition is the only one of these edits that cannot break an existing caller. Same wording in the workflow section of SKILL.md, plus a note in the trait section that narrowing runs the other way because an impl is a special case.

[mkovaxx]

We can refine the error messages to report pre-invariant failed and post-invariant failed. Do you think that would help?

[mkovaxx]

Also worth recording, since it cuts against the intuition that the sound directions are the safe ones: weakening a genuine precondition is the only one of these edits that cannot break an existing caller.

I think there are two different concerns getting mixed up here. There are three "entities" at play: a call site, a function's spec, and the function's body. The general insight is that any change is allowed to touch only one of those three, and must assume that the other two are correct. Without that constraint, changes can collapse correct code into nonsense. I suspect the deeper difficulty is figuring out which one of the three to change based on context.

[mkovaxx]

@rayslava Pre/postinvariant terminology in errors was added back! #197

[rayslava]

Nice, thanks — dropped my own version of this and rebased onto yours. Skill docs now use preinvariant/postinvariant, and note that the group panic still reports neither, so you need both flags to see which clause it was.

[rayslava]

Good point, that's a much better way to frame it — rewrote the guidance around it, and diagnostics.md now lists what usually tells you which of the three it is. One tweak: edits can still cascade, since tightening a requires means fixing the callers that relied on the loose one.

[mkovaxx]

Consider adding: In most situations, adding an empty #[spec] is still preferable because it explicitly states that the spec is tautological (i.e. equivalent to requires: true and ensures: true).

[rayslava]

Added, to both spec.md and the decision rules in SKILL.md: a bare #[spec] records that the contract is deliberately tautological, which is not the same as nobody having considered it. It is also not purely decorative — it is what enables loop specs inside the body.

Two caveats came out of checking it, and I would rather state them than have the advice bite someone.

Some functions cannot carry a spec at all, because the macro evaluates the body inside a closure: -> impl Trait (E0562), const fn (E0015), and returning &mut borrowed from a parameter (captured variable cannot escape FnMut closure body, which carries no error code at all). Returning a shared & is fine, including a reborrow from a &mut parameter — I checked, since it is the natural thing to assume breaks too. I have written this as the closure rule plus known instances rather than a closed list, since successive passes kept turning up more of them.

And on a function nested in a trait or an impl, an empty spec is #[spec()] rather than #[spec]: a nested attribute is read with parse_args, so the parentheses are needed even when empty. That applies to traits and trait impls as well as inherent impls. Omitting the attribute there is equally valid and means the same empty spec.

All three compile failures are documented among the indirect errors with compile_fail examples that the suite compiles and checks.

[rayslava]

Also picked up #196 — skill now says a move pattern is reconstructed rather than telling people to reach for |ref output|, and documents the no-mixing and .. rules. The refutable-pattern case moved from E0507 to E0005 too.

[MauScheff]

This is a very good idea, I'm using codex and I would love to just point it to anodized and having it just work. Any progress on this / ETA? Thanks :) @rayslava

[MauScheff]

I think the main thing I'd simplify here is SKILL.md.

From what I see, this is the main entry point agents will read, and at ~350 lines I think it's overly long. Ideally, these files should work more like indexes that explain what the skill does and point to the relevant reference files depending on what the agent needs.

An agent might just want to understand what the skill is about, and we don't want to load all that extra context if it's not necessary. So I think we could make SKILL.md much shorter, maybe under 100 lines.

There's also quite a bit of duplication between SKILL.md and reference.md. Things like clause grammar, captures, qualifiers, and other implementation details are explained in both places. I think most of that could just live in reference.md, with SKILL.md pointing to it when needed.

I also feel there's some overfitting to specific use cases. For example, the "Four things that are not what you expect" section and the detailed version migration instructions seem like things that belong in migration.md or reference.md, rather than the main skill. I generally prefer keeping prompts as generic as possible to avoid unnecessarily biasing the model toward particular scenarios.

There are definitely some important instructions that should stay in SKILL.md, especially things the agent needs to know before doing anything else. But I'd try to keep those to a minimum and let the agent read the relevant files as needed.

So basically, I'd suggest:

• Make SKILL.md much shorter, ideally under 100 lines.
• Keep it focused on what the skill does, the essential instructions, and which files to read for different tasks.
• Move most of the detailed technical explanations into reference.md, migration.md, etc.
• Avoid repeating the same information across files.
• Keep the prompts more general unless there's a specific reason to be prescriptive.

Overall, I think there's just too much text and we could probably achieve the same result with a much simpler structure. I like the idea of having the documentation and examples validated against the actual code, but I think we can preserve that without putting so much information into the main skill.