pstack 新增元技能：让 Agent 画状态图再用 TLA+ 形式化验证找 bug
DavidKPiano · x · 2026-10-21
pstack 发布 v0.15.27，带来新的 /create-formal-verification-skill 元技能（beta）：它会根据你想验证的系统特性，自动生成一个新技能和形式化验证套件——比如用 TLA+ 为状态机和并发系统建模，或用 Rust 的 kani 检查未定义行为。
配套的实践流程是：先让编码 agent 画出系统的状态图（配图示例为一个聊天通知系统的状态机，标出了 bug 与修复后的分支），再用形式化验证（数学化证明系统的不变量）去发现用户实际会踩到的边界 bug。作者认为这样既能更好理解代码和用户流程，也能提前修掉线上问题。
「编程与Agent」频道最新
- OmniGraph 开源：给 AI Agent 记忆装上 Git 式分支与合并 — techNmak · 2026-10-21
- 2x5090 本地跑 Qwen3.8 做 agent 编程，vLLM 成唯一不炸缓存的方案 — TooManyPascals · 2026-10-21
- Hermes Agent 游戏插件:一句话生成精灵图、音乐、3D 并试玩抓崩溃 — Teknium · 2026-10-21
- 每周都有新 AI 工具？用一个网关统一授权免去反复重连 — verrsane · 2026-10-21
- 官方不出 GUI，Pi 编程 Agent 社区自建四款图形界面 — solyarisoftware · 2026-10-21
- 借 AI 两天把 Laravel 应用从 5.8 一路升到 11，作者称此前难以想象 — hermanschutte · 2026-10-21