pstack 新增了一个 skill /create-formal-verification-skill 定位是 meta-skill：不直接帮你做形式化验证，而根据你想验证的系统特性，自动生成一个定制的验证 skill 和配套验证套件。比如你要验证状态机和并发行为的正确性，它会生成基于 TLA+ 的方案；要排查 Rust 代码的未定义行为，则生成基于 Kani 的方案。 Grok Bot 插件安装： https://x.ai/bot/plugin/9717366 背后的概念：形式化验证 测试只能证明 “bug 存在”，无法证明 “没有 bug”；形式化验证则是对系统的性质做数学证明：证明某个不变量 (即“必须永远为真”的性质或“定律”) 在所有可能的情况下都成立。 poteto 点出了两条技术路线的分别： · 传统路线(外置建模)：用一门独立的规范语言 (如 TLA+) 给系统建模，再运行求解器/模型检查器去穷举状态空间验证规范。代码和证明是两套东西。 · 新路线 (同语言证明)：Kani 直接写在 Rust 里，Bend 的证明以 laws 的形式表达在其类型系统中；没有单独的建模语言，证明和代码活在同一处。 形式化验证是个 “理论很美、实践从未进入主流” 的领域，poteto 指出了两个历史原因：建模本身很难 (把业务需求抽象成形式化模型是专业 skill)，以及规范与实现难以同步 (需求一变，两份东西都要改)。 她的判断是：这两个瓶颈恰好是 LLM 擅长接管的，让 agent 承担建模和同步的苦活。而反过来，形式化验证给 agent 提供的是传统测试给不了的强反馈：“数学上不可能违反”，这对让 AI 写出正确的软件是质的提升，她称之为“超能力”。