The system described here, A Computational Logic for Applicative Common Lisp (ACL2), is a reimplemented extended version of the Boyer-Moore theorem prover Nqthm. ACL2 is geared toward large-scale verification as well as enhancements in interactivity and convenience required for industrial-strength applications. While preserving the use of total functions within the logic, ACL2 extends a large applicative subset of Common Lisp. Besides a useful collection of data types, the extension captures single-threaded states, I/O, multiple-valued functions, fast applicative arrays, and property lists. ACL2 requires that every function have a “guard,” an extralogical notation describing the intended domain of the function. This notion helps relate the logic to Common Lisp, allowing efficient execution while separating the concerns of admission of logical definitions, simplification of the proofs of certain function properties, type correctness, and compliance with Common Lisp. The goals of robustness, stability, maintainability, and support for proofs are addressed explicitly. Two industrial applications are described: a model of a signal processing chip and the proof of a floating-point division kernel.