alt Hacker NewsI 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?