From 1+1=2 to machine-checked curve arithmetic — the book
A LaTeX/TikZ book plus compiling exercise files - now in its second edition (14 chapters, 132 pages) - a curriculum that takes an undergraduate with zero formal-methods background to the point of reading, and extending, the real Lean 4 proofs in the ed25519/Pallas verification family.