An AI-written BLAKE3 fork ships proofs and mutation tests, and says no human has read it line by line

The README describes a fork of official BLAKE3 1.8.7 for 64-bit Arm and x86-64 and says: "AIs wrote it under Zooko's direction, and no human has reviewed it line by line or audited it." The README names Zooko among BLAKE3's designers. In place of review, the project lists symbolic-execution proofs that each assembly kernel matches a written specification, more than 2,000 small mistakes planted in the Rust code that the tests must each catch, official test vectors, a startup self-test, and guard pages beside every input and output buffer.

QUALITY.md says these checks found eight bugs, all fixed. Examples it gives: an Arm kernel that produced the wrong digest for the shortest messages, and Intel and AMD batch assembly that read past the end of an input. It says the proofs found no bug in the Arm kernels, but did find mistakes in some of the tools and models used to build the proofs.

The document also lists what stays unverified. The proofs trust the written specification, the instruction models, the Z3 prover and each kernel's stated memory and calling convention. Nothing checks that the unsafe Rust keeps Rust's aliasing rules under every thread interleaving. We did not run the proofs or the tests, and the speed claims are the authors' own. The repository showed 10 stars and a 0.9.0 release when we read it.

Why it matters: If nobody reviews the code, the checks have to do the reviewing, and this project writes down which checks it uses and what each one takes on trust. That list of trusted parts, and the finding that the proofs' own tooling contained mistakes, are a template for documenting any machine-verified output. Every claim here comes from the project's own documents and nobody outside it has audited the code, so read it as a design to study, not as evidence that the approach works.