feat: add an agent skill for coding assistants

.agents/plugins/marketplace.json

@@ -0,0 +1,19 @@
+{
+  "name": "anodized",
+  "interface": {
+    "displayName": "Anodized"
+  },
+  "plugins": [
+    {
+      "name": "anodized",
+      "source": {
+        "source": "local",
+        "path": "./plugins/anodized"
+      },
+      "policy": {
+        "installation": "AVAILABLE"
+      },
+      "category": "Developer Tools"
+    }
+  ]
+}

.claude-plugin/marketplace.json

@@ -0,0 +1,32 @@
+{
+  "$schema": "https://anthropic.com/claude-code/marketplace.schema.json",
+  "name": "anodized",
+  "owner": {
+    "name": "anodized-rs"
+  },
+  "metadata": {
+    "description": "The Anodized agent skill: write and review `#[spec]` specifications in Rust."
+  },
+  "plugins": [
+    {
+      "name": "anodized",
+      "source": "./plugins/anodized",
+      "description": "Write, review, and debug Anodized `#[spec]` specifications on Rust functions, traits, loops, structs, and enums, and run the runtime-check build configurations.",
+      "version": "0.7.0",
+      "author": {
+        "name": "anodized-rs"
+      },
+      "homepage": "https://github.com/anodized-rs/anodized",
+      "repository": "https://github.com/anodized-rs/anodized",
+      "license": "MIT OR Apache-2.0",
+      "category": "development",
+      "keywords": [
+        "anodized",
+        "rust",
+        "specification",
+        "design-by-contract",
+        "verification"
+      ]
+    }
+  ]
+}

.github/workflows/ci.yml

@@ -140,6 +140,25 @@ jobs:
       - name: Integration test anodized-logic
         run: cargo test -p anodized-logic --tests --no-fail-fast
 
+  test-skill-tools:
+    name: Lint and test skill-tools
+    runs-on: ubuntu-latest
+    needs: fmt
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@1.95.0
+        with:
+          components: clippy
+
+      - name: Lint skill-tools
+        run: cargo clippy -p skill-tools --all-targets -- -D warnings
+
+      - name: Validate the agent skill and plugin manifests
+        run: cargo test -p skill-tools --tests --no-fail-fast
+
   test-test-util:
     name: Lint test-util
     runs-on: ubuntu-latest

.gitignore

@@ -15,3 +15,6 @@ Cargo.lock
 
 # macOS specific files
 .DS_Store
+
+# Local agent configuration
+.claude/

AGENTS.md

@@ -0,0 +1 @@
+CLAUDE.md

CHANGELOG.md

@@ -7,6 +7,20 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Added
+
+- **[anodized] Agent skill and plugin** - The repository now ships an agent skill for Claude
+  Code and Codex under `plugins/anodized`, installable with
+  `claude plugin marketplace add anodized-rs/anodized`. Its factual tables are generated from
+  the crate sources and its examples are compiled, so it cannot drift from the syntax it
+  documents.
+
+### Fixed
+
+- **[anodized] Repaired the examples in `REFERENCE.md`** - Several examples still used the
+  pre-0.6 postcondition syntax and did not compile; others warned, or asserted a comparison
+  the type already guaranteed.
+
 ## 0.7.0 (2026 Sep 27)
 
 ### Breaking Changes

CLAUDE.md

