先让 TLC 跑一遍，再让 AI 写代码：用 TLA+ 约束 AI 实现分布式服务
AI 写的分布式代码总在迟到写入、租约过期、滚动发布这些地方出错，测试一轮轮补也补不完。改成先写 TLA+ 规约、用 TLC 穷举，再让 AI 按动作一比一实现、用状态机 fuzz 对照之后，问题终于收敛了。文中附一个开源的完整示例，每个结论都可以自己跑出来。
这个标签下共有 2 篇文章。
AI 写的分布式代码总在迟到写入、租约过期、滚动发布这些地方出错，测试一轮轮补也补不完。改成先写 TLA+ 规约、用 TLC 穷举，再让 AI 按动作一比一实现、用状态机 fuzz 对照之后，问题终于收敛了。文中附一个开源的完整示例，每个结论都可以自己跑出来。
AI-written distributed code keeps breaking on late writes, expired leases and rolling deploys, and more tests never seem to converge. Writing a TLA+ spec first, checking it exhaustively with TLC, having the AI implement it action by action and cross-checking with state-machine fuzzing finally made the bugs converge. Comes with an open-source example where every claim can be reproduced.