AI 写代码的速度越快，你越需要一套能证明代码真的没埋雷的硬本事，
硅谷开发女神lauren 刚分享了一套用 AI 降维抓虫的硬核打法，

核心动作就两步：先让智能体把代码和用户流程画成一张状态图，再调用形式化验证工具 TLA+ 去穷举抓 bug。

平时我们测试软件或者审阅代码，默认靠的是人脑想测试用例，但人类最不擅长的就是穷举多端并发的边缘状态，就拿她图里演示的聊天软件通知来说，用户在电脑上开着频道但没点开讨论串，结果回复被直接吞成已读，

或者手机明明已经看过了消息，兜里还在疯狂震动；甚至开了免打扰模式手机照样响，电脑从休眠醒来还在闪假未读，这些跨设备交织的奇葩组合，人工测试永远漏得像筛子，但真实用户上线第一天就一定会撞上。

她这套打法最聪明的地方，是把原本高不可攀的数学级形式化验证给平民化了，以前之所以没人愿意用 TLA+，是因为要把业务需求手写成严密的数学规格说明实在太折磨人，而且代码一改就得重写，

现在她在开源项目 pstack 里直接做了一个造技能的元技能，你只需要定好必须永远成立的铁律，比如开了免打扰就绝对不准震动，AI 就会自动替你画出状态图、生成验证套件，把所有可能的状态分支跑个底朝天，把违规的路径全部标红揪出来。

这就好比你修一座有上百个岔路口的地下迷宫，以前找死胡同全靠派几个测试员举着手电筒往里硬走，走十趟也摸不完所有偏僻角落，

现在是让 AI 先在空中画出整座迷宫的俯视蓝图，再直接往入口灌满高压水，哪条暗道漏水、哪个阀门锁死，一眼就能在图纸上抓个正着。

说到底，这套先画状态图、再用铁律穷举的逻辑，根本不只属于程序员，咱们在公司里设计跨部门审批、入转调离交接或者奖金核算流程时，最容易出乱子的也永远是边缘情况撞车，

比如员工休假当天恰好触发跨级审批、转岗交接期还在跑旧部门权限，与其出了事故开十场复盘会扯皮，不如先让 AI 把业务制度画成状态图，再拿底线规则一条条去撞，图画不出来的地方，就是你制度没想明白的漏洞。