The Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible guide to proving theorems in this system.