pstack v0.15.27 新增形式化验证技能

pstack v0.15.27 附带了一个新技能 /create-formal-verification-skill！

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

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

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

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

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