Coq's vibrant ecosystem for verification engineering
summary
Coq now supports end-to-end, layered verification: a Verified Software Toolchain connects C proofs to the CompCert semantics and backends like CompCert and CertiCoq; domain libraries include Flocq, Mathematical Components, FCF, CertiGraph and interaction trees. Proven artifacts include HMAC‑DRBG (cryptographic bound ~0.5+2^-70), a generational GC, Newton sqrt for floats, Reed‑Solomon erasure code, and compiler backends; a Coq platform distribution pins compatible package versions to avoid dependency hell and the proofs build and check reproducibly.
AI-written summary · about
chapters (17)
- 0:00Start
- 0:06Andrew Appell
- 2:25Prove Programs Correct
- 6:34What Language Should We Write the Program
- 8:22Connect the Program to the Low-Level Spec
- 11:34Verified Software Tool Chain
- 19:01Separation Logic
- 31:17Forward Erasure Correction
- 32:46Generational Garbage Collector
- 35:41Foundational Cryptography
- 36:08Foundational Cryptography Framework
- 38:42Interval Arithmetic
- 45:28Dll Hell
- 49:47The Collaborative Ecosystem
- 51:20Continuous Open Source
- 52:06Continuous Integration
- 55:14Proof Irrelevance
related talks
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 04mSoftware Verification meets Real-World Cryptography
47mHow to trust a verified program?
01h 07mThe Cogent and Dargent approach to facilitating verified software development
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
27mC4: verified transactional objects