> ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point

> ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the AMD K5 microprocessor in the wake of the Pentium FDIV bug. The interesting applications page of the ACL2 documentation has a summary of some uses of the system. Industrial users of ACL2 include AMD, Centaur Technology, IBM, Intel, Oracle, and Rockwell Collins. ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM. https://en.wikipedia.org/wiki/ACL2 https://en.wikipedia.org/wiki/ACL2 NQTHM was used to check e.g. FM9001 CPU ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 Microprocessor Proof. Tech. Rept. 86, Computational Logic, Inc., 1994. ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/086.pdf