tla-skill：让编码智能体用 TLA+ 和 ts-tla 验证并优化软件

tla-skill 是一个面向编码智能体的技能，教智能体用 TLA+ 为整个程序建模，把每个规格放在对应代码旁，并在每次构建时用 tla-ts 检查。它要求每个有状态组件都有规格或书面说明，并通过变异体证明每个检查、锁和信号确有必要。该技能支持 Claude Code 插件和 Cursor，需要 Node 20 或 Bun，不需要 Java 或 TLC。