Depends on the details of how you're formalizing your verification and what tools you have at your disposal. It could be immensely useful as a stand-in for a sp

Depends on the details of how you're formalizing your verification and what tools you have at your disposal. It could be immensely useful as a stand-in for a specification since it reduces a large class of verification to "does it do the same thing as the reference compiler." E.g. it's a huge amount of work to exhaustively formally specify the Rust type system (as opposed to just specify it in English). However, if you already have an assumed correct, but slow, type checker then your verification effort can boil down to just "does my compiler have a type error if [and only if if you care about more than just safety properties] the reference compiler has a type error?" That's still an enormous amount of work to verify, but is comparatively trivial to specify.