Isn't formal verification a "just write it twice" approach with different languages? (and different logical constraints on the way you write the languages)