A Verified Foreign Function Interface Between Coq and C
summary
VeriFFI provides a verified foreign-function interface that translates Coq dependent types and Coq functional models into VST specs so C functions, once proved against those specs using VST, are guaranteed to implement the Coq models when linked with code compiled from Coq (via zico). The system generates proofs and rewrite equalities from refi descriptions (a hybrid deep/shallow IR produced by metaprograms) and demonstrates working proofs for pure and mutable-array examples, though full open-program compiler correctness and some side‑effect proofs remain unfinished.
AI-written summary · about
chapters (14)
- 0:00Verified FFI between Coq and C
- 1:03Multi-language verification problem
- 2:48Verify project setup
- 3:52Machine integer interfaces
- 4:56FFI operational side
- 5:16C function correctness proofs
- 7:00Function specs via reification
- 8:01Reified vs monolithic specs
- 9:45Dependent types via reification
- 11:09Type safety in FFI calls
- 13:16FFI with side effects
- 13:36Talk takeaways
- 14:39Future work and compiler correctness
- 15:06Q&A
related talks
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent
01h 06mVerifying a compiler through equational means
24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTL
24mFreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
23mVellvm: Formalizing the Informal- 01h 06mVerifying a compiler through equational means
01h 05mAll the Languages Together
29mTowards Formally Verified Just-In-Time Compilation