tla-plus-expert SKILL.md skillA
tla-plus-expert from rysweet/amplihack-rs is an agent skill: a SKILL.md folder an AI agent loads when a task calls for it.
mdr add rysweet/amplihack-rs/tla-plus-expert@v1.0.0Pins v1.0.0 in mdr.lock. Pin the fingerprint instead.
- Audit grade
- A, 17 of 17 checks passed
- Kind
- SKILL.md skill
- Repository
- rysweet/amplihack-rs
- Path
amplifier-bundle/skills/tla-plus-expert/SKILL.md- Versions recorded
- 2
- Latest version
- v1.0.0, committed Jul 27, 2026
- First version recorded
- May 4, 2026
- Size
- 3,589 bytes
- Repository stars
- 11
- License
- none declared
TLA+ formal specification expert for writing specs, model checking, and applying formal methods to amplihack workflows.
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+ Expert Skill ## Purpose Provides expert-level TLA+ formal specification assistance for designing, verifying, and reasoning about concurrent and distributed systems within amplihack. ## When This Skill Activates - User asks to write or review a TLA+ specification - User needs help with model checking (TLC) configuration or output interpretation - User wants to formally verify a protocol or workflow design - User asks about invariants, liveness properties, or safety properties - User wants to apply formal methods to amplihack components - User mentions PlusCal or wants to translate between PlusCal and TLA+ - User references Lamport, Demirbas, or formal methods best practices ## How It Works This skill delegates to the `tla-plus-expert` agent which has deep knowledge of: 1. **TLA+ language and idioms** — writing specs, operators, temporal formulas 2. **TLC model checker** — configuration, trace interpretation, state space management 3. **Seven mental models** (Demirbas) — abstraction, global shared memory, local guards, invariants, stepwise refinement, atomicity refinement, communication 4. **Industry case studies** — 8 production uses from AWS, MongoDB, Microsoft Azure …
Read the whole file at its exact version.
How to install
mdr add rysweet/amplihack-rs/tla-plus-expert@sha256:a29db2e94fbc264bThe line at the top of this page pins the label v1.0.0, 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_dy5fb2nv22sm2uxy)
3 badge image fetches in 30 days. What the badge shows.
Versions
The registry has recorded 2 versions of this file, between May 4, 2026 and Jul 27, 2026, about one every 84 days.
| version | committed | commit | size | audit | |
|---|---|---|---|---|---|
| v1.0.0 latest | 2026-07-27 | 18da0b6 | 3,589 B | A | view · diff |
| v1.0.0 | 2026-05-04 | b7ad1ff | 3,117 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 (3589 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
rysweet/amplihack-rs · 11 stars · license none declared · pushed 2026-10-22 · branch main
API
GET https://markdownregistry.com/api/v1/artifacts/art_dy5fb2nv22sm2uxy GET https://markdownregistry.com/api/v1/resolve?ref=rysweet/amplihack-rs/tla-plus-expert GET https://markdownregistry.com/api/v1/blob/a29db2e94fbc264b493b209ccb872259ecea34067a4a914c418f7da98fc393e5
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.