跳至正文返回首页pstack 新增形式化验证 meta-skill：按系统特性自动生成 TLA+ 或 Kani 验证方案
- 核心发布：pstack v0.15.27 新增
/create-formal-verification-skill，定位为 meta-skill——不直接做形式化验证，而是根据用户想验证的系统特性，自动生成定制的验证 skill 与配套验证套件。例如验证状态机和并发行为时生成基于 TLA+ 的方案，排查 Rust 未定义行为时生成基于 Kani 的方案。
- 技术路线区分：传统路线用独立规范语言（如 TLA+）给系统建模，再运行求解器穷举状态空间，代码与证明是两套东西；新路线如同语言证明——Kani 直接写在 Rust 里，Bend 的证明以 laws 形式表达在其类型系统中，没有单独的建模语言，证明与代码活在同一处。
- 问题与机会：形式化验证长期“理论很美、实践未进主流”，两个历史瓶颈是建模难、规范与实现难同步。pstack 作者 poteto 的判断是，这两项苦活恰好可由 LLM 接管；而形式化验证反过来给 agent 提供传统测试给不了的强反馈——“数学上不可能违反”，对让 AI 写出正确软件是质的提升。
- 初步验证：poteto 表示已用该 skill 以 TLA+ 建模自家代码，并发现若干 bug。
- 行业观察：把形式化验证封装为按需生成的 agent 技能，意味着验证门槛从“掌握 TLA+ 或 Kani”下移到“描述要验证什么”。若生成质量稳定，代码审查与测试之外将多出一层可自动运行的数学证明检查；但其实际收益仍取决于生成方案是否贴合系统语义，以及验证成本能否压到日常开发可承受的范围。
🔗 原推文 | poteto 原帖
