If you use microprocessors from companies like AMD and Intel, there is a good chance that parts of their design were checked with large amounts of Lisp code. E

If you use microprocessors from companies like AMD and Intel, there is a good chance that parts of their design were checked with large amounts of Lisp code. Example: https://github.com/acl2/acl2/tree/master/books/rtl/rel11 https://github.com/acl2/acl2/tree/master/books/rtl/rel11 > This directory contains an ACL2 library of register-transfer logic, developed at AMD from 1995 to 2011, and at Intel from 2012 to the present, in support of the mechanical verification of the floating-point arithmetic units designed during those periods by the respective companies.