alt Hacker NewsWhen I met him unfortunately I didn't realize how important he was (1987). The place where I worked used formal methods to verify the design of an FPU, in collaboration with the PRG. iirc the project was a success. I never heard of formal methods being successfully used again until TLA+ a few years ago.
Inmos’ Occam-based verification of their FPU in collaboration with researchers at Bristol and Oxford iirc? Citation: http://people.cs.bris.ac.uk/~dave/formalmethods.pdf
David May was my PhD supervisor and always spoke very highly of Sir Tony Hoare.
Edit: I’m also lucky enough to have worked with Geoff Barrett, the guy that completed that formal verification (and went on to do numerous other interesting things). Some people may be interested to learn that this work was the very first formal verification of an FPU - and the famous Intel FPU bug could have been avoided had Intel been using the verification methods that the Inmos and University teams pioneered.