This is indeed very similar in the approach. Proofs done at assembly level, with the advantage of a clear semantics, over massive code bases, with access to a lot of tokens and using interactive theorem provers, Rocq or Lean, whose base theories are quite similar.

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.