ACL2, or A Computational Logic for Applicative Common Lisp, is an interactive theorem prover that combines a Lisp-based programming language for developing formal models of systems with a reasoning engine that can prove things mechanically and mathematically of said models. It is both the functional programming language built on top of lisp and a First-order Logic