VeriFast is a leading tool for the modular formal verification of correctness properties of single-threaded and multi-threaded C and Rust programs. It verifies a program by symbolically executing each function in isolation, exploiting user-annotated preconditions, postconditions, and loop invariants written in a form of separation logic, and using a separation logic-based symbolic representation of memory. However, the tool itself, written in roughly 30K lines of OCaml code, has not been formally verified. Therefore, bugs in the tool could cause it to falsely report the correctness of the input program. We here report on an early result extending VeriFast to emit, upon successful verification of a Rust program, a Rocq proof script that proves correctness of the program with respect to a Rocq-encoded axiomatic semantics of Rust. This significantly enhances VeriFast's applicability in safety-critical domains. We apply hinted mirroring: we record key information from VeriFast's symbolic execution run, and use it to direct a replay of the run in Rocq.

翻译：VeriFast是用于单线程与多线程C及Rust程序正确性属性模块化形式验证的主流工具。该工具通过隔离符号执行每个函数进行验证，利用用户以分离逻辑形式编写的先决条件、后置条件及循环不变式，并采用基于分离逻辑的内存符号表示。然而，该工具本身（约由3万行OCaml代码实现）尚未经过形式化验证，因此工具中的缺陷可能导致其错误报告输入程序的正确性。本文报告一项早期研究成果：扩展VeriFast使其在成功验证Rust程序后，生成能证明该程序相对于Rocq编码的Rust公理语义正确性的Rocq证明脚本。这显著增强了VeriFast在安全关键领域的适用性。我们采用提示镜像技术：记录VeriFast符号执行过程中的关键信息，并利用这些信息指导Rocq中的执行重演。