Tla Workbenches

younes-io/agent-skills

A portable Agent Skills repo for TLA+ workbenches, with generated Claude Code and Codex plugin wrappers.

Skills

• 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 (Portable Agent Skills)

List skills from this repo (local checkout):

npx -y skills add . --list

Install from GitHub:

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:

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:

/plugin marketplace add younes-io/agent-skills

Install the plugin:

/plugin install tla-workbenches@younes-agent-skills

Reload plugins:

/reload-plugins

Invoke the plugin-qualified skills:

/tla-workbenches:tla-check
/tla-workbenches:tla-proof

Codex Plugin Install

This repo also ships a Codex-native plugin wrapper.

For a local checkout, add this repo's marketplace file in Codex:

.agents/plugins/marketplace.json

The Codex marketplace entry points at:

plugins/tla-workbenches

The Codex plugin manifest lives at:

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

Once installed, invoke the skills from Codex with:

$tla-check
$tla-proof

Repo layout

Skills live under:

• skills/<skill-name>/SKILL.md
• skills/<skill-name>/agents/
• skills/<skill-name>/scripts/
• skills/<skill-name>/references/

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

Codex-specific wrapper files live under:

• .agents/plugins/marketplace.json
• plugins/tla-workbenches/.codex-plugin/plugin.json
• plugins/tla-workbenches/assets/
• scripts/validate_codex_plugin.sh

The root skills/ directory is the only editable source of skill content. The plugin skills/ tree is generated from it and committed for GitHub-based Claude Code and Codex installs.

Releases

VERSION is the single release source of truth.

When a change to VERSION reaches main, GitHub Actions will:

• sync the release version into the Claude and Codex plugin manifests
• validate the repo state
• create and push the matching Git tag (vX.Y.Z)
• create the matching GitHub Release

Normal content changes do not create a release unless VERSION changed in that push.

tla-check prerequisites

See skills/tla-check/SKILL.md for full usage.

Examples: https://github.com/younes-io/tlaplus-workbench-examples

Common prerequisites:

• bash
• jq
• java
• tla2tools.jar (set TLA2TOOLS_JAR or pass --jar to the runner script)

tla-proof prerequisites

See skills/tla-proof/SKILL.md for full usage.

Examples: https://github.com/younes-io/tlaplus-workbench-examples

Common prerequisites:

• bash
• jq
• tlapm (or pass --tlapm with an absolute path/wrapper)