[js8]

I would recommend https://lean-lang.org/theorem_proving_in_lean4/, especially the first few chapters, if you're willing to use Lean.