TLAPS-Bench：用 AI 智能体为 TLA+ 系统规范构建机器可验证证明的基准

TLAPS-Bench 是面向 TLA+ 规范、用 AI 智能体构建机器可验证证明的基准与执行框架，包含来自 95 个真实系统规范的 265 个证明目标。研究用 Codex 搭配 GPT 模型在 12 个规范的 70 个目标上评测前沿智能体，最高分的 GPT-6.1 Sol (max) 证明了 31 个目标（44.3%）。