TLA-Verus:用 LLM 智能体自动证明 TLA+ 规约的时序性质
tianyin_xu · x · 2026-11-02
NeurIPS'26 workshop 论文 TLA-Verus:从 GitHub 抓取 TLA+ 规约,翻译成 Verus,再让 LLM 智能体证明其中的安全性与活性性质。动机是 TLA+ 的两大痛点:规约与代码脱节、证明支持薄弱(TLC 只能查小规模配置,TLAPS 活性证明弱)。
博主 muratdemirbas 提出尖锐批评:
- 论文开局即放弃解决第一个问题——TLA+ 与生成的 Rust 代码间没有细化证明,且 TLA-Verus 根本不生成代码;连 TLA+ 与 Verus 规约之间也没有任何细化证明,无法保证翻译后的语义与原意一致。
- 论文低估了 TLAPS 做时序证明的能力:用 BY PTL 可将步骤交给 LTL 决策程序 LS4,coalescing 技术可将一阶义务抽象为命题原子,Lamport 的时序规则(含把弱公平性转为 leads-to 的 WF1)都在;真正短板是对 ENABLED 的推理能力弱。
「编程与Agent」频道最新
- Agent 操刀 Final Cut Pro，自动剪完一支音乐视频 — ZeroStateReflex · 2026-11-02
- Zed CEO 晒用 Codex 做的派对平台跳跃游戏 SLAG，支持 1-8 人 — zeeg · 2026-11-02
- 省 Grok 用量技巧：让机器人写脚本定时跑，别天天重复提问 — nima_owji · 2026-11-02
- mnemos v2 MCP 将发布：浏览器内实时看 Agent 记忆形成全过程 — RileyRalmuto · 2026-11-02
- Supabase 推出 Compute 私测:Agent 与长任务可直接跑在 Postgres 旁 — dshukertjr · 2026-11-02
- ChatGPT Sites 五大玩法：自带数据库、MCP 托管与自定义域名 — gabrielchua · 2026-11-02