If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):

1. https://mitpress.mit.edu/9780262527958/the-little-prover/

2. https://mitpress.mit.edu/9780262536431/the-little-typer/

David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.