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