This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.
And CompCert, a formally verified C compiler written in Coq: https://compcert.org/
(even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq.
For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif.
For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.
Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/.