面向关键领域的 VeriFast 认证：通过标记镜像实现验证工具结果的实用主义认证
编程语言
2026-01-21 v1
摘要
VeriFast 是一个领先的工具，用于对单线程和多线程 C 和 Rust 程序的正确性属性进行模块化形式验证。它通过符号执行每个函数，利用用户在分离逻辑中编写的前置条件、后置条件和循环不变量，并使用分离逻辑表示的内存来验证程序。然而，该工具本身（约3万行 OCaml 代码）尚未形式化验证。因此，工具中的错误可能导致其错误报告输入程序的正确性。我们在此报告了一项初步工作，将VeriFast扩展以在成功验证 Rust 程序后发出Rocq证明脚本，以证明程序相对于Rocq编码的 Rust 公理语义的正确性。这显著增强了VeriFast在安全关键领域的适用性。我们采用标记镜像技术：我们记录VeriFast符号执行运行的关键信息，并用于在Rocq中对该运行进行重放。
引用
@article{arxiv.2601.13727,
title = {Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring},
author = {Bart Jacobs},
journal= {arXiv preprint arXiv:2601.13727},
year = {2026}
}
备注
8 pages, 2 figures