VERDICT：多智能体并行模块化验证框架

VERDICT 是一个面向大规模程序模块化演绎验证的多智能体框架，通过基于假设的并行规约合成与双向过程间冲突协调，让各函数智能体可同时推进验证。在真实 C 程序上，它合成的规约质量优于现有方法并大幅缩短验证时间，首次扩展到完整的 20,000 行 X.509 解析器，数小时内排除几乎所有潜在运行时错误，而 PREGUSS 等此前工具运行数天仍远未达到。