Compiling C to Safe Rust, Formalized

Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.

What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)

I suppose hypothetically putting it in an easier language to make changes in. Though it's hard to imagine it being easier to make changes to transpiled code than the original.

Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.