@@ -0,0 +1,100 @@
+# Working on Anodized
+
+This file is for agents changing *this repository*. The skill under
+`plugins/anodized/skills/anodized/` is a different thing: it teaches people who *use* the
+crate how to write specs. Both exist; do not confuse them.
+
+## Layout
+
+| Crate | Owns |
+| --- | --- |
+| `anodized` | The user-facing facade: re-exports `spec`, plus `result` and `try_call!`. |
+| `anodized-macros` | The proc macro, and the `cfg` dispatch that decides what it emits. |
+| `anodized-core` | Parsing and instrumentation. The real logic, and the tool interop layer. |
+| `anodized-logic` | `int`, `implies!`, `opaque!`, `forall`, `exists`. |
+| `anodized-fmt` | Formatter library and CLI for `#[spec(...)]`. |
+| `test-util` | Internal test helpers. Not published. |
+| `skill-tools` | Generates and validates the agent skill. Not published. |
+
+`README.md` is a symlink to `crates/anodized/README.md`, which is included as the crate's
+rustdoc via `#![doc = include_str!]` — so **its examples are doctested**.
+
+## Build configurations
+
+There are **no Cargo features**. Behavior is controlled entirely by `--cfg` flags:
+
+| Flag | Effect |
+| --- | --- |
+| *(none)* | Specs embedded and type-checked; no checks run. |
+| `anodized_discard_specs` | Specs dropped entirely; incompatible with all other flags. |
+| `anodized_embed_specs` | Specs emitted as separate items for analysis; incompatible with runtime-check flags. |
+| `anodized_charon` | Embedding with Charon contract attributes; requires nightly and Charon tool registration. |
+| `anodized_print` | Violations report to stderr and continue. |
+| `anodized_panic` | Violations panic. |
+| `anodized_try` | Enables `try_call!`. Requires `anodized_panic`. |
+
+CI passes them as `cargo --config 'build.rustflags=["--cfg","anodized_panic"]' test`. Adding a
+new flag means updating `check-cfg` in **both** `crates/anodized/Cargo.toml` and
+`crates/anodized-macros/Cargo.toml`; `skill-tools` fails if the documented set drifts.
+
+## Commands
+
+```bash
+cargo fmt --all -- --check
+cargo clippy -p <crate> --all-targets -- -D warnings
+cargo test -p anodized --tests --no-fail-fast
+cargo test -p skill-tools --tests --no-fail-fast
+cargo run -p skill-tools --bin skill-gen -- --write
+```
+
+## Conventions
+
+Clippy must be clean. **No `#[allow]`** — fix the cause, or delete the code. No `unwrap`,
+`expect`, or `panic!` in production paths; propagate with `?`. Files stay under 500 lines.
+
+Unit tests live in a sibling file, wired up with `#[cfg(test)] #[path = "x_tests.rs"] mod`.
+Integration tests are one file per feature under `crates/anodized/tests/`. UI tests use
+trybuild with `.stderr` goldens — regenerate with `TRYBUILD=overwrite`. `anodized-fmt` uses
+golden fixtures under `tests/fixtures/`.
+
+## Editing the agent skill
+
+`plugins/anodized/skills/anodized/` is a shipped artifact.
+
+- Every ```` ```rust ```` block in it is compiled by `cargo test -p skill-tools`. So is every
+  block in `crates/anodized/REFERENCE.md`.
+- The tables between `<!-- anodized:generated:... -->` markers are generated. Edit
+  `crates/skill-tools/src/generate.rs`, then run `skill-gen --write`. Do not hand-edit inside
+  the markers.
+- Change a clause keyword, a qualifier, a `cfg` flag, or a macro error message and the tests
+  will name the document that needs updating.
+
+Loop conditions are dropped before they reach the compiler, so "every block compiles" proves
+nothing about their validity. Read them by eye. Both `struct` and `enum` conditions generate
+a type-checked `Spec::predicate`; test that predicate or enforce it at a `Spec!(T)` function
+boundary to check the invariant at runtime.
+
+**No test covers meaning.** The coverage tests assert that a term *appears*; they cannot tell
+whether the sentence around it is still true. Changing spec semantics requires a manual read
+of `SKILL.md` and `reference.md`. This is the residual risk and it is not automatable.
+
+## Which documents are verified
+
+| Document | Verified? |
+| --- | --- |
+| `crates/anodized/README.md` | Yes — doctested as crate rustdoc. |
+| `crates/anodized/REFERENCE.md` | Examples only, via `skill-tools`. Prose is not. |
+| The agent skill | Examples, tables, and runtime claims, via `skill-tools`. Prose is not. |
+
+When they disagree, the skill and the README win.
+
+## Releasing
+
+Bump, in one commit: `[workspace.package] version` and the `[workspace.dependencies]`
+`anodized*` lines; the `anodized = "x.y.z"` snippet in `crates/anodized/README.md`;
+`version` in `.claude-plugin/marketplace.json`, `plugins/anodized/.claude-plugin/plugin.json`,
+and `plugins/anodized/.codex-plugin/plugin.json`; and `CHANGELOG.md`.
+
+The plugin version is always the workspace version. `skill-tools` reads its own
+`CARGO_PKG_VERSION` — which is the workspace version — and fails if a manifest disagrees, so a
+mismatched plugin cannot be released.

Cargo.toml

@@ -6,6 +6,7 @@ members = [
     "crates/anodized-logic",
     "crates/anodized-macros",
     "crates/cargo-anodized",
+    "crates/skill-tools",
     "crates/test-util",
     "fuzz",
 ]
@@ -34,6 +35,7 @@ keywords = [
 ]
 
 [workspace.dependencies]
+anodized = { version = "0.7.0", path = "crates/anodized" }
 anodized-core = { version = "0.7.0", path = "crates/anodized-core" }
 anodized-fmt = { version = "0.7.0", path = "crates/anodized-fmt" }
 anodized-logic = { version = "0.7.0", path = "crates/anodized-logic" }

crates/anodized/README.md

@@ -101,6 +101,24 @@ reported before the panic.
 
 For more details and other approaches, see [The Anodized Reference](https://github.com/anodized-rs/anodized/blob/main/crates/anodized/REFERENCE.md).
 
+## Using Anodized with a Coding Agent
+
+Anodized ships an agent skill, so an assistant writes current `#[spec]` syntax instead of guessing from other contract systems.
+
+```sh
+# Claude Code
+claude plugin marketplace add anodized-rs/anodized
+claude plugin install anodized@anodized
+
+# Codex
+codex plugin marketplace add anodized-rs/anodized
+codex plugin add anodized@anodized
+```
+
+The skill loads by itself when you mention Anodized or `#[spec]`. It also adds two commands: `/anodized:spec` to add specs to code you point it at, and `/anodized:check` to run your tests under every build configuration.
+
+Using an agent with no plugin support? Point it at [the skill directory](https://github.com/anodized-rs/anodized/tree/main/plugins/anodized/skills/anodized).
+
 ## Why Anodized
 
 Rust has a growing ecosystem of excellent verification tools - Aeneas, Creusot, Flux, Hax, Kani, Prusti, Verus, and more. Each one brings unique strengths. Anodized provides a shared specification layer so that these tools, and the developers who use them, do not have to go it alone.

crates/skill-tools/Cargo.toml

@@ -0,0 +1,17 @@
+[package]
+name = "skill-tools"
+description = "Generates and validates the Anodized agent skill and its plugin manifests"
+publish = false
+
+version.workspace = true
+edition.workspace = true
+rust-version.workspace = true
+license.workspace = true
+repository.workspace = true
+
+[dependencies]
+anodized-core.workspace = true
+serde_json = "1"
+
+[dev-dependencies]
+anodized.workspace = true

crates/skill-tools/src/bin/skill-gen.rs

@@ -0,0 +1,53 @@
+//! Rewrites, or verifies, the generated tables in the Anodized agent skill.
+
+use std::process::ExitCode;
+
+use skill_tools::generate;
+
+fn main() -> ExitCode {
+    let mode = std::env::args().nth(1);
+    match mode.as_deref() {
+        Some("--write") => run(write),
+        Some("--check") | None => run(check),
+        Some(other) => {
+            eprintln!("unknown argument `{other}`; expected `--write` or `--check`");
+            ExitCode::FAILURE
+        }
+    }
+}
+
+fn run(action: fn() -> skill_tools::Result<bool>) -> ExitCode {
+    match action() {
+        Ok(true) => ExitCode::SUCCESS,
+        Ok(false) => ExitCode::FAILURE,
+        Err(error) => {
+            eprintln!("error: {error}");
+            ExitCode::FAILURE
+        }
+    }
+}
+
+fn write() -> skill_tools::Result<bool> {
+    let changed = generate::write()?;
+    if changed.is_empty() {
+        println!("generated regions are already up to date");
+    } else {
+        for file in changed {
+            println!("updated {file}");
+        }
+    }
+    Ok(true)
+}
+
+fn check() -> skill_tools::Result<bool> {
+    let stale = generate::check()?;
+    if stale.is_empty() {
+        println!("generated regions are up to date");
+        return Ok(true);
+    }
+    for region in stale {
+        eprintln!("stale generated region: {region}");
+    }
+    eprintln!("run `cargo run -p skill-tools --bin skill-gen -- --write`");
+    Ok(false)
+}