The FM9801 Microprocessor is a microprocessor design designed for formal verification research. It contains a number of features found in today's microprocessor designs, such as speculative execution, out-of-order execution, branch prediction, exceptions, and so on. The FM9801 Microprocessor has been completely verified using the ACL2 theorem prover. It is the most complex pipelined microprocessor design ever completely verified.