# TLA+

TLA+在AI代码验证中的能力与局限

Claude Code发明者称Opus可用TLA+检测竞态条件。该工具擅长验证安全性与活性属性，但“正确规范”不等于“正确实现”，且难以直接表达所有系统特性，需理性看待其能力边界。