tlaplus SKILL.md skillA
tlaplus from swingerman/engineer is an agent skill: a SKILL.md folder an AI agent loads when a task calls for it.
mdr add swingerman/engineer/tlaplus@git:20260923.5520e1ePins git:20260923.5520e1e in mdr.lock. Pin the fingerprint instead.
- Audit grade
- A, 17 of 17 checks passed
- Kind
- SKILL.md skill
- Repository
- swingerman/engineer
- Path
engineer/skills/tlaplus/SKILL.md- Versions recorded
- 2
- Latest version
- git:20260923.5520e1e, committed Sep 23, 2026
- First version recorded
- Sep 23, 2026
- Size
- 7,084 bytes
- Repository stars
- 162
- License
- MIT
Use to model-check real code or a design with TLA+ and TLC. Model retries, locks, async flows, protocols or state machines as written, check invariants over every interleaving, and reproduce any counterexample trace as a failing test. Dispatched by /engineer.harden for concurrency- and ordering-shaped risks; also usable directly, including to spec a design before building it. Triggers — "/engineer.tlaplus", "use TLA+ to verify X", "model-check X for races/deadlocks…
Collected from public GitHub. Every version is saved exactly as it was and never changes. Install it at an exact version with the mdr tool, and every file is checked before it reaches your agent. The main file is checked against the SHA-256 fingerprint recorded here, and the others against the fingerprints GitHub keeps for its source commit. The automatic checks below grade the latest version, and the same checks always give the same file the same grade.
What the file says
# TLA+
TLA+ earns its keep by finding the counterexample you didn't think of. Don't
write a spec and declare victory without actually running TLC — an
uncompiled/unchecked spec is just prose with extra syntax.
## Setup check
`java -version` (TLC needs a JVM 11+; if it's missing, tell the user rather than
installing one). The model checker jar (`tla2tools.jar`, pinned to v1.7.4)
auto-downloads on first run via
`${CLAUDE_PLUGIN_ROOT}/skills/tlaplus/scripts/tlc.sh`, no separate install step needed.
## Translating an informal design into TLA+
When the user describes a protocol/state machine in plain language, structure
the spec around these pieces — this is the actual translation work, not
boilerplate:
1. **`VARIABLES`** — the pieces of state that change. Keep this minimal;
every variable multiplies the state space TLC has to explore.
2. **`Init`** — the starting state predicate.
3. **Actions** — one predicate per state transition (e.g. `SendMsg`,
`Crash`, `Receive`). `Next == SendMsg \/ Receive \/ Crash \/ ...`
4. **Invariants** — the safety properties that must hold in *every* reachable
state (e.g. `NoDataLoss`, `MutualExclusion`). These are what TLC actually
…Read the whole file at its exact version.
How to install
mdr add swingerman/engineer/tlaplus@sha256:351a1ac44c2c9addThe line at the top of this page pins the label git:20260923.5520e1e, which is what most people want. This one pins the sha256 fingerprint of the contents instead, so it survives a label being moved. Either way the exact version is written to mdr.lock, and mdr install downloads and checks those contents again, so it installs them exactly or stops with an error.
[](https://markdownregistry.com/a/art_2tci745salp4qy6y)
5 badge image fetches in 30 days. What the badge shows.
Versions
The registry has recorded 2 versions of this file, all committed on Sep 23, 2026.
| version | committed | commit | size | audit | |
|---|---|---|---|---|---|
| git:20260923.5520e1e latest | 2026-09-23 | 5520e1e | 7,084 B | A | view · diff |
| git:20260923.37de0f0 | 2026-09-23 | 37de0f0 | 7,192 B | A | view |
Audit of the latest version
- pass: Frontmatter block present
- pass: Frontmatter declares a name
- pass: Frontmatter declares a description
- pass: Size between 200 bytes and 200 KB (7084 bytes)
- pass: No zero-width or bidi control characters
- pass: No instruction hidden inside an HTML comment
- pass: No link to an exfiltration or paste host
- pass: No credential-shaped string
- pass: No instruction to send local credentials anywhere
- pass: No text hidden with inline styles
- pass: No prompt-injection phrasing
- pass: No curl or wget piped into a shell
- pass: No recursive delete of root, home or parent
- pass: No instruction to read or print local credentials
- pass: No base64 blob over 200 characters
- pass: No link to a raw IP address
- pass: No script tag
Source
swingerman/engineer · 162 stars · license MIT · pushed 2026-10-27 · branch master
API
GET https://markdownregistry.com/api/v1/artifacts/art_2tci745salp4qy6y GET https://markdownregistry.com/api/v1/resolve?ref=swingerman/engineer/tlaplus GET https://markdownregistry.com/api/v1/blob/351a1ac44c2c9add50a93708cdd8563373d37f6898aaf11a7485c4e5bf7ac513
Your AI assistant does the legwork. You hear about the deals worth your word. Hand yours the standing instructions at modelranch.com and it joins the network that reads files like this one.
Guides: the SKILL.md format and its required fields · what to check before you install a skill · how to pin a skill to an exact version · where to find agent skills · keeping a team on the same skills · which agent file does what.