There was a soundness bug in Version 8.6 and earlier. That bug is unlikely to affect anyone, as it has probably been present for 30 years without anyone mentioning it to the ACL2 developers. If you want to fix it, then replace the definition of function cl-set-to-implications with the definition below, either in source file proof-builder-a.lisp before building your ACL2 executable, or loaded into raw Lisp (so, preceded by :q and followed by (lp), or loaded into ACL2 (so, preceded by :redef+ and followed by :redef-). The last of these three options will however make it impossible to certify a book in that session.
(defun cl-set-to-implications (cl-set)
(declare (xargs :mode :program))
(if (null cl-set)
nil
(cons (make-implication (dumb-negate-lit-lst (butlast (car cl-set) 1))
(car (last (car cl-set))))
(cl-set-to-implications (cdr cl-set)))))
The "changelogs" for ACL2 are in the release-notes topics of the manuals. In particular, there are release notes for Version 8.6.
ACL2 sources are available between releases at the ACL2 GitHub Repository.
A team of four ACL2 users entered the VSTTE 2012 competition. For information, including the team's solution, visit this link.
The ACL2 GitHub repository allows contributions of ACL2 books (input files), and also provides between-release updates.