025 · 返回值被唯一确定，就算规格完整了吗？SpecAgent 用依赖感知规划、形式验证、跨规格修复与强度审查生成 ACSL 规格；其完备性探针能识别返回值欠约束，但不能单独证明规格已表达全部重要语义。