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).