What TLA+ can and can't check

作者讨论TLA+形式化验证的能力边界，针对“TLA+将拯救AI”的热潮降温。文中提到Claude Code发明人Boris Cherny称Opus能用TLA+发现竞态条件，但作者强调需冷静看待其适用范围。