Projects / ACL2


ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.

Operating Systems

Recent releases

  •  11 Apr 2011 06:21

    Release Notes: The accumulated-persistence utility can now do finer-grained tracking, providing data for individual hypotheses and the conclusion of a rule. The defattach utility now permits the use of :program mode functions, though this requires the use of a trust tag. Redefinition is no longer permitted for functions that have attachments. The system function translate-and-test now permits its LAMBDA form to refer to the variable WORLD, which is bound to the current ACL2 logical world. The built-in "untranslate" functions were improved to produce let* expressions when appropriate.

    •  25 May 2009 18:40

      Release Notes: There is improved support for controlling the printer and "eviscerating" large objects. Certificate files now take advantage of structure sharing and are more compact. The user now has more control over the "rulers" used in termination analysis. Many various efficiency improvements have been made, mainly with respect to supporting very large objects. A few soundness bugs have been patched, and there have been numerous other bugfixes.

      •  05 Jun 2007 21:51

        Release Notes: A soundness bug and some other minor bugs have been fixed. Including books has been sped up by as much as 50%. Rewriting can be dynamically monitored. Accumulated persistence supports meta-rules and identifies useless rules, and many other minor updates have been made.

        •  05 Dec 2006 08:07

          Release Notes: A few soundness bugs were identified and corrected along with several potential hard Lisp errors and other minor issues. The performance of theory invariants has been improved. New books include a resolution/paramodulation prover, concurrency modelling, transfinite induction, and a simplification utility. A new "trust tag" feature allows the use of potentially unsafe features in ACL2 extensions.

          •  06 Aug 2006 04:07

            Release Notes: Several bugs were fixed, including a soundness bug. Efficiency has been significantly improved, and the regression suite runs about 20% faster. New features include time limits for the prover, enhanced controls for compilation with certify-book, and a new utility for debugging failed encapsulate and progn events.

            Recent comments

            05 Jun 2007 12:13 aiken11

            Re: Why such an IMHO offensive name?

            > do you guys want to popularize on

            > Franz's success? Or is it a bad pun on

            > ACL?



            I doubt there was any intended connection. Franz's renamed their product from "ExCL" to "Allegro CL" in 1988 (according to their company history page), and the ACL2 project began in 1989 (according to their acknowledgements page).

            07 Dec 2006 11:42 asigov

            Why such an IMHO offensive name?
            do you guys want to popularize on Franz's success? Or is it a bad pun on ACL?


            Project Spotlight


            A Fluent OpenStack client API for Java.


            Project Spotlight

            TurnKey TWiki Appliance

            A TWiki appliance that is easy to use and lightweight.