Too be fair it looks like they're "just" using CompCert to go from C to asm. CompCert has been around for a while and is a verified compiler, which itself is quite an accomplishment.
But yes, it is remarkable how far things have come with regards to formal methods. But it is still quite tedious to do unless you're an academic working in the field.
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!
But yes, it is remarkable how far things have come with regards to formal methods. But it is still quite tedious to do unless you're an academic working in the field.