为什么加入 Antithesis？形式化方法与模拟测试的取舍

Antithesis 通过确定性模拟让测试可控地探索并发交错，解决传统测试无法控制系统调度、难以复现竞态的问题。文中用 C++ 双线程计数器示例说明：同一竞态 bug 在 600 万次普通测试中仅出现 8 次，而 TLA+ 模型检查器能直接找出该状态空间。作者认为形式化验证、抽象建模与测试各有取舍，Antithesis 只解决测试不可靠这一项。