3 ms·
FSCQ is a really great example of a large system with proofs of correctness using extraction from Coq. Another well known project is CompCert the certified C c
by johnbender 9y ago
FSCQ is a really great example of a large system with proofs of correctness using extraction from Coq.
Another well known project is CompCert the certified C compiler [1]. Which has seen a fair amount of external testing and use in verification of GCC and Clang as a reference for checking invalid compiled semantics [2] (to say nothing of compiling programs).
1 http://compcert.inria.fr http://compcert.inria.fr
2 https://blog.regehr.org/archives/1052 https://blog.regehr.org/archives/1052