I know the project quite well, it's led by Appel and is called Verified Software...

mpu on June 7, 2015 | parent | context | favorite | on: Verified Correctness and Security of OpenSSL HMAC

I know the project quite well, it's led by Appel and is called Verified Software Toolchain. They not only compile their code with compcert but also use its correctness theorem to derive the validity of the Assembly code!