ACL2 demostrador de teoremas

El día de hoy me llamó la atención ACL2 (Applicative Common LISP) el cual puede servir como un demostrador de teoremas. Por ahora me puse averiguar en que aplicaciones fue utilizado con exito, que vienen siendo los siguientes:

-Encontrar bugs en compiladores, al mismo tiempo que se valida el diseño.
-Probar sistemas complejos de hardware y software.