I'm curious how their approach compares with what Theorem & Anthropic are trying to do with formally proving nixpkgs:
https://theorem.dev/blog/verified-software-stack/
It seems the work of Google involved more experts work, although it might be more about how things are presented. Also this work on Signal contains a substantial specification and verification of the cryptographic protocol, something requiring specialists of the field. On the Anthropic & Theorem side, the specification is more general (and hence lighter): memory safety and absence of assert failures. They target also various software instead of Signal in particular.