3 ms·CompCert is a good example of Coq used to develop complex commercial proven correct software.by deterministic 3y agoCompCert is a good example of Coq used to develop complex commercial proven correct software.