用 pstack 技能将状态图转为 TLA+ 验证

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。 试试看，并告诉我效果如何！

查看原文

pstack v0.15.27 ships with a new skill /create-formal-verification-skill! it's still in beta, and similar to /create-verification-skill, this is a meta-skill that creates a new skill and formal verification suite based on the characteristics you want to verify. for example, you may want to model state machines and systems with concurrency using TLA+, or use kani in rust to check for undefined behavior. if you're new to formal verification, think of it as mathematically proving properties and invariants (something that must always be true) or "laws" of your system. usually, this means modeling your programs in a separate language like with TLA+ and then running the solver on that spec. newer approaches like with kani and @bendlang take a different approach where there is no separate language: you write kani in rust, and bend in bend (it's also a programming language, and the proofs are written as laws and expressed in its type system). historically formal verification never reached mainstream status because of the difficulty in modeling and writing proofs. it's quite difficult to model your business requirements and keep them in sync! but i expect that we will see more innovation in formal verification in the future as being able to formally verifiy that the code does what you intended gives your agents superpowers in writing correct software. in the meantime though, i've been experimenting with modeling our code with TLA+ and have already found several bugs with the skill created by /create-formal-verification-skill. try it out and let me know how it goes!