> [Hey, does anyone recall which processor it was that was Formally Verified?
> At least, verified as conforming to the specifications, given the usual
> waffling about assuming that fussy analog transistors really are perfect
> digital switches ;-), with nothing being said about even HOPING to formally
> prove the specification correct...  

It was the FM9001, formally and mechanically verified by a souped up version
of the Boyer-Moore Theorem prover by Computation Logic Inc (which seems
to have consisted of Boyer, Moore, and a few of their ex-students):
parts of the AMD 586 floating point unit):

	http://www.cli.com/hardware/fm9001.html

CLI also verified parts of the AMD 586 floating point unit. The company
seems to have dissolved this year and Moore started teaching at UT, where
Boyer already taught.

> (And, to pretend at least some vague
> current-users topicality, has NetBSD been ported to that processor? :-) ) ]

(And to keep pretending by answering the question "Uh, no" :-)

Although if you dig into their web site you should find something on one of 
their students verifying the 68000 machine code from the BSD string library
produced by a verified assembler. This is from memory. It happened while I 
was a grad student there - sometime around 1991.

Jason