ACL2
{{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".