https://the-little-prover.github.io/

[book-cover]   The Little Prover

               Written by Daniel P. Friedman and Carl Eastlund
               Drawings by Duane Bibby
               Foreword by J Strother Moore
               Afterword by Matthias Felleisen

               Available from MIT Press

J-Bob

J-Bob is our little proof assistant, available on Github. For an
introduction to J-Bob, see Appendix A of The Little Prover.

J-Bob is available for ACL2, Scheme, and Racket (via the Dracula
package). J-Bob is open source, feel free to adapt our proof
assistant to the programming language of your choice.

Bear in mind that J-Bob is simple so that its source code can be read
and understood. As a result, using J-Bob can be tedious and tricky at
best. We sympathize with any difficulties you have, and we look
forward to the creative extensions that users of J-Bob may come up
with to make it easier.

Errata

Pages 165-166: replace all occurrences of "cheese" by "eggs"

Page 167: Frame 10 RHS: add "-31" to the right of "29"

Page 169: Frame 21 LHS: drop "of chapter 2"

Page 170: Frame 25 LHS: drop "of chapter 2"

Page 171: Frame 32 LHS: drop "of chapter 3"

Page 178: Frame 60 LHS: drop "of chapter 5"

Page 178: Frame 60 LHS: replace "56" by "55"