Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring

TL;DR

The paper tackles the risk that VeriFast's own implementation may harbor bugs, since the verification tool itself has not been formally verified. It introduces Hinted Mirroring, a pragmatic technique that records key symbolic-execution data from VeriFast and replays it inside Rocq to produce a Rocq-based proof of Rust programs verified by VeriFast. The authors implement a proof-script generator that outputs bodies, preds, specs, symex_trees, and a single correctness goal, and prove soundness of the approach with respect to a Rocq AxSem, bridging separation-logic verification with foundational reasoning. This approach broadens VeriFast's applicability to safety-critical domains and points to future work on more Rust features, automation steps, and validation against alternative semantics.

Abstract

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.

Figures (2)

• Figure 1: An example VeriFast-annotated Rust program that reverses a linked list of pointer variables
• Figure 2: Symbolic execution traces for functions main and reverse_iter ($\mathsfsl{original} \neq \mathsf{nullptr}$ case), showing the symbolic heap, symbolic store, and path condition at each point. Since the path condition only grows, and in these examples so does the symbolic store, we only show new elements. Producing a chunk adds it to the front of the symbolic heap. Newly produced heap chunks are shown in green; heap chunks that will be consumed next are underlined in red. $\mathsf{ConsumeChunk}$ hints are shown in orange (see § 3).