ACL2 ist eine mathematische Logik, eine Programmiersprache und ein mechanischer Satzbeweiser, der auf der applikativen Untermenge von Common Lisp beruht. Es ist eine robuste und produktiv einsetzbare Version des NQTHM- oder Boyer/Moore-Satzbeweisers und wurde bereits für die formale Verifikation von kommerziellen Mikroprozessoren, der Java Virtual Machine, interessanten Algorithmen usw. benutzt. (non)