I developed predicate transformer semantics for sequential Ada83 that were the basis of the Penelope formal verification system. The predicate transformers were derived systematically from a denotational semantics in the way described in my 1981 POPL paper.
Supported the Ada9X design team with formal analysis and description of the new object-oriented constructs. The definition used Z specifications of semantic domains and natural semantics to describe Ada9X objects and dispatching operations.
The proper way to used verification technology is as an integral part of the design process. The idea is to build things that are correct by construction. Ultimately we want to produce code from specifications automatically.
Code synthesis is practical when limited to narrow domains. I have developed a special purpose language and associated code generator for satellite control systems (used on Gravity Probe B). The tool produces flyable Ada code from MatLab specifications of control laws.
Why do we need more programming languages? Because in the long term programming will become a tool of many professions just like programming spreadsheets has already become the job of accountants.
For the domain of investment banking I have designed a special purpose language for describing and analyzing investment portfolios of derivative instruments.
My short paper Formal Methods in Practice elaborates on the idea of domain specific languages and their role in technology transfer.