Ilya 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。