pstack v0.15.27 新增形式化验证技能 /create-formal-verification-skill

lauren· @poteto · X·2026-10-19 05:05· 1 小时前AI 评分44

AI 导读

pstack v0.15.27 发布新技能 /create-formal-verification-skill，目前仍处 beta。该元技能可根据想验证的特性生成新技能与形式化验证套件，例如用 TLA+ 建模状态机与并发系统，或用 Rust 的 kani 检查未定义行为。作者用它以 TLA+ 建模自家代码，已发现多个 bug。

正文 · 原文

pstack v0.15.27 发布了新技能 /create-formal-verification-skill！

它仍处于 beta 阶段，与 /create-verification-skill 类似，这是一个元技能，会根据你想验证的特性创建一个新技能和形式化验证套件。例如，你可能想用 TLA+ 对状态机和并发系统建模，或用 Rust 中的 kani 检查未定义行为。

如果你对形式化验证不熟悉，可以把它理解为用数学方法证明系统的属性和不变量（必须始终为真的东西）或“定律”。通常，这意味着用 TLA+ 这样的独立语言对你的程序建模，然后对该规约运行求解器。较新的方法如 kani 和 @bendlang 采用了不同的思路，没有独立语言：你在 Rust 中写 kani，在 bend 中写 bend（它也是一种编程语言，证明以定律形式编写并表达在其类型系统中）。

历史上形式化验证从未成为主流，因为建模和编写证明非常困难。将业务需求建模并保持同步相当困难！但我预计未来形式化验证会出现更多创新，因为能够形式化验证代码是否按你的意图执行，会让你的智能体在编写正确软件方面获得超能力。

不过与此同时，我一直在尝试用 TLA+ 对我们的代码建模，并且已经通过 /create-formal-verification-skill 创建的技能发现了几个 bug。

试试看，并告诉我效果如何！

来源：lauren · x.com