用智能体画状态图配合 TLA+ 穷举抓 bug 的方法
AI 写代码的速度越快，你越需要一套能证明代码真的没埋雷的硬本事，
lauren 分享了一套用 AI 抓 bug 的做法：先让智能体把代码和用户流程画成状态图，再调用形式化验证工具 TLA+ 穷举违规路径。她在开源项目 pstack 里做了一个造技能的元技能，用户只需定好必须永远成立的规则，AI 就会生成验证套件并标出违规分支。作者认为这套先画状态图再按底线规则穷举的思路也可用于跨部门审批等业务流程。
查看原帖让智能体画一张状态图（本图中的假设示例），然后用你借助 pstack 制作的 /create-formal-verification-skill，通过类似 TLA+ 的方式找出 bug，这件事真的很酷。你既能更好地理解自己的代码，也能弄清用户流程应当如何运作，还能修复用户原本会遇到的问题。
查看原文
there's something really cool about asking your agent to draw a statechart (hypothetical example in this image), then using the /create-formal-verification-skill you made with pstack to find bugs through something like TLA+. you can both understand your code better and how the user flow should work, and fix issues users would otherwise see
正文
核心动作就两步：先让智能体把代码和用户流程画成一张状态图，再调用形式化验证工具 TLA+ 去穷举抓 bug。
平时我们测试软件或者审阅代码，默认靠的是人脑想测试用例，但人类最不擅长的就是穷举多端并发的边缘状态，就拿她图里演示的聊天软件通知来说，用户在电脑上开着频道但没点开讨论串，结果回复被直接吞成已读，
或者手机明明已经看过了消息，兜里还在疯狂震动；甚至开了免打扰模式手机照样响，电脑从休眠醒来还在闪假未读，这些跨设备交织的奇葩组合，人工测试永远漏得像筛子，但真实用户上线第一天就一定会撞上。
她这套打法最聪明的地方，是把原本高不可攀的数学级形式化验证给平民化了，以前之所以没人愿意用 TLA+，是因为要把业务需求手写成严密的数学规格说明实在太折磨人，而且代码一改就得重写，
现在她在开源项目 pstack 里直接做了一个造技能的元技能，你只需要定好必须永远成立的铁律，比如开了免打扰就绝对不准震动，AI 就会自动替你画出状态图、生成验证套件，把所有可能的状态分支跑个底朝天，把违规的路径全部标红揪出来。
这就好比你修一座有上百个岔路口的地下迷宫，以前找死胡同全靠派几个测试员举着手电筒往里硬走，走十趟也摸不完所有偏僻角落，
说到底，这套先画状态图、再用铁律穷举的逻辑，根本不只属于程序员，咱们在公司里设计跨部门审批、入转调离交接或者奖金核算流程时，最容易出乱子的也永远是边缘情况撞车，
比如员工休假当天恰好触发跨级审批、转岗交接期还在跑旧部门权限，与其出了事故开十场复盘会扯皮，不如先让 AI 把业务制度画成状态图，再拿底线规则一条条去撞，图画不出来的地方，就是你制度没想明白的漏洞。