Proofs about the code inside the prover — RISC Zero's dalek fork, verified
There's a category error hiding in a lot of zkVM enthusiasm: the proof attests execution — this binary, on this input, produced this output. It attests nothing about whether the binary means what you think it means. If the ed25519 verify inside your guest accepts signatures it shouldn't, the zkVM will happily produce an unimpeachable proof that the wrong thing ran correctly. Soundness of the wrapper, garbage in the core.
RISC Zero guests that check ed25519 signatures use RISC Zero's own fork of curve25519-dalek (v4.1.3, patched for the guest environment). This repo gives that fork the same treatment as the rest of the family: pinned source snapshot (risc0-curve25519-dalek-source), Charon/Aeneas extraction to Lean 4, and the full pyramid proven about the extracted code — 𝔽ₚ field arithmetic at radix 2⁵¹, the complete twisted-Edwards group law, scalar arithmetic mod ℓ, and the EdDSA acceptance criterion as the apex certificate, axiom cone audited by the build down to the named SHA-512/wire-format boundary.
Composed with the zkVM's own guarantee, the two halves finally say something whole: the SNARK says this code ran; the Lean certificates say this code is the acceptance criterion of EdDSA. Neither claim substitutes for the other, and the gap between them is exactly where "we use ZK, we're safe" hand-waving lives. My zk-perp DEX runs signature checks inside a RISC-Zero guest, so this wasn't an abstract itch — it's the missing assurance layer under something I'd already built and blogged here.
The fork angle compounds the zkVM angle. A guest-patched crypto library is a fork optimized under pressure — cycle counts inside a prover are expensive, and pressure is where semantics quietly bend. The proofs went through against the extraction of the patched source, which is the strongest statement available that the guest optimizations preserved the math. Where the family's proofs needed target-specific adjustment, the adjustments themselves document the drift.
Fourth target, same discipline: nothing in the repo that doesn't compile, no status-table claim without a passing verification/check.sh, and the open frontier (byte-level to point-level lifting) stated in the README rather than implied away.