For a little over 11 years, I worked for ICL (now part of the Fujitsu Group); the ProofPower web site will tell you a lot more about the work that was done there in the development of tools to support formal methods, particularly specification and proof in HOL and Z. There are several papers on the web site.
These tools were originally conceived for use in the certification of high assurance secure systems, but are now mainly used for specifying and verifying safety critical systems. I am now an independent consultant in this area - still working closely with my former colleagues from ICL. My company Lemma 1 has some WWW pages you might like to visit.
I also have a strong interest in using mechanized proof tools to formalise pure mathematics. There is a light-hearted report on one aspect of progress in this area, where you can also find useful links to the available systems.
In my spare time, I sometimes work as a tutor on the Open University's CCI/MMT M.Sc. course. I'm also a member of the Z standardisation panel. I have a personal collection of papers concerned with the Z standard.
Last Update: $Date: 2009/04/26 15:12:25 $; Visits to this site: