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.
The same authors also wrote "A Brief ACL2 Tutorial" [0], which seems to explain the process of developing an ACL2 proof more.
[0]: https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html
