Veil 2.0 发布，用 Lean 4 验证协议
热点事件持续更新
Veil 2.0 发布，用 Lean 4 验证协议
1 篇报道1 个报道来源6 小时前更新
先了解这件事
AI 综述
Ilya Sergey 团队发布 Veil 2.0 形式化验证框架，以 Lean 4 规约、模型检验并证明分布式协议和状态转移系统的安全性与活性。团队称，新模型检查器的安全性检查速度比 TLC 快 2 至 20 倍，并支持 LTL 活性证明模式。 框架还提供 TLA+ 转 Veil 的 LLM skill、PlusCal 风格 DSL、CTI 不变式发现器及自动综合工具 UPDR；配套网站设有 Playground 和 GitHub 仓库，相关工具由 @zqy1018 及外部贡献者完成。
AI 根据报道生成 · 6 小时前更新
最新进展11月7日 07:48
Ilya Sergey 团队发布 Veil 2.0：用 Lean 4 验证分布式协议报道时间线
沿着报道，了解事件的不同侧面。
11月7日
- AGI HuntIlya Sergey 团队发布 Veil 2.0：用 Lean 4 验证分布式协议
Ilya Sergey 团队发布形式化验证框架 Veil 2.0，用于在 Lean 4 中规约、模型检验并证明分布式协议与状态转移系统的安全性与活性。新增模型检查器的安全性检查比 TLC 快 2–20 倍，并支持 LTL 活性证明模式；另提供 TLA+ → Veil 的 LLM skill、PlusCal 风格 DSL、CTI 不变式发现器和自动综合工具 UPDR。
本事件热度走势
- 可比范围当前
- 9
- 可比范围峰值
- 1011月7日 08:00
- 近 24 小时变化
- –
02.557.510
08:0009:0010:0011:0012:0013:00
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。