add Claude plugin wrapper and rename TLA skills (#12)

Author: younes-io

.claude-plugin/marketplace.json

@@ -0,0 +1,21 @@
+{
+  "name": "younes-agent-skills",
+  "owner": {
+    "name": "younes-io"
+  },
+  "metadata": {
+    "description": "Portable TLA+ agent skills for Claude Code and other Agent Skills clients.",
+    "version": "0.1.0"
+  },
+  "plugins": [
+    {
+      "name": "tla-workbenches",
+      "description": "TLA+ workbench skills for TLC model checking and TLAPS proofs.",
+      "version": "0.1.0",
+      "author": {
+        "name": "younes-io"
+      },
+      "source": "./plugins/tla-workbenches"
+    }
+  ]
+}

.github/workflows/skill-ci.yml

@@ -7,8 +7,8 @@ on:
       - main
 
 jobs:
-  tlaps-workbench:
-    name: TLAPS Workbench Script Tests
+  tla-proof:
+    name: TLA Proof Script Tests
     runs-on: ubuntu-latest
 
     steps:
@@ -24,10 +24,10 @@ jobs:
       - name: Shell syntax checks
         run: |
           set -euo pipefail
-          bash -n skills/tlaps-workbench/scripts/tlaps_check.sh
-          bash -n skills/tlaps-workbench/scripts/tests/tlaps_check_test.sh
+          bash -n skills/tla-proof/scripts/tlaps_check.sh
+          bash -n skills/tla-proof/scripts/tests/tlaps_check_test.sh
 
       - name: Run TLAPS runner regression tests
         run: |
           set -euo pipefail
-          bash skills/tlaps-workbench/scripts/tests/tlaps_check_test.sh
+          bash skills/tla-proof/scripts/tests/tlaps_check_test.sh

.github/workflows/validate.yml

@@ -0,0 +1,28 @@
+name: Validate
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  validate:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-node@v4
+        with:
+          node-version: 20
+
+      - name: Validate portable skill pack
+        run: npx -y skills add . --list
+
+      - name: Sync generated Claude plugin skills
+        run: ./scripts/sync_claude_plugin_skills.sh
+
+      - name: Check generated plugin skills are committed
+        run: git diff --exit-code -- plugins/tla-workbenches/skills
+
+      - name: Validate Claude plugin metadata and generated skills
+        run: ./scripts/validate_claude_plugin.sh

README.md

@@ -1,13 +1,13 @@
 # younes-io/agent-skills
 
-A small skill pack compatible with the Vercel `skills` CLI.
+A portable Agent Skills repo for TLA+ workbenches, with a generated Claude Code plugin wrapper.
 
 ## Skills
 
-- `tlaplus-workbench`: Write and iteratively refine executable TLA+ specs (`.tla`) and TLC configs (`.cfg`), run TLC model checking, and summarize counterexamples.
-- `tlaps-workbench`: Write and iteratively refine TLAPS theorem proofs in TLA+ (`.tla`), run `tlapm`, and summarize proved vs failed/omitted obligations.
+- `tla-check`: Write and iteratively refine executable TLA+ specs (`.tla`) and TLC configs (`.cfg`), run TLC model checking, and summarize counterexamples.
+- `tla-proof`: Write and iteratively refine TLAPS theorem proofs in TLA+ (`.tla`), run `tlapm`, and summarize proved vs failed/omitted obligations.
 
-## Install / List (Vercel skills CLI)
+## Install / List (Portable Agent Skills)
 
 List skills from this repo (local checkout):
 
@@ -18,15 +18,42 @@ npx -y skills add . --list
 Install from GitHub:
 
 ```bash
-npx -y skills add younes-io/agent-skills --skill tlaplus-workbench
-npx -y skills add younes-io/agent-skills --skill tlaps-workbench
+npx -y skills add younes-io/agent-skills --skill tla-check
+npx -y skills add younes-io/agent-skills --skill tla-proof
 ```
 
 Alternatively, use the URL form:
 
 ```bash
-npx -y skills add https://github.com/younes-io/agent-skills.git --skill tlaplus-workbench
-npx -y skills add https://github.com/younes-io/agent-skills.git --skill tlaps-workbench
+npx -y skills add https://github.com/younes-io/agent-skills.git --skill tla-check
+npx -y skills add https://github.com/younes-io/agent-skills.git --skill tla-proof
+```
+
+## Claude Code Install
+
+Add the marketplace in Claude Code:
+
+```text
+/plugin marketplace add younes-io/agent-skills
+```
+
+Install the plugin:
+
+```text
+/plugin install tla-workbenches@younes-agent-skills
+```
+
+Reload plugins:
+
+```text
+/reload-plugins
+```
+
+Invoke the plugin-qualified skills:
+
+```text
+/tla-workbenches:tla-check
+/tla-workbenches:tla-proof
 ```
 
 ## Repo layout
@@ -38,9 +65,19 @@ Skills live under:
 - `skills/<skill-name>/scripts/`
 - `skills/<skill-name>/references/`
 
-## tlaplus-workbench prerequisites
+Claude-specific wrapper files live under:
+
+- `.claude-plugin/marketplace.json`
+- `plugins/tla-workbenches/.claude-plugin/plugin.json`
+- `plugins/tla-workbenches/skills/`
+- `scripts/sync_claude_plugin_skills.sh`
+- `scripts/validate_claude_plugin.sh`
+
+The root `skills/` directory is the only editable source of skill content. The Claude plugin `skills/` tree is generated from it and committed for GitHub-based Claude Code installs.
+
+## tla-check prerequisites
 
-See `skills/tlaplus-workbench/SKILL.md` for full usage.
+See `skills/tla-check/SKILL.md` for full usage.
 
 Examples: <https://github.com/younes-io/tlaplus-workbench-examples>
 
@@ -50,9 +87,9 @@ Common prerequisites:
 - `java`
 - `tla2tools.jar` (set `TLA2TOOLS_JAR` or pass `--jar` to the runner script)
 
-## tlaps-workbench prerequisites
+## tla-proof prerequisites
 
-See `skills/tlaps-workbench/SKILL.md` for full usage.
+See `skills/tla-proof/SKILL.md` for full usage.
 
 Examples: <https://github.com/younes-io/tlaplus-workbench-examples>
 

plugins/tla-workbenches/.claude-plugin/plugin.json

@@ -0,0 +1,8 @@
+{
+  "name": "tla-workbenches",
+  "version": "0.1.0",
+  "description": "TLA+ workbench skills for TLC model checking and TLAPS proofs.",
+  "author": {
+    "name": "younes-io"
+  }
+}

skills/tlaplus-workbench/SKILL.md …la-workbenches/skills/tla-check/SKILL.mdskills/tlaplus-workbench/SKILL.md renamed to plugins/tla-workbenches/skills/tla-check/SKILL.md skills/tlaplus-workbench/SKILL.md renamed to plugins/tla-workbenches/skills/tla-check/SKILL.md

@@ -1,15 +1,15 @@
 ---
-name: tlaplus-workbench
-description: "Write and iteratively refine executable TLA+ specs (.tla) and TLC model configs (.cfg) from natural-language system designs; run TLC model checking; summarize pass/fail and counterexamples with explicit assumptions and bounds. Use when asked to: design/validate a state machine or distributed protocol with TLA+, create/edit .tla or .cfg files, run TLC, or interpret TLC failures/counterexamples."
+name: tla-check
+description: "Write and iteratively refine executable TLA+ specs (.tla) and TLC model configs (.cfg) from natural-language system designs; run TLC model checking; summarize pass/fail and counterexamples with explicit assumptions and bounds. Use when asked to design or validate a protocol/state machine, create or edit .tla/.cfg files, run TLC, or interpret TLC failures."
 ---
 
-# TLA+ Workbench
+# TLA+ Check
 
 ## Outputs
 
 - TLA+ spec(s): `*.tla`
 - TLC config(s): `*.cfg`
-- TLC run artifacts: `.tlaplus-workbench/runs/<run-id>/...` (logs, json trace if any)
+- TLC run artifacts: `.tla-check/runs/<run-id>/...` (logs, json trace if any)
 
 ## Non-Negotiables (Honesty Rules)
 
@@ -97,17 +97,17 @@ Prereqs:
 - `jq` on PATH
 - `tla2tools.jar` available and pointed to by `TLA2TOOLS_JAR` (or pass `--jar`)
 
-Run (from the `tlaplus-workbench` skill directory):
+Run (from the `tla-check` skill directory):
 
 ```bash
 scripts/tlc_check.sh --spec path/to/Foo.tla --cfg path/to/Foo.cfg
 ```
 
 This writes a run directory under the spec folder:
-- `.tlaplus-workbench/runs/<run-id>/summary.json`
-- `.tlaplus-workbench/runs/<run-id>/tlc.stdout`
-- `.tlaplus-workbench/runs/<run-id>/tlc.stderr`
-- `.tlaplus-workbench/runs/<run-id>/counterexample.json` (only if TLC produced one)
+- `.tla-check/runs/<run-id>/summary.json`
+- `.tla-check/runs/<run-id>/tlc.stdout`
+- `.tla-check/runs/<run-id>/tlc.stderr`
+- `.tla-check/runs/<run-id>/counterexample.json` (only if TLC produced one)
 
 ### 5) Iterate (Tight Loop)
 

plugins/tla-workbenches/skills/tla-check/agents/openai.yaml

@@ -0,0 +1,4 @@
+interface:
+  display_name: "TLA+ Check"
+  short_description: "Write and check TLA+ specs with TLC"
+  default_prompt: "Turn a natural-language system design into a minimal TLA+ spec (.tla) and TLC model config (.cfg), run TLC model checking, summarize results and counterexamples with explicit bounds and assumptions, and iterate until either properties pass within bounds or a counterexample remains."

…us-workbench/references/spec_skeleton.md …ls/tla-check/references/spec_skeleton.mdskills/tlaplus-workbench/references/spec_skeleton.md renamed to plugins/tla-workbenches/skills/tla-check/references/spec_skeleton.md skills/tlaplus-workbench/references/spec_skeleton.md renamed to plugins/tla-workbenches/skills/tla-check/references/spec_skeleton.md

@@ -17,7 +17,7 @@ Options:
   --java BIN            Java executable (default: java)
   --workers N           TLC workers (default: 1)
   --timeout-secs N      Kill TLC after N seconds (default: 0 = no timeout)
-  --out-root PATH       Run artifact root (default: <spec-dir>/.tlaplus-workbench/runs)
+  --out-root PATH       Run artifact root (default: <spec-dir>/.tla-check/runs)
   --trace-max-steps N   Max trace steps in counterexample summary (default: 50)
   -h, --help            Show this help
 EOF
@@ -302,7 +302,7 @@ fi
 if [[ -n "$OUT_ROOT" ]]; then
   out_root="$(abs_maybe_missing "$OUT_ROOT")"
 else
-  out_root="$spec_dir/.tlaplus-workbench/runs"
+  out_root="$spec_dir/.tla-check/runs"
 fi
 
 mkdir -p "$out_root"