FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq
summary
FreeSpec implements impure computations in Coq using a free monad over explicit interfaces and certifies them with contract types built from a computable witness plus caller and implementer obligations. The framework proves properties like “never use a closed file descriptor” for a verified mini HTTP server implemented in Coq, uses tactics such as proven_pure and a preserving tactic to discharge obligations, supports FFI execution (the HTTP server is exercised 100 times), and shows the extraction/run pipeline works.
AI-written summary · about
chapters (14)
- 0:00FreeSpec introduction
- 3:08Certified systems demos
- 4:11Mini HTTP server in Coq
- 5:30Reading files impurely
- 7:24Defining FreeSpec interfaces
- 9:09Generic TCP server in Coq
- 10:16Impure computation contracts
- 11:43File system witness states
- 15:38HTTP server proof compliance
- 17:29Respect tactics automation
- 19:52Witness states preservation
- 20:55Verified HTTP server execution
- 22:08Future directions
- 22:50Q&A
related talks
21mMaking Concurrent Hardware Verification Sequential
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
20mA Verified Foreign Function Interface Between Coq and C
13mSpoq: Scaling Machine-Checkable Systems Verification in Coq
25mExorcising Spectres with Secure Compilers
31mFormal Specification
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent
59mCoq to C Translation with Partial Evaluation + Counterexample Generation