I have found Isabelle very useful, and Dafny even more so.
Amazon AWS uses Dafny to prove the correctness of some complex components.
Then, they extract verified Java code. There are other target languages.
Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.
Have you tried using them as macro assemblers in the way described in the paper?
No, I haven't. I have used them with shallow embedding techniques that are relatively similar, but not in this way.
That sounds interesting!