CounterProof 在 AI 模型的协助下审查安全关键代码。
在实践中，AI 审查不是确定性的。把同一次审查运行两次，预计会得到不同的发现项；换上新一代模型，预计又会得到不同的发现项。在这一点上，LLM 代码审查的表现更像模糊测试，而不像静态分析器；而且和模糊测试一样，它永远没有完成的时候（Thomas Dullien，《实验的时代》［英文］，BlueHat Asia 2026）。
正因如此，我们拒绝代表你作出以下主张。
我们不把 AI 模型之间的一致当作证明。模型经常犯同样的错误：两个模型都出错时，它们往往错在同一处；来自不同公司的模型也不会自动相互独立（Kim 等，ICML 2025）。一个共同的答案，可能是一个共同的错误。
我们不让一个流畅的裁决压过一项测试。对于托管、结算、共识和密钥处理代码，起决定作用的是执行、测试和证明。模型输出告诉我们该看哪里；它并不告诉我们什么是真的。
我们按每个发现项的确立方式为其标注。“已复现”指在固定的版本上，针对未经修改的代码运行过测试。“已阅读”指有对该代码的阅读作为支持，但没有运行它。我们从不把后者当作前者呈现。
我们不靠投票压过提出发现项的审查者来关闭一个发现项。只有当提出者撤回它，或者它已对照代码得到证实时，这个发现项才会关闭。
我们不把“我们什么也没发现”报告成“什么也不存在”。一个干净的结果说明的是检查了什么，而不是什么不存在。