ACL2
Programming language and theorem prover
title: "ACL2" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["lisp-(programming-language)", "common-lisp-(programming-language)-software", "proof-assistants", "free-theorem-provers", "lisp-programming-language-family", "software-using-the-bsd-license"] description: "Programming language and theorem prover" topic_path: "technology/programming-languages" source: "https://en.wikipedia.org/wiki/ACL2" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0
::summary Programming language and theorem prover ::
::data[format=table title="Infobox programming language"]
| Field | Value |
|---|---|
| bodystyle | width:320px |
| logo | ACL2 Logo 2014 transparent.png |
| name | ACL2 |
| paradigm | Functional, meta |
| designer | Robert S. Boyer, J Strother Moore and Matt Kaufmann |
| developer | Matt Kaufmann and J Strother Moore |
| year | 1990 (limited distribution), 1996 (public distribution) |
| latest_release_version | 8.6 |
| latest_release_date | |
| typing | Dynamic |
| influenced_by | Common Lisp, Nqthm |
| license | BSD |
| website | |
| operating_system | Cross-platform |
| :: |
| bodystyle = width:320px | logo = ACL2 Logo 2014 transparent.png | name = ACL2 | paradigm = Functional, meta | designer = Robert S. Boyer, J Strother Moore and Matt Kaufmann | developer = Matt Kaufmann and J Strother Moore | year = 1990 (limited distribution), 1996 (public distribution) | latest_release_version = 8.6 | latest_release_date = | typing = Dynamic | influenced_by = Common Lisp, Nqthm | license = BSD | website = | operating_system = Cross-platform
ACL2 (A Computational Logic for Applicative Common Lisp) is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software.
Overview
The ACL2 programming language is an applicative (side-effect free) variant of Common Lisp. ACL2 is untyped. All ACL2 functions are total that is, every function maps each object in the ACL2 universe to another object in its universe.
ACL2's base theory axiomatizes the semantics of its programming language and its built-in functions. User definitions in the programming language that satisfy a definitional principle extend the theory in a way that maintains the theory's logical consistency.
The core of ACL2's theorem prover is based on term rewriting, and this core is extensible in that user-discovered theorems can be used as ad hoc proof techniques for subsequent conjectures.
ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, NQTHM. Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories. ACL2 also derives efficiency from being built on Common Lisp; for example, the same specification that is the basis for inductive verification can be compiled and run natively.
In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, received the ACM Software System Award "for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software."
Proofs
ACL2 has had numerous industrial applications. In 1995, J Strother Moore, Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of the AMD K5 microprocessor in the wake of the Pentium FDIV bug.
Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.
References
References
- "XDOC — Note-1-7".
- (August 1, 2008). "ACM: Press Release, March 15, 2006".
- "Software System Award". [[Association for Computing Machinery]].
- "ACL2 Annotated Bibliography".
- "ACL2 Workshops and UT ACL2 Seminar".
- (1996). "A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm". IEEE Transactions on Computers.
::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::