In many cases it’s possibly to refine a state machine based specification to an imperative implementation (and thereby carry safety properties down to the implementation) but at present the implementation usually looks like the state machine (thus codesign)
Easier maybe, but more useful? I disagree. Just because it's difficult to prove things about real programs doesn't change the fact that a formally verified program has really important advantages--like being able to actually run it, and knowing the executing code actually fulfills the spec rather than relying on a human translation layer.
Furthermore: such output depends, for correctness, on a complete and accurate description of the salient details of the programming language, and the environment it needs to run in, provided to the proof system. But such a description is more complicated and error-prone than the description of the state machine. So, you need an extra proof that the language and system description are accurate and complete, which is not provided.
As for your first point, I would wager (having done it many times) that it is considerably easier to translate a proven, working program to another language correctly, than it is to do the same thing with an abstract state machine.
So, until I see the announcement, the reasonable interpretation is that it has not been done.