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