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

TL;DR

This paper extends the VeriFast verification tool to produce formal proof scripts in Rocq, enabling formal correctness guarantees for verified Rust programs and improving safety in critical applications.

Contribution

It introduces a method to generate Rocq proof scripts from VeriFast's symbolic execution, enhancing verification trustworthiness for Rust programs.

Findings

Successfully generated Rocq proofs for verified Rust programs

Enhanced VeriFast's applicability in safety-critical domains

Demonstrated the effectiveness of hinted mirroring technique

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.