{{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}}
ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.