主要来源shao__meng
查看原文事件专题 ·单一信源
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。
当前结论
pstack 出了个 meta-skill，你说要验证啥，它就帮你生成 TLA+ 或 Kani 的验证方案，作者自己已经用它找到了几个 bug。
2 个信源41° AI 热度最后更新 2026/10/19 02:04:35
证据链
2 个信源相关来源 1宝玉
查看原文冲突核查
现有去重数据只说明这些来源讨论同一事件，不代表立场相同。当前没有结构化的支持或反驳证据，不自动推断冲突。