工程师用 AI 造并发测试工具:无规约语言也能抓真 bug

cto_junior · x · 2026-09-23

ctojunior 在推文串中分享：他们用 AI 帮忙构建了一个并发 bug 测试工具，不追求 TLA+ 式的形式化证明——TLA+ 检查器会穷举一定规模内的所有执行顺序，而他们的工具只尝试调度器给出的顺序。代价是不需要学习规约语言，但依然抓到了真实的并发 bug。

他的实用建议：如果你怀疑 AI 写的模型有问题，先拿一个你已经理解的 bug 来测试它——因为很容易把同一个错误假设自动化两次，自我验证会互相印证。后续推文还补充：一些失败其实是模型本身的错误而非代码 bug，所以每个失败都会对照真实代码检查，模型犯的错也被存成测试用例；他们借助 hypothesis 库做失败精简（shrink），把 40 步随机执行压缩成最小复现序列，再固化成普通单元测试。