A method for catching bugs by having agents draw state diagrams and exhaustively searching with TLA+
English text is being prepared.
lauren shared a method for catching bugs with AI: first have the agent draw the code and user flows into a state diagram, then call the formal verification tool TLA+ to exhaustively search for violating paths. In the open source project pstack, she built a meta-skill that creates skills; users only need to define the rules that must always hold, and the AI will generate a verification suite and flag violating branches. The author believes this approach of first drawing state diagrams and then exhaustively searching according to baseline rules can also be applied to business processes such as cross-department approvals.
Why read this
AI score 65
The original article breaks formal verification into two steps: drawing state diagrams and exhaustive search following ironclad rules, and provides a reusable meta-skill approach that is easy to transfer to other processes.
Topics
View original postthere'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
View original
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
Body
核心动作就两步：先让智能体把代码和用户流程画成一张状态图，再调用形式化验证工具 TLA+ 去穷举抓 bug。
平时我们测试软件或者审阅代码，默认靠的是人脑想测试用例，但人类最不擅长的就是穷举多端并发的边缘状态，就拿她图里演示的聊天软件通知来说，用户在电脑上开着频道但没点开讨论串，结果回复被直接吞成已读，
或者手机明明已经看过了消息，兜里还在疯狂震动；甚至开了免打扰模式手机照样响，电脑从休眠醒来还在闪假未读，这些跨设备交织的奇葩组合，人工测试永远漏得像筛子，但真实用户上线第一天就一定会撞上。
她这套打法最聪明的地方，是把原本高不可攀的数学级形式化验证给平民化了，以前之所以没人愿意用 TLA+，是因为要把业务需求手写成严密的数学规格说明实在太折磨人，而且代码一改就得重写，
现在她在开源项目 pstack 里直接做了一个造技能的元技能，你只需要定好必须永远成立的铁律，比如开了免打扰就绝对不准震动，AI 就会自动替你画出状态图、生成验证套件，把所有可能的状态分支跑个底朝天，把违规的路径全部标红揪出来。
这就好比你修一座有上百个岔路口的地下迷宫，以前找死胡同全靠派几个测试员举着手电筒往里硬走，走十趟也摸不完所有偏僻角落，
说到底，这套先画状态图、再用铁律穷举的逻辑，根本不只属于程序员，咱们在公司里设计跨部门审批、入转调离交接或者奖金核算流程时，最容易出乱子的也永远是边缘情况撞车，
比如员工休假当天恰好触发跨级审批、转岗交接期还在跑旧部门权限，与其出了事故开十场复盘会扯皮，不如先让 AI 把业务制度画成状态图，再拿底线规则一条条去撞，图画不出来的地方，就是你制度没想明白的漏洞。