Menu

Individual skill

statechart

Model-check a TLA+ spec with TLC and turn the result into a reader-labeled Mermaid state diagram plus a report of the shortest path to every violated rule. Use on /statechart, to explain a bug as a walk through states, or to read any TLA+ result (formal verify skills route here).

plugins/requie/endostack/skills/statechart/SKILL.md

Read pinned source

Source commit d780783eba4ecc7c8b9429f95c9362df95f07c61

What was checked

Matches the observed repository HEAD
Yes
Scanner rules are current
Yes
Repository scan complete
No
Skill scan complete
No
Observed behavior
Network or broad shell
Last checked
Nov 4, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings)
1,537
Repository last updated
Nov 7, 2026
License
Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files
Read excerpt

# statechart

Run TLC on a TLA+ spec of anything with discrete states (a signup flow, a network protocol, a job queue) and present the result in the terms of the person who has to judge it. The tool writes a Mermaid state diagram and a markdown report that gives, for every violated rule, the shortest sequence of steps that reaches the violation.

Verify skills produced by the `create-formal-verification-skill` skill ([../create-formal-verification-skill/SKILL.md](../create-formal-verification-skill/SKILL.md)) send their TLA+ results here. Do not use this skill for other formalisms or for systems with no meaningful discrete state.

The CLI is `scripts/statechart`. Its flags, environment variables, and exit codes are documented in [scripts/README.md](scripts/README.md) and in its usage text; this file covers how to use it well.

## Running it

1. Copy the spec and its config into a throwaway directory outside the repo (`mktemp -d`), so generated files never land in a commit.
2. Run `scripts/statechart <spec.tla>`, adding the config, view, and output-folder flags from the README as needed. By default it reads the `.cfg` beside the spec and writes to a new `<spec>-chart` folder. The output folder must be absent or empty.
3. The first run downloads a pinned TLA+ tools jar (checked against a SHA-256), so it needs network access once. It never installs Java: you need Java 11 or later on `PATH`, or `JAVA` pointing at one. Read the README for the variables that point it at a jar you already have or block the download.