Industrial-Strength Documentation for ACL2

ABSTRACT. The modeling tools, specifications, and proof scripts for an industrial formal verification effort can easily reach hundreds of thousands of lines of source code. High quality documentation is vital for teams that are working on projects of this scale. We have developed a flexible, scalable docu- mentation tool for ACL2 that can incorporate the documentation for the ACL2 theorem prover, the Community Books, and an organization’s internal formal verification projects. The resulting manuals are automatically accurate and current, and are easily deployed throughout an organization.