I don't think a reasonable reading of the statement implies "fully automated", at which point the answer to the question is no.
Obviously some C code isn't just "not verifiable correct" but "actually wrong in a memory unsafe way". That code isn't going to be automatically translated without human intervention because, how could it be, there is no correct equivalent code. The tooling is going to have to have an escape hatch where it says "I don't know what this code is meant to do, and I know it isn't meant to do what it does do (violate promises to the compiler), help me human".
On a theoretical level it's not possible for that escape hatch to only be used when undefined behaviour does occur (rices theorem). On a practical level it's probably not even desirable to try because obtuse enough code shouldn't just be blindly translated.
So what I imagine the tooling ends up looking like is an interactive tool that does the vast majority of the work for you, but is guided by a human, and ultimately as a result of that human guidance doesn't end up with exactly equivalent code, just code that serves the same purpose.
Obviously some C code isn't just "not verifiable correct" but "actually wrong in a memory unsafe way". That code isn't going to be automatically translated without human intervention because, how could it be, there is no correct equivalent code. The tooling is going to have to have an escape hatch where it says "I don't know what this code is meant to do, and I know it isn't meant to do what it does do (violate promises to the compiler), help me human".
On a theoretical level it's not possible for that escape hatch to only be used when undefined behaviour does occur (rices theorem). On a practical level it's probably not even desirable to try because obtuse enough code shouldn't just be blindly translated.
So what I imagine the tooling ends up looking like is an interactive tool that does the vast majority of the work for you, but is guided by a human, and ultimately as a result of that human guidance doesn't end up with exactly equivalent code, just code that serves the same purpose.