北京
pstack 更新到 v0.15.27，带了一个新技能：/create-formal-verification-skill。目前还在 beta 阶段。
它和 /create-verification-skill 是同一路数——一个元技能，根据你想验证的特性，生成一套新的技能加形式化验证套件。想用 TLA+ 给状态机和并发系统建模，可以；想在 Rust 里用 kani 查未定义行为，也可以。
对没接触过形式化验证的人，可以这么理解：用数学方法证明系统的属性和不变量，也就是那些必须永远为真的东西，或者叫系统的"定律"。
常规做法是把程序建模到另一门语言里，比如 TLA+，再拿求解器去跑这份规格。新一些的路子不一样，kani 和 bend 就不需要单独的语言——kani 直接写在 Rust 里，bend 写在 bend 里（bend 本身也是一门编程语言，证明以定律的形式写出来，放在它的类型系统里表达）。
形式化验证一直没进主流，原因很直接：建模和写证明太难了。把业务需求建模出来，还要让它和代码保持同步，这件事本身就够呛。
但作者押了一个方向：未来形式化验证会看到更多创新。理由是，如果能形式化地验证代码确实做了你想让它做的事，那你的 agent 在写正确软件这件事上就等于开了挂。
眼下他自己已经在拿 TLA+ 给代码建模做实验，用 /create-formal-verification-skill 生成的技能，已经找出了好几个 bug。
这条更新发布于 10 月 18 日晚上 9:05，浏览量 1,081。作者在末尾招呼大家试用，并反馈效果。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
