By younes-io
Write and iteratively refine TLA+ specifications (.tla) and TLC configs (.cfg) from natural language, run model checking, and analyze counterexamples. Author and verify theorem proofs with TLAPS, check obligations, and diagnose failures for protocol and state machine validation.
npx claudepluginhub younes-io/agent-skillsWrite 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.
Write and iteratively refine TLA+ theorem proofs in `.tla` modules with TLAPS (`tlapm`); run proof checks and summarize proved vs failed/omitted obligations with explicit assumptions and trust boundaries. Use when asked to create or fix `THEOREM` or `PROOF` blocks, diagnose TLAPS failures, strengthen inductive invariants, prove equivalence, or tune proof structure.
A portable Agent Skills repo for TLA+ workbenches, with a generated Claude Code plugin wrapper.
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.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
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
Skills live under:
skills/<skill-name>/SKILL.mdskills/<skill-name>/agents/skills/<skill-name>/scripts/skills/<skill-name>/references/Claude-specific wrapper files live under:
.claude-plugin/marketplace.jsonplugins/tla-workbenches/.claude-plugin/plugin.jsonplugins/tla-workbenches/skills/scripts/sync_claude_plugin_skills.shscripts/validate_claude_plugin.shThe 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.
VERSION is the single release source of truth.
When a change to VERSION reaches main, GitHub Actions will:
vX.Y.Z)Normal content changes do not create a release unless VERSION changed in that push.
See skills/tla-check/SKILL.md for full usage.
Examples: https://github.com/younes-io/tlaplus-workbench-examples
Common prerequisites:
bashjqjavatla2tools.jar (set TLA2TOOLS_JAR or pass --jar to the runner script)See skills/tla-proof/SKILL.md for full usage.
Examples: https://github.com/younes-io/tlaplus-workbench-examples
Common prerequisites:
bashjqtlapm (or pass --tlapm with an absolute path/wrapper)TDD-validated implementation planning with plan review quality gate (2 skills, 5 agents, 1 command) - write plans, validate against codebase reality before execution
Skills for developing with Lean 4 and Mathlib — proof methodology, toolchain setup, bisection, and more
24 elite skills across 5 layers: discipline, domain expertise, intelligence, coordination, and execution. Turn Claude Code into a proactive engineering partner.
Core ACE workflow with TDD-based skills, task enforcement, and quality reviewers
Teaches design patterns for workflow-based Claude Code skills and provides a review agent for auditing existing skills
Share bugs, ideas, or general feedback.
Formal methods and specification languages: UML/SysML modeling, TLA+ specifications, OpenAPI/AsyncAPI contract-first design, state machines, and Use Case 2.0 methodology.
Own this plugin?
Verify ownership to unlock analytics, metadata editing, and a verified badge.
Sign in to claimOwn this plugin?
Verify ownership to unlock analytics, metadata editing, and a verified badge.
Sign in to claim