如何验证Why3输出的Proof Obligations，确认代码契约证明有效性？

生成文件的格式说明 #

你观察到的类Lisp/ML格式的文件，并不是证明器生成的输出，而是Frama-C的WP插件将C代码、ACSL契约转换后，喂给对应证明器的证明义务输入文件，格式完全匹配对应证明器的输入规范：

• Alt-Ergo对应的文件采用其原生自定义语法，风格接近ML系语言，仅支持Alt-Ergo直接解析，用来声明逻辑符号、公理和待证明的目标命题。
• Z3/CVC4对应的文件符合SMT-LIB 2.x通用标准，采用S表达式（类Lisp）语法，所有兼容SMT标准的求解器都可以解析这类文件。

不依赖证明器本身正确性核验证明的方案 #

仅靠当前生成的文件无法完成核验 #

你现在导出的文件本质是「待证明的题目」，不包含任何证明过程，自然没办法仅凭这些文件确认契约和证明的有效性。

可通过导出证明凭证实现独立核验 #

主流SMT求解器和Why3框架都支持证明凭证输出能力，你可以通过调整启动参数，让证明器完成证明后输出对应的证明痕迹：比如Z3可输出proof log、Alt-Ergo可输出证明项。
这类证明痕迹可以用代码量极小、逻辑简单，甚至本身已经过形式化验证的独立证明检查器（如Dedukti、smtcoq等）进行核验，整个核验流程不需要信任Z3/Alt-Ergo这类大型证明器的实现正确性，仅需要信任底层逻辑规则和体量极小的证明检查器即可。

内容的提问来源于stack exchange，提问作者artless-noise-bye-due2AI