[chhoumann]

t3-pstack moves to Lauren Tan's pstack at cursor/plugins 4ec7ffa for all three components. Only pstack changed upstream, only in the statechart skill that rc.17 shipped, and its version stays at 0.15.30. Two upstream PRs land. #776 fixes the skill, and #779 cleans up its scripts with no change in behavior.

pstack #776 brings the skill up to its current version. Before it, a run could draw a wrong chart or exit with the wrong code and not say so.

• The label map stops on a variable or field that the --fixed or --against model lacks. Before, it gave that variable the current model's start value.
• New --config, --fixed-config, and --against-config flags. The agreed spec is never checked with the code model's config, and a missing config stops the run and lists the configs beside the spec.
• A rule the agreed config does not check reads "not checked" in the stories. Before, they said the agreed spec keeps it.
• When TLC finds a broken rule and then throws a Java exception, the run keeps the paths TLC printed, marks the rule broken, and warns that the charts can miss states.
• On a file system that cannot rename into the output folder (ENOSYS, EXDEV, or EISDIR, as on FUSE mounts), the run copies the files into place.
• The test of each TLC run's temp folder accepts Naturals.tla anywhere under it, where TLC 1.8.0 puts it.

cursor/plugins#776 also checks each rule with one worker per CPU and checks a broken rule again with one worker, which gives the shortest paths. Each PROPERTY gets its own TLC run, and --expect-broken accepts it. With --against, each story says whether a config beside the agreed spec expects the bug. With --fixed or --against, the run lists each condition of an action that no \* file:line comment ties to code. SKILL.md (+4 -4) asks for those citations, says what a valid replay is, and asks the hand-off to say whether the spec already lists each bug.

pstack #779 deletes statechart script comments that repeat the code. Where a comment held a fact, a helper's name now says it.

• splitComments becomes splitCommentsKeepingOffsets, and checkTlcOutput becomes tlcOutputWarning.
• quote becomes escapeMermaidQuotes, luminance becomes wcagRelativeLuminance, and parseMermaid's declared becomes declaredInRegion.
• cited takes { above } in place of a positional flag, and one exported PRIMES_OR_UNCHANGED regex replaces two copies of the same regex.

#779 touches lib.mjs, statechart.mjs, tlc-to-chart.mjs, and the test file, 44 lines in and 64 out. No file outside the skill uses a name it changes.

All of it is Lauren's code and byte-identical to upstream at 4ec7ffa. No substitution, fork, or hook changed.

Commits

