一句话：提出 VeriFFI，在 Coq 与 C 之间建立可验证的 FFI，保证组合程序的类型安全与正确性。
在 Coq 中可以编写依赖类型函数程序并证明其正确性，在 C 中可以编写底层程序并用 C 验证工具证明其正确性；问题是如何将两者组合并交互证明。本文提出 VeriFFI，一个经过验证的外部函数接口：它把 Coq 的函数类型、构造子类型以及函数模型翻译为 VST 函数规约；若用户能在 VST 中证明 C 函数满足这些规约，则 C 函数的行为符合用户指定的函数模型，即使其实现可能完全不同。这样，调用 C 代码的 Coq 函数证明便可依赖该行为。实现该翻译的关键是一种新颖的 Coq 依赖类型混合深/浅描述。VeriFFI 保证组合程序类型安全与正确性。
One can write dependently typed functional programs in Coq, and prove them correct in Coq; one can write low-level programs in C, and prove them correct with a C verification tool. We demonstrate how to write programs partly in Coq and partly in C, and interface the proofs together. The Verified Foreign Function Interface (VeriFFI) guarantees type safety and correctness of the combined program. It works by translating Coq function types (and constructor types) along with Coq functional models into VST function-specifications; if the user can prove in VST that the C functions satisfy those specs, then the C functions behave according to the user-specified functional models (even though the C implementation might be very different) and the proofs of Coq functions that call the C code can rely on that behavior. To achieve this translation, we employ a novel, hybrid deep/shallow description of Coq dependent types.
@article{KorkutSA25,
title = {A Verified Foreign Function Interface between Coq and C},
author = {Joomy Korkut and Kathrin Stark and Andrew W. Appel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704860}
}