TLAPS-Bench 发布：真实系统 TLA+ 规范成为前沿 AI 形式化证明难题

加州大学研究者 tianyinxu 宣布将在 Frontier Data Summit 介绍 TLAPS-Bench，一个面向前沿 AI 的长程形式化证明基准。该基准基于真实系统与协议的 TLA+ 规范，用 TLA+ Proof System 形式化证明正确性，目前前沿模型仍难以自主完成。项目由 TLA+ 基金会、Specula 团队及合作者完成，提供可扩展、可复用的基准套件。