ACL2 (A Computational Logic for Applicative Common Lisp) is a software system that integrates a programming language, a mathematical logic, and an automated theorem prover. It is designed to support formal verification of software and hardware systems by using a subset of Common Lisp as its specification language. The system has been widely applied in both industrial and academic settings to prove the correctness of algorithms, microprocessors, and security protocols. ACL2 emphasizes a mechanized, sound logical framework in which all theorems are mechanically checked, and all programs must be proven terminating before they can be used as executable specifications.
1.1 History and Development
1.1.1 Origins from Nqthm (Boyer-Moore Prover)
ACL2 traces its roots to the Boyer-Moore theorem prover, later known as Nqthm, developed by Robert S. Boyer and J Strother Moore beginning in the 1970s. Nqthm was one of the first automated theorem provers to use a pure Lisp-based logic with induction, and it demonstrated the feasibility of proving complex theorems about programs and hardware. The system was used successfully in several landmark verifications, such as the proof of correctness of the Berkeley C string library and the verification of the FM8501 microprocessor. However, Nqthm’s reliance on a Lisp dialect different from Common Lisp limited its integration with mainstream programming tools.
1.1.2 Key Contributors and Release Timeline
ACL2 was developed by J Strother Moore and Matt Kaufmann, with significant contributions from others. The first public release of ACL2 occurred in 1996. Since then, the system has seen continuous development, with major versions released approximately every two to three years. Notable contributors include William McCune (for its early implementation), and later developers from Centaur Technology, the University of Texas at Austin, and other organizations. The latest stable version as of this writing is ACL2 8.6, released in 2023.
1.2 Core Design Principles
1.2.1 Applicative Common Lisp Subset
ACL2 uses a purely applicative subset of Common Lisp. “Applicative” means that the language is free of side effects such as assignment (setq), destructive operations (rplaca), and input/output during proof checking. This subset retains the syntactic and semantic conventions of Common Lisp, allowing users to write programs that are executable by Common Lisp compilers but also interpretable as logical definitions. The choice of Common Lisp as the base language facilitates integration with existing software and provides a large standard library of functions that can be used in specifications.
1.2.2 First-Order Logic with Induction
The logic of ACL2 is a first-order, quantifier-free logic (though with syntactic extensions for if-then-else and equality) that supports induction as a proof rule. The absence of explicit quantifiers is compensated by the use of recursive functions and definitions that implicitly define properties. Induction is the primary proof technique for proving properties of recursive functions, and the system provides powerful heuristics for choosing appropriate induction schemes.
1.2.3 Mechanical Proof Checking
Every theorem proved in ACL2 is mechanically verified by a small, trusted kernel. The kernel implements a set of axioms and rules of inference, and all proofs are reduced to a series of steps that can be checked by this kernel. This design ensures that the correctness of the theorem prover depends only on the kernel’s implementation, which is kept as simple and verifiable as possible. Users are free to define new proof strategies, but all derived theorems are ultimately justified by the kernel.
2.1 Syntax and Semantics
2.1.1 Terms, Formulas, and Definitions
The syntax of ACL2 logic is that of Common Lisp s-expressions. A term is either a constant (numbers, symbols, characters, strings), a variable symbol, or a function application of the form (f t1 ... tn), where f is a function symbol and t1,...,tn are terms. Formulas are terms that evaluate to boolean values (nil or non-nil). Definitions are introduced using the defun macro, which defines a new function symbol along with its body. Every definition must be admissible: the function must be terminating (proved via a measure), and the body must respect the type and guard restrictions.
2.1.2 Axioms and Rules of Inference
ACL2 starts with a set of built-in axioms that define the basic operations on numbers, cons pairs, strings, characters, and symbols. The rules of inference are few and are designed to be sound.
2.1.2.1 Propositional Axioms
The propositional axioms include those of classical propositional logic, largely expressed through the if-then-else macro if. The axioms for if state that (if t nil t) is equivalent to (not t) and that (if t x y) is x when t is non-nil and y otherwise. Standard propositional tautologies are derived using rewriting rules.
2.1.2.2 Equality Substitution
Equality in ACL2 follows the usual properties: reflexivity, symmetry, transitivity, and the principle of substitution of equals for equals. The equal predicate is defined axiomatically as returning t when its two arguments are identical and nil otherwise. The system uses rewriting to replace equals by equals in formulas.
2.1.2.3 Induction Schemas
ACL2 supports several induction schemas, the most common being standard mathematical induction on natural numbers and structural induction on s-expressions. The system automatically selects an appropriate induction schema based on the recursive calls in the functions involved. Users can also explicitly specify induction hints.
2.2 Types and Type Systems
2.2.1 Recognizer Functions
ACL2 does not have a static type system. Instead, types are represented by recognizer functions: predicates that return true for elements of a given type. For example, integerp recognizes integers, consp recognizes cons pairs, and stringp recognizes strings. The user can define new recognizers. The logic itself is untyped: any function can be applied to any argument, but the axioms for the function may only be valid for arguments satisfying certain recognizers (guards).
2.2.2 Guard Verification
2.2.2.1 Guard Conjectures
When a function is defined, the user may attach a guard: a formula that specifies the intended domain of the function. For example, (defun +-of-squares (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (+ (* x x) (* y y))) indicates that x and y should be integers. The system then generates guard conjectures that state: for any arguments satisfying the guard, the function’s body does not cause an error and belongs to the specified type.
2.2.2.2 Defthm and Guard Obligations
A theorem statement (using defthm) is only guaranteed to hold under the guards of the functions it uses. Before a theorem is admitted, the system may require the user to prove guard obligations that ensure the hypothesis of the theorem implies the guards of all functions called. Once guard verification is complete, the function can be executed efficiently by Common Lisp without runtime checks.
3.1 Proof Strategies
3.1.1 Rewriting and Simplification
3.1.1.1 Term Rewriting Rules (Rewrite Rules)
Rewriting is the primary proof strategy in ACL2. The user can declare formulas as rewrite rules using defthm with the :rule-classes :rewrite option. When such a rule is available, the system replaces one side of an equality with the other under appropriate conditions. Rewriting proceeds in a term-normalizing fashion, applying rules wherever their left-hand sides match subterms.
3.1.1.2 Simplification with Built-in Theories
ACL2 includes a built-in theory of simplification that handles equality, if-then-else normalization, linear arithmetic (for rationals via a decision procedure), and other elementary operations. The simplifier reduces terms to a normal form and often discharges simple goals automatically.
3.1.2 Induction
Induction is invoked when the prover encounters a goal involving a recursive function. ACL2 selects an induction scheme based on the recursion patterns of the functions in the goal. The system may also perform general-purpose induction that combines multiple functions. The induction step generates base case(s) and induction step(s). The induction hypothesis is instantiated appropriately.
3.1.3 Case Analysis and Generalization
Case analysis is performed by destructing terms based on recognizers (e.g., consp, integerp) using the “case-split” mechanism. Generalization attempts to replace a constant symbol by a variable to make a theorem easier to prove by induction. These strategies are used as part of the simplification and rewriting loop.
3.2 User Interaction and Automation
3.2.1 The Command-Line Interface
ACL2 operates primarily through a read-eval-print loop (REPL) reminiscent of Common Lisp. Users enter commands at the ACL2 !> prompt. Commands include defthm, defun, and various proof-checking directives. The system prints progress messages and, upon success, confirms the theorem.
3.2.2 Hints and Proof Tactics
Users can provide hints to guide the prover. Hints are inserted after the defthm form using the :hints keyword argument. Common hints include :use (to include a previously proved theorem), :induct (to specify an induction scheme), and :expand (to force expansion of a function). More advanced hints like :in-theory control which rewriting rules are active. Hints are structured as advice rather than scripts, and the prover attempts to honor them while maintaining soundness.
3.2.3 Proof Management (Defthm, Defaxiom, Defun)
defun introduces a function definition (with termination proof). defthm introduces a theorem that must be proved. defaxiom introduces an axiom without proof (used with caution). Once admitted, these forms are stored in the system’s database and can be used in later proofs. The :trans command allows users to inspect a theorem’s proof tree, and :sketch provides a high-level overview.
3.3 Advanced Proof Techniques
3.3.1 Use of Meta-Reasoning (Meta Rules)
ACL2 supports meta-rules: procedures written in the ACL2 programming language that analyze the current goal and suggest transformations. A meta-rule is declared with defmeta, and the prover applies it as a simplification step. Meta-rules can implement decision procedures (e.g., for arithmetic) or domain-specific reasoning.
3.3.2 Functional Instantiation
Functional instantiation is a proof technique that allows the user to prove a theorem for a generic function and then instantiate that function with a concrete one. For example, one can prove that a property holds for any function satisfying certain conditions and then apply that theorem to a specific implementation. This is done using the :functional-instance lemma instance hint.
3.3.3 Partial Correctness and Termination
ACL2 requires termination proofs for all recursive functions. The default method is to admit a lexicographic measure, typically a natural number, that strictly decreases with every recursive call. For partial correctness only (i.e., without termination), ACL2 provides a “defun-sk” macro for defining functions using second-order logic, but those are not executable. For total correctness, a measure is required.
4.1 Subset of Common Lisp
4.1.1 Supported Datatypes (Lists, Numbers, Cons Pairs)
ACL2 supports the same datatypes as Common Lisp: integers, rational numbers, strings, characters, symbols, and cons pairs (lists). The language also includes arrays and hash tables (with restrictions), but the strictly functional model forbids side effects on these structures.
4.1.2 Pure Functional Programming Model
In ACL2, all functions must be purely functional: they cannot alter global state, perform I/O, or have side effects. This ensures that functions correspond directly to logical definitions. The language does provide mv-let for multiple values and let for lexical binding.
4.1.3 Recursion and Termination Proofs
Recursion is the only form of iteration. Every recursive function must be proven terminating by the system before it can be used in proofs. The user specifies a measure (usually a natural number) that decreases with each recursive call. ACL2 automatically generates termination conjectures and attempts to prove them using its theorem prover. If the proof fails, the user can provide a measure hint.
4.2 Libraries and Utilities
4.2.1 Standard Library (Arithmetic, Lists, Sets)
ACL2 ships with a substantial standard library, known as the “ACL2 system books.” These books cover arithmetic (including bit vectors and linear arithmetic), lists (rev, append, member), sets (using ordered lists or MBE (Mbe) optimized representations), and other common data structures. The library is accompanied by numerous theorems about the functions, enabling users to build on verified foundations.
4.2.2 User-Defined Packages
Users can define their own packages (namespaces) using Common Lisp’s defpackage macro. ACL2 treats packages in the standard way, allowing separate development and avoiding name clashes. The system also supports the concept of “encapsulate” to introduce constrained functions (like abstract interfaces) that can be instantiated later.
5.1 Hardware Verification
5.1.1 Microprocessor Correctness (e.g., FM9001, Centaur)
One of the earliest and most famous applications of ACL2 was the verification of the FM9001 microprocessor, which was proved to correctly execute assembly instructions at the gate level. Later, Centaur Technology used ACL2 to verify aspects of its x86-compatible microprocessor design, including correctness of floating-point operations and memory management units.
5.1.2 Pipeline and Cache Coherence
ACL2 has been used to verify pipeline correctness (e.g., the ARM6 pipeline) and cache coherence protocols. The system’s ability to reason about induction over time steps makes it suitable for modeling hardware with finite-state machines and proving invariant properties.
5.2 Software Verification
5.2.1 Operating System Components (e.g., seL4)
The seL4 microkernel, a landmark in formal verification, used ACL2 in its verification efforts. The seL4 project proved the correctness of its C implementation via a translation to ACL2 specifications. ACL2 was used to prove high-level properties such as that the kernel never corrupts user data and that system calls behave correctly.
5.2.2 Cryptographic Algorithms
ACL2 has been applied to verify the correctness of cryptographic primitives, including AES, RSA, and elliptic curve implementations. The system’s support for arbitrary-precision arithmetic and bit-level reasoning (using the “bv” library) allows detailed verification of cryptography algorithms.
5.2.3 Java Virtual Machine Models
The Java Virtual Machine (JVM) has been modeled in ACL2, and several properties of bytecode verifier and execution semantics have been proved. These models help demonstrate the soundness of security policies in Java applets and mobile code.
5.3 Educational and Research Uses
ACL2 is widely used in graduate courses on formal verification and automated theorem proving. Its gentle learning curve (due to its Lisp syntax) and interactive nature make it suitable for teaching induction and rewriting. Research uses include meta-level reasoning, proof automation, and integration with other verification tools.
6.1 Relationship to Common Lisp
While ACL2 uses a subset of Common Lisp, it should not be confused with Common Lisp itself. ACL2 functions are only executable in a Common Lisp environment after guard verification, and they exhibit the same behavior as their Common Lisp counterparts on prescribed inputs. The standard Common Lisp functions (like car, cdr, +) are defined axiomatically in ACL2, and the logic includes theorems about their behavior. However, ACL2 does not support side effects, CLOS, or macros that manipulate state.
6.2 Comparisons with Other Theorem Provers
6.2.1 HOL, Isabelle, Coq
ACL2 differs from higher-order logic provers (HOL, Isabelle, Coq) in its logic: ACL2 uses first-order logic (quantifier-free) while others use higher-order logic. ACL2 lacks dependent types but compensates with a simple, executable language. Its automation is less user-guided than Coq’s but more automatic than HOL’s. ACL2 is particularly strong for hardware and sequential program verification, whereas Coq excels in certified programming and type theory.
6.2.2 Boyer-Moore Family (Nqthm, PC-Nqthm)
ACL2 is the direct successor of Nqthm. The main improvements are: using an industry-standard language (Common Lisp), a more powerful rewriting engine, and support for guard verification. PC-Nqthm was an interactive predecessor that allowed more user control; ACL2 integrated many of those ideas into the automatic loop. ACL2 also has a much larger library and community.
7.1 Online Forums and Mailing Lists
The primary communication channels for ACL2 users are the mailing list acl2@utlists.utexas.edu and the GitHub repository acl2/acl2. The mailing list archives contain many years of discussions on theorem proving techniques, library contributions, and bugs.
7.2 Documentation and Books
7.2.1 The ACL2 Book Series
The most comprehensive resource on ACL2 is the series “Computer-Aided Reasoning: An Approach” by Kaufmann, Manolios, and Moore, and “Computer-Aided Reasoning: ACL2 Case Studies.” These books cover both theory and practice, including many case studies.
7.2.2 Online Tutorials and Workshops
The ACL2 website (acl2.org) provides tutorials, a detailed hyperlinked manual, and links to research papers. The annual ACL2 Workshop brings together users and developers and publishes proceedings. Workshops include tutorials on new features and applications.
7.3 Annual ACL2 Workshop
The ACL2 Workshop has been held yearly since 1996 (with occasional hiatus). It includes presentations of new projects, tool improvements, and educational talks. The workshop encourages both novice and expert users to share experiences and contribute to the community.