The halo2 Book, by Jack Grigg, Sean Bowe, Daira Emma Hopwood, and Ying Tong Lai, is the living online documentation for the halo2 proving system and its Rust crate. Its strength is the way it ties a circuit author's layout choices to the cost of a proof and to what that proof can establish. It does this by linking its chapters on chips and testing to design and background chapters on arithmetization and commitments.
The chapter on proof systems separates a relation from the circuit implementing it. It counts intermediate advice values alongside private inputs as the witness, so the witness depends on how the circuit was written. It then distinguishes a proof that some witness exists from a proof that the prover knew one. The second property is formalized by an extractor that can compute the witness by observing how the proof was generated. A protocol asking whether Alice holds a key needs that stronger property, and the chapter warns that the higher-level protocol must handle malleable or replayed proofs, since Alice could otherwise present a proof someone else generated. Zero knowledge and succinctness are defined as separate properties.
In a PLONKish configuration, fixed columns hold configuration constants, advice columns hold the witness, and instance columns hold public inputs, while custom gates reach cells at offsets from the row where their selector is set. The chips chapter explains that offset references cut the number of columns and therefore proof size, at the price of making row order significant. Each chip must place its offset gates correctly within a region, and a separate floor planner chooses the row where each region starts, so gadget-level code need not handle relative references or layout directly. The authors intend this separation to make code easier to audit, which still leaves the circuit's author answerable for whether the chips together encode the intended relation.
The practical sections bring that question down to a small circuit, which constrains a fixed constant times the squares of two private values to equal a public output. On the developer tools page, MockProver takes assignments prepared as for a real proof, checks them directly against every constraint the author wrote, and reports which constraint failed. A passing run shows that the written constraints hold for those inputs and is silent about conditions nobody wrote down. The example also alters the public output and expects failure. Negative tests of that kind can expose an omitted constraint, though no collection of them guarantees that every omission has been found.
Omission is also the hazard behind the implementation notes on proofs, which describe halo2 proofs as opaque byte streams with no concrete Proof struct. These streams are created and consumed through the TranscriptWrite and TranscriptRead traits, whose implementations must write to or read from a buffer while hashing each component into the transcript. That coupling guards against placing data in a proof structure that never enters the transcript. The authors also observe that verification thereby accounts for deserialization, which point compression keeps from being negligible.
On the commitment side, the inner product argument opens a committed polynomial with logarithmic communication, yet computing the commitment G still requires a multiexponentiation whose length grows linearly with the polynomial. The recursion section, which closes the background material, defers that check. A verifier circuit witnesses G and exposes it, together with the round challenges, as public inputs. The next instance checks it with logarithmic work and inherits a new G' with fresh challenges. The deferral continues until one linear-time computation decides the whole batch. Over a cycle of curves, a proof produced on one curve can be verified efficiently in a circuit over the other, while some checks are deferred to the next native circuit.
The proving system overview says its protocol description will likely be replaced by the Halo 2 paper and security proof. A TODO marks where the components providing zero knowledge should be written up, and a user tutorial on lookups is also incomplete. These gaps describe how complete the documentation is and say nothing about whether the system has a security proof or provides zero knowledge. The book fits developers who are comfortable with Rust, finite fields, polynomials, and elliptic curve notation, who write or review halo2 circuits, and who need to trace each constraint to its cost and guarantee.