acl2 (math/acl2) Add to my watchlist

Applicative Common Lisp / A Computational Logic

ACL2 (Applicative Common Lisp / A Computational Logic) is the successor to nqthm, the Boyer-Moore theorem prover. ACL2 can be used to automatically or semi-automatically prove theorems and has been used extensively in real applications (e.g., proving the correctness of certain calculations in the floating point unit of the AMD K5 microprocessor. ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover. Because the meta-language is the same as the language (a subset of Common Lisp), it is very flexible.

Version: 8.3 License: BSD GitHub
Maintainers JacksonIsaac
Categories math
Platforms darwin
  • ccl (Use ccl as the underlying lisp)
  • certify (Certify the included books)
  • emacs (Include support for using acl2 under emacs)
  • nonstd (Build the nonstandard analysis books for handling real numbers)
  • regression (Run the regression test suite (nb: takes hours))

"acl2" depends on

lib (1)
build (1)

Ports that depend on "acl2"

No ports

Port notes

Users who want to use ACL2 for serious work should
install the certify variant (sudo port install +certify),
which will certify (i.e., prove all of the theorems)
in the included examples. This can take several hours.

Port Health:

Loading Port Health

Installations (30 days)


Requested Installations (30 days)


Livecheck results

acl2 seems to have been updated (port version: 8.3, new version: 8.5)

livecheck ran: 8 hours ago