It is interesting how readable the proofs produced by ACL2 are. Also, the automation applies induction and generalizes conjectures, which is something that no other proof assistant I'm aware of does.<p>The same authors also wrote "A Brief ACL2 Tutorial" [0], which seems to explain the process of developing an ACL2 proof more.<p>[0]: <a href="https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html" rel="nofollow">https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html</a>