poteto@poteto

aunque le tengo bastante fe a los métodos formales, creo que vale la pena bajar un poco las expectativas e investigar por tu cuenta (aclaración: no soy experta en el tema). no pueden garantizar que tu código no tenga bugs, solo que coincide con la spec bajo ciertos supuestos, y las specs salen de lo que la gente quiere, no de las matemáticas. mientras hagamos software para humanos, nada puede probar que tu spec es correcta, solo tú puedes juzgarlo. creé la skill /statechart en pstack principalmente porque ayuda a que las máquinas de estado implícitas en tu código sean más obvias y legibles para ti, así puedes reducir la superficie de revisión y revisar el trabajo a un nivel más alto: ¿de verdad coincide con tu intención y tu objetivo? usé muchísimo esta skill mientras hacía mi juego tibo.dog, abajo pueden ver el statechart del modo historia, con el que pude encontrar muchos bugs. en ese sentido, creo que el model checking (p. ej. TLA+ con TLC) es bastante útil para entender y verificar propiedades de tu sistema e2e, y no tienes que escribir toneladas de código de verificación nuevo. la spec no es tu código real, así que siempre hay riesgo de que se desfasen, pero hasta ahora me ha ido bien encontrando bugs reales con eso. suelo combinarlo también con verificación empírica (correr el código) para confirmar que son reales otros tipos de verificación formal como demostrar teoremas (p. ej. Lean, Dafny), bounded model checking (p. ej. CBMC, Kani), etc. tienen sus propios tradeoffs. las demostraciones cubren todas las entradas posibles, pero solo para las propiedades especificadas, y requieren mucho más código/trabajo. el bounded model checking puede correr sobre tu código real, lo que evita el desfase, pero solo revisa hasta cierto número de pasos, así que sirve más para encontrar bugs que para probar que no los hay así que creo que a corto-mediano plazo todavía vas a tener que armar tu codebase por capas: restricciones y guardrails (tipos, reglas de lint, diseño de api, refactorización), verificación empírica (tests, evals, uso real) y verificación formal para las partes que de verdad lo necesitan. ninguna atrapa todo por sí sola, pero en capas atrapan mucho más y reducen lo que te queda por revisar pero quizás en el límite la bitter lesson gane y el código perfecto simplemente salga impreso sin bugs cada vez. incluso en ese escenario, /statechart igual parece muy útil para confirmar que el agente entendió bien tu intención. ¡pruébala si todavía no lo has hecho!

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