| Technical approach | ACL2 is a constructive logic. Typical ACL2 models are executable. This allows an approach to system design that mixes test with proof. For example, our formalizations of programming languages tend to be operational definitions. |
| Technical challenges | The major challenge in constructing such modeling systems is to adjust the expressiveness of the modeling language to the complexity of the analysis tools. If a language is very powerful and expressive, tools designed to analyze models expressed in it will tend to be less automatic and more complex. |
| Hard/New/Different | What is new about ACL2, as compared to its predecessor, NQTHM, is its suitability for the modeling of extremely large systems. |