The official specification of ACL2 can be found in the papers A Precise Description of the ACL2 Logic and Structured Theory Development for a Mechanized Logic.
ACL2 has a number of features that make it highly suitable for system modelling. Our goal is to enable HOL users to employ ACL2 as a trusted oracle. A specific case study we have in mind is to experiment with ACL2 for executing the verified ARM model due to Anthony Fox.
One of the tricky things about translating from the untyped ACL2 logic to typed higher order logic is figuring out which types to assign. An example Staples gives is that, depending on the context, the ACL2 S-expression NIL might need to be translated to F (falsity of HOL type bool), or [] (the empty list) or NONE (the empty option). The ACL2PII user has to set up "translation specifications" that are pattern-matching rewrite rules to perform the ACL2 to HOL translation. These are encoded in ML and thus cannot be validated by proof.
The approach we are now developing starts from the pioneering ACL2PII work, but aims to minimise the amount of translation that needs to be trusted. Instead of having an ML datatype representing ACL2, we define a type of s-expressions inside higher order logic that faithfully models ACL2. We then define functions on s-expressions corresponding to the ACL2 primitives so that the ACL2 axioms hold. We thus construct a model of the ACL2 logic inside HOL. We are implementing inference rules that encode higher order types and functions into ACL2 s-expressions and functions on s-expressions. The tricky ML code of ACL2PII is replaced by inference rules of the HOL logic, so the results are guaranteed sound by HOL's fully-expansive LCF methodology.
Then translation from ACL2 formulas represented inside HOL to ACL2 is still a step that needs to be implemented in ML and trusted, but it is now a just a very straightforward printing step.
There is an evolving working paper entitled Connecting HOL to ACL2 by Mike Gordon, Warren Hunt and Matt Kaufmann.