We introduce an evaluation framework of 500 C verification tasks across five property types (memory safety, overflow, termination, reachability, data races) built on SV-COMP 2025, and evaluate 14 models across six families. We find that high overall accuracy masks a critical weakness: while most models reliably confirm properties hold, violation detection varies widely and degrades sharply with program length. To close this gap, we train on formal verification artifacts: running the Soteria symbolic execution engine on generic open-source C code and using the resulting traces for continued pretraining of Qwen3-8B. Just ${\sim}$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points, producing one of the most balanced accuracy profiles among evaluated models. On violation detection, the trained 8B model outperforms the 4$\times$ larger Qwen3-32B without thinking and approaches it in overall accuracy. The interaction between trace training and chain-of-thought is superadditive: neither alone provides meaningful gains, but their combination does. Improvements transfer across all five property types, including ones the training traces do not target. Our 28 configurations confirm the gains stem from trace semantics, not code volume, and that trace curation and format matter.

翻译：我们引入一个基于SV-COMP 2025构建的评估框架，包含500个覆盖五种属性类型（内存安全、溢出、终止性、可达性、数据竞争）的C语言验证任务，并对六个系列的14个模型进行评估。研究发现，高整体准确率掩盖了一个关键弱点：虽然大多数模型能可靠地确认属性成立，但违规检测能力差异显著，且随程序长度急剧下降。为弥合这一差距，我们使用形式化验证工件进行训练：在通用开源C代码上运行Soteria符号执行引擎，并将生成的轨迹用于Qwen3-8B的持续预训练。仅需约3000条错误轨迹结合推理时的思维链推理，即可将违规检测能力提升超过17个百分点，成为评估模型中准确率分布最均衡的模型之一。在违规检测任务中，经训练的8B模型性能超越规模大4倍的Qwen3-32B（无推理模式），并在整体准确率上接近该模型。轨迹训练与思维链的交互呈现超可加性：单独使用任一方法均无法带来显著收益，但二者结合效果显著。性能提升可迁移至全部五种属性类型，包括训练轨迹未针对的属性。我们的28组实验配置证实，收益来源于轨迹语义而非代码规模，且轨迹的筛选与格式至关重要。