pstack v0.15.27 推出 meta-skill /create-formal-verification-skill

pstack v0.15.27 新增 skill /create-formal-verification-skill，目前处于 beta 阶段。它是一个 meta-skill，根据要验证的系统特性自动生成定制的验证 skill 和配套套件：验证状态机与并发行为时生成基于 TLA+ 的方案，排查 Rust 未定义行为时生成基于 Kani 的方案。poteto 指出形式化验证未成主流的两个原因是建模困难和规范与实现难同步，而这正是 LLM 能承担的部分。她已经用该 skill 生成的方案建模自己的代码，发现了几个 bug。