1. Sync to 7698375 (#776). bun tools/sync.mjs moves each component's pin from eb4db2b to 7698375 and updates SKILL.md, lib.mjs, statechart.mjs, tlc-to-chart.mjs, and test/statechart.test.mjs cleanly. Each matched upstream's at 7698375 under cmp, file modes included. The 15 declared forks were left alone. cursor-team-kit and thermos synced with no file changes.
2. Release. VERSION and the manifests move to 2.0.0-rc.18. CHANGES gets the entry with its behavior-delta table. NOTICE, NOTICE-skills, poteto-mode's copy of the notice, and the README pointed at 7698375, and the README's pinned installer command names the new tag. The skill count stays at 65.
3. Sync to 4ec7ffa (#779). bun tools/sync.mjs moves each pin from 7698375 to 4ec7ffa and updates lib.mjs, statechart.mjs, tlc-to-chart.mjs, and the test file cleanly. diff -r finds the whole skill folder identical to upstream at 4ec7ffa, and each file's git mode matches upstream's. The 15 declared forks were left alone. cursor-team-kit and thermos synced with no file changes.
4. Release files to 4ec7ffa. The rc.18 CHANGES entry names 4ec7ffa in its title, links #779 beside #776, and says what #779 renames. NOTICE, NOTICE-skills, poteto-mode's copy of the notice, and the README's pin point at 4ec7ffa. The version stays 2.0.0-rc.18, and the behavior-delta table is unchanged because #779 changes no behavior.

On T3

Nothing T3-specific changes. The new flags and messages name no Cursor tool, .cursor/ path, model, or subagent, so no rule is needed, and #779 adds none. The scripts still find TLC only through TLA2TOOLS and JAVA, since cursor/plugins#776 left out its source's repo-pinned TLC install. The rc.17 limits still hold. Under Codex's workspace-write sandbox TLC cannot listen on its RMI port, and --png cannot reach the npm registry.

TLC 1.8.0 is a prerelease, and one gap remains with it. It words a broken temporal property as "Temporal property X was violated.", which the scripts do not read yet. So a broken temporal PROPERTY stops the run with "TLC stopped on an error that is not a broken rule", as cursor/plugins#776 reports. The "no TLC" message still points at 1.7.4, the latest stable release.

Checks at 4ec7ffa

These ran on this head.

• bun tools/sync.mjs <component> 4ec7ffa --dry-run for pstack, cursor-team-kit, and thermos after both new commits exits 0 for each, with no warning, no undeclared fork, no denylist hit, and no unmatched substitution. pstack reads 132 unchanged files and the same 15 declared forks with 551 changed lines as rc.17, and tools/forks.json is unchanged.
• bun tools/generate.mjs --check reports 17 generated files current and passes the hooks freeze check.
• GIT_CONFIG_GLOBAL=/dev/null bun test tests/ --timeout 30000 passes 550, skips 46, and fails 0.
• The skill's tests without TLC pass 29 and skip 38 on Node 24.22.1 on macOS.
• markdownlint 0.18.1 reports no error on the five changed Markdown files.
• t3-sheet.mjs against this machine's sheet and catalog reports that every role line parses and dispatches.
• git grep finds no use of checkTlcOutput, splitComments, quote(, or luminance( left anywhere in the repo.
• End to end. statechart.mjs from-spec scripts/model/OutputFolder.tla --map scripts/model/OutputFolder.map.mjs on the bundled model, with TLC 1.7.4 (TLC2 2.19) and Java 21.0.12.1 on macOS, finds that all five rules hold and prints "TLC ran 6 times in 4.5 s". It draws a 19-state chart in two parallel regions of 4 and 15 states from 4,294 model states, with 19 states that work and 0 that break a rule. It writes chart.mmd, stories.md, and summary.json and exits 0.

Checks at 7698375

These ran on 2d8b487, before #779 was folded in. #779 changes no behavior, and they were not rerun.

• The skill's tests without TLC passed 29 and skipped 38 on Node 20.20.2 on Linux.
• On Linux (Docker, Node 20.20.2, OpenJDK 17.0.20.1), with TLC 1.7.4, 66 of 67 passed and the PID-namespace test skipped because Docker blocks unprivileged unshare. With TLC 1.8.0, 65 passed, that test skipped, and the PROPERTY test failed on the wording above.
• On macOS (Java 21.0.12.1, Node 24.22.1) with TMPDIR set to its canonical /private/var path, TLC 1.7.4 passed 65, skipped 1, and failed 1. TLC 1.8.0 passed 64, skipped 1, and failed that test and the PROPERTY test. The failing test fails renames through LD_PRELOAD, which macOS ignores, as in rc.17, and it passes on Linux. With the default /var/folders TMPDIR, four more tests failed comparing temp paths and passed once TMPDIR was canonical.
• The Naturals.tla fix, shown on TLC 1.8.0. The test from rc.17 fails because TLC 1.8.0 parses Naturals.tla from tmp/tlc-<n>/Naturals.tla, one folder below the path it expects. The synced test passed.
• statechart.mjs from-spec OutputFolder.tla --png on a copy of the bundled model, with TLC 1.8.0 and Java 21, found that all five rules hold and drew the same 19-state chart. It wrote chart.mmd, chart.png, stories.md, and summary.json and exited 0. Its chart.mmd and summary.json were identical to what rc.17's scripts write on the same TLC.
• The new --config flag. With a config that lists two of the five rules, the run checked only those two in 3 TLC runs, drew the same chart, and exited 0. With a config that does not exist, it exited 2 with <dir>/Missing.cfg does not exist. Pass --config with the config to check OutputFolder.tla with. The configs beside it: OutputFolder.cfg, TwoRules.cfg. and wrote no output folder.

---

Note

Medium Risk
Changes TLC orchestration, spec-vs-code comparison semantics, and chart output for a formal-verification workflow; misconfiguration could still mislead PMs, though the release mostly replaces silent wrong charts with explicit stops and warnings.

Overview
Release 2.0.0-rc.18 bumps version manifests and pins all three synced components to Lauren Tan's cursor/plugins 4ec7ffa. Aside from notices and changelog, almost all code change is the upstream statechart skill (pstack #776 behavior fixes, #779 rename-only cleanup).

The from-spec / chart pipeline is stricter and more explicit when comparing code to an agreed spec or fix:

• --config, --fixed-config, and --against-config choose which TLC configs run; --against never uses the code model's config, and missing configs fail with a list of configs beside the spec.
• When a shared mapping reads a variable the --fixed / --against model lacks, the run stops instead of silently filling from the current model's initial state.
• Stories say "not checked" when the agreed config does not include a rule; with --against, they can also say whether a sibling config's \* expect: line already expects the bug.
• PROPERTY rules get separate TLC runs (charts still only color INVARIANT breaks); --expect-broken can target properties.
• TLC runs use parallel workers, then re-run broken invariants with one worker for shortest stable paths; if TLC throws after reporting a violation, paths are kept with a warning that charts may be incomplete.
• Uncited action conditions (no \* file:line on guards the code does not check) are warned and recorded in summary.json; SKILL.md tightens replay and hand-off guidance.
• Publishing falls back to copy when rename fails (FUSE / EXDEV / EISDIR); failed publishes can leave work in a named temp dir.

Helper renames only (#779): e.g. checkTlcOutput → tlcOutputWarning, quote → escapeMermaidQuotes.

^{Reviewed by Cursor Bugbot for commit 58f7119. Bugbot is set up for automated code reviews on this repo. Configure here.}