pstack 的 /statechart 稳定了：画状态机，顺手跑 mini TLC 找 bug

pstack v0.15.36 的 /statechart skill 进入稳定版。画状态机只是表面。它内部塞了一个 mini TLC 编译器：解析、降级到一个小 IR，再由后端输出 mmd 语法。配合 /create-formal-verification-skill，可以把状态机和分布式系统抽象建模，用来找 bug。lauren 在推文里说，她刚用它找到两个真 bug。推文附了 /statechart skill 的图表。

用法不复杂。让 agent 按你喜欢的风格生成图表，skill 会提示走 Pele。Pele 是 Obsidian 开源的一个轻量库，把 Mermaid 语法渲染成 SVG，用 CSS 变量做主题，改颜色不用重新渲染。官方给的数据：gzip 后 230 kB，对 Mermaid.js 的 1.6 MB；渲染 0.05 到 0.3 ms，对 6 到 82 ms；直接依赖 0 个，对 23 个；小屏上它会调整布局，Mermaid.js 是缩放整张图。它支持 Mermaid 12.1.0 内置的图表类型。想要蓝图、手绘百科插图这类风格，可以自己调主题。

这条推文下面，讨论很快拐到 TLA-ts。TLC 是 TLA+ 生态里的模型检查器，过去跑在 JVM 里。Aiden Bai 发了 TLA-ts，一个 100% TypeScript 写的 TLC 替代品，号称 2 倍快，能跑在浏览器里。有人追问状态指纹和对称约简怎么处理，有人问 2 倍是快在大状态空间，还是快在 JVM 启动这种小规格场景。lauren 回复说会看看支持 tla-ts。

也有人泼冷水。ShadowAguy 说 mini TLC 编译器挺好，直到状态空间爆炸找上门。Baron 问 Windows 上有没有 POSIX 问题。Marcell 问能不能用在 bot routines 上。这些反馈比发布会本身有用。形式化验证喊了多年，卡住人的常常不是 TLA+ 语法，是跑 TLC 之前那串环境摩擦：JVM、日志、和各种 agent 沙箱的集成。把模型检查塞进 skill，让跑一次检查接近生成一张图，摩擦就降了一截。

回复区有人直接甩了个视频。

还有人贴图捧场。

别急着把所有流程图都换成状态机。先拿并发逻辑、重试、取消、分布式锁这类地方试。工具的价值是让跑一下模型检查变得顺手，不是让每个人都变成形式化方法专家。有人已经在回复区道谢并贴图，剩下的就看 Windows 和状态空间爆炸什么时候被解决。