poteto@poteto

虽然我挺看好形式化方法的，但我觉得还是值得降低一下预期，自己去研究研究（免责声明：我不是这方面的专家）。它没法保证你的代码没有 bug，只能保证在某些假设下代码符合 spec，而 spec 来自人们想要什么，不是来自数学。只要我们还在为人类写软件，就没有什么能证明你的 spec 是对的，只有你自己能判断。 我在 pstack 里做 /statechart 这个 skill，主要是因为它能让你代码里隐含的状态机变得更明显、更好读，这样你就能缩小 review 的范围，在更高的层面去审：它到底符不符合你的意图和目标？我做游戏 tibo.dog 的时候狂用这个 skill，下面是故事模式的 statechart，我靠它找出了好多 bug。 从这个角度看，我觉得模型检测（比如 TLA+ 配 TLC）对端到端理解和检查系统的属性挺有用的，而且你不用写一大堆新的验证代码。spec 不是你真正的代码，所以总有漂移的风险，但到目前为止我用它找到真 bug 的体验都还不错。我一般也会配合经验验证（实际跑代码）来确认 bug 是真的。 其他类型的形式化验证，比如定理证明（如 Lean、Dafny）、有界模型检测（如 CBMC、Kani）等，各有各的取舍。证明能覆盖所有可能的输入，但只针对你写明的属性，而且要多写很多代码、多花很多功夫。有界模型检测可以直接跑在你真正的代码上，避免了漂移，但它只检查到一定步数，所以更擅长找 bug，而不是证明没有 bug。 所以我觉得在近中期，你还是得给代码库分层：约束和护栏（类型、lint 规则、API 设计、重构）、经验验证（测试、evals、真实使用），以及对真正需要的部分做形式化验证。单靠哪一个都抓不全，但叠在一起能抓到多得多的问题，也能缩小留给你 review 的部分。 不过也许到了极限，bitter lesson 会胜出，每次都能完美地打印出零 bug 的代码。就算是那样，/statechart 在确认 agent 有没有正确理解你的意图这件事上，看起来还是很有用。还没试过的话就去试试吧！

while i'm quite bullish on formal methods, i think it's worth tempering expectations and doing your own research on it (disclaimer: i am not an expert in it). it cannot guarantee your code is bug free, only that it matches the spec under certain assumptions, and the specs come from what people want, not math. as long as we build software for humans, nothing can prove that your spec is right, only you can judge. i created the /statechart skill in pstack primarily because it helps make the state machines implicit in your code more obvious and legible to you, so you can shrink the review surface and review the work at a higher level: does it actually match your intent and goal? i used this skill a ton while building my game http://tibo.dog, below you can see the statechart for story mode where i was able to find many bugs with it. in that sense, i think model checking (eg TLA+ with TLC) is quite useful for understanding and checking properties of your system e2e, and you don't have to write tons of new verification code for it. the spec isn't your actual code so there's always a risk of drift, but so far i've had good experiences finding actual bugs with it. i tend to pair it with empirical verification (running the code) also to confirm it's real other types of formal verification like proving theorems (eg Lean, Dafny), bounded model checking (eg CBMC, Kani) etc have their own tradeoffs. proofs cover every possible input, but only for the properties specified, and it takes a lot more code/work. bounded model checking can run on your actual code, which avoids drift, but it only checks up to a certain number of steps, so it's better at finding bugs than proving there aren't any so i think in the near-medium term you'll still need to layer your codebase: constraints and guardrails (types, lint rules, api design, refactoring), empirical verification (tests, evals, real usage), and formal verification for the parts that really need it. none of these catch everything on their own, but layered together, they catch a lot more and shrink what's left for you to review but also maybe in the limit, the bitter lesson will prevail and flawless code will just be printed out perfectly every time with no bugs. even in that scenario, /statechart still seems very helpful in confirming that the agent understood your intent correctly. give it a try if you haven't already! https://github.com/cursor/plugins/tree/main/pstack/skills/statechart