Nice description and first steps. Ideal moves would probably be the following:
Modifying front-end for Frama-C flow or similar tool to take a subset of Rust with specs, generate the VC’s, and feed them to supported provers. He seems to be doing something similar but Im sure there’s some good tools to build on.
For manual and high-assurance, embed Rust into Simpl/HOL that seL4 used. Do an AutoCorres tool with that. You now have ability to pull similar effort with translation validation to machine code. Next, extend COGENT to generate Rust subset Simpl supports. You can now do, like their C example, a whole filesystem functionally that outputs verified Rust or machine code. Optionally extend the COGENT tool with QuickCheck, QuickSpec, etc esp where tests/specs can translate to Rust to. Quite a foundation for other Rust developments to build on. Including redoing Rust compiler in COGENT at least for certified, reference version. ;)