A tool for drawing Mermaid statecharts from TLA+ models. A statechart shows how a system moves between observable states, and TLA+ is a formal language for describing and checking system behavior.

Use it to show bugs as state transitions, explain a protocol or service to reviewers, or turn an agreed chart into a TLA+ model.

It makes complex product flows, protocols, and services easier to inspect as paths between states. It can highlight a numbered path that reaches a state where a rule is broken.

statechart — Skill for Claude Code and Cursor by backnotprop/pstack

About the project

pstack is a collection of plain Agent Skills and engineering principles that guide AI-assisted software development across coding agents such as Claude Code, Codex, Pi, Cursor, and OpenCode. It is for developers who want reusable practices for tasks including testing, technical writing, debugging, review, and coordinating agent work. The catalogue entries are the project's skills, agents, and plugin.

backnotprop/pstack · 2,800 stars · on GitHub

Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

Any agent

npx skills add backnotprop/pstack --skill statechart

Clone the repo

git clone --depth 1 https://github.com/backnotprop/pstack

Made for: Claude Code, Cursor.

Or install pstack, the plugin that ships this one along with the rest of its 61 skills, 2 agents.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

README.md

[![agentmods](https://agentmods.dev/badge/skills/backnotprop/pstack/statechart/github.svg)](https://agentmods.dev/skills/backnotprop/pstack/statechart)

Your own site

<a href="https://agentmods.dev/skills/backnotprop/pstack/statechart"><img src="https://agentmods.dev/badge/skills/backnotprop/pstack/statechart/github.svg" alt="Measured on agentmods" height="20"></a>

Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.

Your own site · 80×15

<a href="https://agentmods.dev/skills/backnotprop/pstack/statechart"><img src="https://agentmods.dev/badge/skills/backnotprop/pstack/statechart.svg" alt="Reviewed on agentmods" width="80" height="20"></a>

Per session 82 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.

When invoked 1,774 The whole file, excluding the scripts and references it only reads on demand.

Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe.

Origin original No closer match found in the catalogue.

Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

Model	Per session	Once invoked
Fable 5.1	$0.00082	$0.01774
Opus 5.5	$0.00033	$0.00710
Sonnet 5.5	$0.00016	$0.00355
Haiku 4.5	$0.00008	$0.00177

Measured 2d ago against content hash b1c544782b15, method: parsed. Prices are Anthropic first-party input rates as of 2026-10-07, from the pricing page.

Security

Grade A, and why

statechart scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 2d ago.

The scan reads SKILL.md. This mod also ships 22 executable files (scripts/bug-states.mjs, scripts/chart-edges.mjs, scripts/chart-parts.mjs, …), listed below but not scanned — reading those needs a real analyzer, not pattern matching.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

skills/statechart/SKILL.md · 37 lines

How it starts

The opening of the file, as written. The whole thing — 37 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Statechart

The chart shows how a system moves between states, in the words of the person who reads it. The scripts call that person the reader, as in readerActions and reader steps. The reader decides whether the behavior is right. The reader can be a PM who reads a product flow, an engineer who reads a protocol or a service, or a reviewer who reads a design. Label each state with what the reader can observe or cares about, such as "Paying" in an app or "Lease held, write pending" in a lock service. Label each step with the event that moves the system, such as "tap Pay" in an app, "the request reads the count" in a service, or "the lease expires" in a lock service. Keep variable and action names out of labels.

Run node <skill dir>/scripts/statechart.mjs --help for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input. The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network. The help's TLC section tells how to use a TLC and Java that you have.

Pick the direction

Use from-spec when a TLA+ model exists, or when the code or design is concrete enough to model. Use from-chart when there is no model, and the people who own the behavior should agree on it before anyone builds or changes it.

If the code already has a TLA+ spec, start from a copy of that spec. Add the variables that the labels and rules need, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as --against. Check it with the config that its authors say it passes, and pass that config as --against-config unless it has the spec's file name. One mapping labels both models, so label states and steps from variables that both have. A label that reads a variable that only the copy has must test "name" in v first, and label the spec's states another way. When a model describes code, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code. Put the file and line of the code that checks each condition of an action in a comment on that condition, as in \* pay.ts:120.

Read the full file on GitHub · 37 lines

Files

What ships with it

26 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

2d ago First seen · 37 lines · 82 tokens per session scan A b1c544782b15

Subscribe to this mod's changes

statechart is a skill published in the GitHub repository backnotprop/pstack (2,800 stars, last pushed today), licensed MIT. It adds 82 tokens to every session and 1,774 once invoked, about $0.0003 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-10-24.

Debugging Planning agent-skills agentskills backnotprop pstack pstack-claude skills

analyze-kernel-bottleneck

Systematically identify whether a GPU kernel is compute-bound, memory-bound, or latency-bound using roofline analysis, occupancy calculations, compute/load ratio per tile, and SASS instruction inspection. Produces a decision matrix for optimization strategy selection (cp.async, warp interleaving, tiling…

pjt222/agent-almanac · 77 tokens

conduct-empirical-wire-capture

Capture outbound HTTP and telemetry from a CLI harness at runtime. Covers capture-channel selection (transcript file vs verbose-fetch stderr vs outbound proxy vs on-disk state), hook-driven per-event capture vs long-running session capture, JSONL output format for diff-friendly artifacts, and the observability table…

pjt222/agent-almanac · 117 tokens

decode-minified-js-gates

Classify gate call variants in a minified JavaScript bundle. Covers context-window extraction around a flag occurrence, identification of 4–6 reader variants (sync boolean, sync config-object, bootstrap-aware TTL, truthy-only, async bootstrap, async bridge), default-value extraction (boolean / null / numeric /…

pjt222/agent-almanac · 138 tokens

correlate-observability-signals

Unify metrics, logs, and traces for cohesive debugging. Implement exemplars for log-to-trace linking, build unified dashboards using RED/USE methods, and enable rapid root cause analysis across observability signals. Use when investigating complex incidents spanning multiple systems, reducing mean time to resolution…

pjt222/agent-almanac · 83 tokens

chrysopoeia

Extract maximum value from existing code — performance optimization, API surface refinement, and dead weight elimination. The art of turning base code into gold through systematic identification and amplification of value-bearing patterns. Use when optimizing a working but sluggish codebase, refining an API surface…

pjt222/agent-almanac · 94 tokens

clean-codebase

Remove dead code, unused imports, fix lint warnings, and normalize formatting across a codebase without changing business logic or architecture. Use when lint warnings have piled up during rapid development, unused imports and variables clutter files, dead code paths were never removed, formatting is inconsistent, or…

pjt222/agent-almanac · 68 tokens