Applications
- Four color theorem: formal proof using Coq was completed in September 2004.
- Feit–Thompson theorem: formal proof using Coq was completed in September 2012.
- Compcert an optimizing compiler for C (programming language) which is fully programmed and proved in Coq.
Read more about this topic: Coq