AI代码能证明不会出错，却证明不了游戏存在赢法

形式化验证专家 Hillel Wayne 深入探讨了利用 TLA+ 等工具验证 AI 生成代码的边界与局限。TLA+ 擅长通过状态序列检查并发系统中的 “安全性质”（坏事不会发生）与 “活性性质”（好事最终发生），能有效识别竞态条件。然而，诸如撤销操作后的状态恢复、省电模式下的功耗对比等涉及跨多条执行路径比较的 “超性质”（hyperproperty），以及统计学承诺和基本的可达性要求，均无法直接转化为 TLA+ 的标准检查性质。虽然可以通过增加状态历史或自我组合等手段绕开限制，但会带来状态空间膨胀和模型失真的代价。开发者必须意识到，形式化验证的有效性取决于能否将期望行为准确定义为工具可识别的逻辑，AI 虽能加速找错，但界定验证范围与评估设计实现的一致性仍需依赖严谨的工程判断。