形式化验证框架 Veil 2.0 发布：用 Lean 4 验证分布式协议
tianyin_xu · x · 2026-11-07
Ilya Sergey 团队发布形式化验证框架 Veil 2.0,用于在 Lean 4 中规约、模型检验并证明分布式协议与状态转移系统的安全性和活性。
主要更新:
- 新增经验证的模型检查器:安全性检查比 TLC 快 2–20 倍,并支持活性(LTL)证明模式
- 提供 TLA+ → Veil 的 LLM skill,方便 AI 编码代理迁移现有规约;支持 PlusCal 风格的 DSL
- 内置反例到归纳(CTI)不变式发现器与自动综合工具 UPDR,可在 Lean InfoView 中直接可视化执行轨迹与反例
配套网站提供 Playground 与 GitHub 仓库,由 @zqy1018 及外部贡献者完成。
「编程与Agent」频道最新
- Claude Code Projects 分阶段开放，Pro/Max/Ultra 可排队申请 — lydiahallie · 2026-11-07
- Anthropic 推出 Claude Code Projects，可接管 Conductor 工作流 — lydiahallie · 2026-11-07
- Anthropic 发文详解：让 Claude 通过「做梦」整理记忆 — round · 2026-11-07
- Seroter 每日精选：agent 冲突防护、企业 AI 现状与 Cursor 部署之战 — rseroter · 2026-11-07
- 用户实测：Amp Code 用了 48 小时后感觉已胜过 Conductor — HankYeomans · 2026-11-07
- 开发者用 Claude Code 搭「PR 工厂」：自动向记者 pitch 数据换曝光 — doooyle · 2026-11-07