Reasonable 团队解读 TLA+：从 Boris Cherny 热传推文到机器可验证软件

Reasonable 团队撰文介绍 TLA+ 是什么，回应 Boris Cherny 用 Opus 5.5 将 Claude Agent SDK 部分建模为 TLA+ 和 Lean 的热传推文。