The official basics page is the cleanest current high-level source: it frames Binius as a binary-field proof system, says Binius64 is optimized for 64-bit-word proving, highlights transparent/hash-based design, and explicitly points readers to the blueprint, docs, benchmarks, and codebase.
The public README is the strongest concise implementation-facing source for the Binius64 mechanism itself. It says arbitrary computations are expressed as non-deterministic circuits over 64-bit words, explains the shifted value indices design, and makes the CPU-performance target explicit.
The blueprint matters because it shows Binius64 is not one undifferentiated proving trick. It separates AND-constraint checking from MUL-constraint checking and says both reduce to a shared shift-reduction target. That decomposition is one of the main reasons Binius belongs in the active corpus.
The announcement post is useful not just for launch context but because it states the product-level design choice most clearly: Binius64 moves away from the earlier VM-oriented and hardware-oriented stack toward a circuit-first, CPU-first proving system. It also explicitly says zero knowledge, more succinct verification, and proof composition are still on the roadmap, which helps avoid overstating current maturity.
The ePrint Polylogarithmic Proofs for Multilinears over Binary Towers is the most useful foundational research source in this pass. It makes the binary-tower-field commitment agenda legible beneath the product surface and gives a better explanation for why Irreducible treats bit-valued multilinears and tiny-field commitments as the key lower-layer lever.
The benchmarks page is worth keeping as a source, but carefully. It is useful for seeing what workloads the team thinks matter in practice — signature aggregation and hash-heavy proving — and for comparing proof size / witness / proving / verification metrics across CPU targets. It should not be treated as a neutral benchmark authority, especially because the launch post itself notes earlier methodology issues in some comparisons.
Why this entry belongs in the corpus
Binius gives the corpus a lower-layer proving-system comparison point beneath zkVMs and prover networks already cataloged.
It makes a useful mechanism split explicit: binary-field arithmetic, 64-bit-word-native constraints, AND-versus-MUL backend separation, and transparent hash-based commitments rather than generic fast proving rhetoric.
The durable insight is that proving performance and control can shift downward into arithmetic choice, constraint vocabulary, and CPU-oriented implementation strategy long before they show up as a zkVM, prover market, or branded app platform.