poteto@poteto

形式手法にはかなり期待してるけど、期待値はちょっと抑えて自分で調べてみるのがいいと思う（免責：私は専門家じゃないです）。形式手法はコードにバグがないことを保証できるわけじゃなくて、ある前提のもとでコードが spec に合ってることを保証するだけ。で、spec は数学じゃなくて人が何を求めてるかから来る。人間のためにソフトウェアを作ってる限り、spec が正しいって証明できるものは何もなくて、判断できるのは自分だけ。 pstack に /statechart スキルを作ったのは、主にコードに暗黙的にある状態機械をもっとはっきり、読みやすくしてくれるから。そうするとレビューする範囲を小さくして、もっと高いレベルでレビューできる：ほんとに自分の意図とゴールに合ってる？ ゲームの tibo.dog を作ってるときにこのスキルをめちゃくちゃ使ってて、下のはストーリーモードの statechart。これでバグをたくさん見つけられた。 その意味で、モデル検査（例えば TLA+ と TLC）はシステムの性質を e2e で理解・チェックするのにかなり便利だと思うし、新しい検証コードを大量に書かなくていい。spec は実際のコードじゃないから常にズレるリスクはあるけど、今のところ実際のバグを見つけられていい感じ。本物か確かめるために、経験的な検証（コードを実際に動かす）とも組み合わせることが多い。 定理証明（Lean、Dafny とか）や有界モデル検査（CBMC、Kani とか）みたいな他の形式検証にもそれぞれトレードオフがある。証明はあらゆる入力をカバーするけど、指定した性質についてだけで、コードも手間もずっと多くかかる。有界モデル検査は実際のコードに対して走らせられるからズレは避けられるけど、一定のステップ数までしかチェックしないから、バグがないことを証明するよりバグを見つけるほうが得意。 だから近〜中期的には、まだコードベースを層にする必要があると思う：制約とガードレール（型、lint ルール、API 設計、リファクタリング）、経験的な検証（テスト、evals、実際の利用）、そして本当に必要な部分には形式検証。どれも単体では全部は拾えないけど、重ねればずっと多く拾えて、自分がレビューする部分も減らせる。 でも極限では bitter lesson が勝って、毎回バグゼロの完璧なコードがそのまま出てくるのかもね。そのシナリオでも、エージェントが自分の意図をちゃんと理解したか確認するのに /statechart はやっぱりすごく役立ちそう。まだなら試してみて！

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