{{stub}}
{{language
|site=http://userweb.cs.utexas.edu/users/moore/acl2/
|strength=strong
|safety=unsafe
|checking=dynamic
|gc=yes
|LCT=yes}}
{{language programming paradigm|Functional}}
{{implementation|Lisp}}
[http://www.cs.utexas.edu/users/moore/acl2/ From the University of Texas at Austin, late 2018:]

ACL2 is a logic and programming language in which you can model computer systems, together with a tool to help you prove properties of those models. "ACL2" denotes "'''A''' '''C'''omputational '''L'''ogic for '''A'''pplicative '''C'''ommon '''L'''isp".