From 1+1=2 to machine-checked curve arithmetic — the book
The verification campaign that produced dalek-ed25519-verified and its siblings left behind a trail of hard-won understanding that lives nowhere in the repos themselves. The proofs compile; the pathway to being able to write them is invisible. This repo is that pathway, written down properly: a twelve-chapter book (106 pages, full color, LaTeX/TikZ, built from source in the repo) plus exercise files that actually compile against a pinned toolchain.
The premise: an undergraduate with high-school algebra, a little programming, and zero formal-verification background can get from 1 + 1 = 2 to reading — and extending — machine-checked proofs about production elliptic-curve code. Not toy code. The actual radix-2⁵¹ field arithmetic of curve25519-dalek, extracted to Lean 4, with the actual constants: 2²⁵⁵ − 19, the ×19 fold, the 254-squaring inversion chain, the true Pratt tree of p − 1. The book's central pedagogical bet is that the real numbers carry the real arguments — every chapter has pen-and-paper worked examples with the production constants, because inverting 19 modulo a 77-digit prime in five lines of Euclid teaches you something that x⁻¹ mod p never will.
The arc: why testing can't find the carry bug (ch. 1), Lean as a programming language (2), Curry–Howard (3), tactics as dialogue (4), the automation discipline — omega, ring, norm_num, decide, and when simp is a loaded weapon (5), modular arithmetic (6), primality certificates (7), the Charon/Aeneas extraction pipeline (8), and the denotation bridge — the commuting square that makes theorems about limbs mean theorems about field elements (9). Then an interlude I'm particularly attached to: one complete verification done entirely by hand, then re-enacted in Lean line by line. Chapters 10–12 tell the full field campaign honestly — including the crash — and end at the pyramid: group law, scalars, signatures, and where the reader comes in.
The engineering claim behind the pedagogy: every solution file compiles with zero errors against the pinned toolchain, and everything the book says about the companion repos reflects their actual, auditable state — open frontiers included. A textbook that drifts from its subject matter is a special kind of lie; this one is built from the same source tree discipline as the proofs it teaches, with exercise holes (sorry) whose solutions ship alongside, each solution leading with how a person finds the answer before the answer itself.
Appendices: recipe cards with drills, guided walkthroughs of every exercise hole, a tour of the real repositories, a glossary, and a thirteen-week course plan — because the honest test of the material is whether someone else can teach from it. The verification family proved the code. This is the part that reproduces the people who can do the proving, which in formal methods has always been the scarcer resource.