Agent 驱动形式化验证盲测：远超传统代码审计

Doug（@0xdoug）团队通过盲测对比 Agent 驱动的形式化验证与传统代码评审，获得实证数据支持。方法上，他们让 agent 起草形式化规范，再用形式验证工具验证，且 prompt 写法对结果有显著影响。在深度审查过的代码库中，该方法发现大量真实漏洞：传统代码审计仅能找出约八分之一的漏洞，而形式化规范几乎全部命中，作者称结论接近万能。

2026-10-24 ~ 2026-10-25 · 2 条相关