Verifying Solana's ed25519 — same theorems, different codebase
Solana doesn't run upstream curve25519-dalek. It runs Anza's own crate, solana-ed25519, forked and maintained for the validator's needs. Every signature that moves value on that chain goes through this code. So a natural question: does the correctness argument for upstream dalek transfer? And the uncomfortable, obvious answer: formally, no. A theorem about one codebase says nothing about a different codebase. "It's basically the same code" is a claim about diff sizes, not about semantics — and diffs against the upstream is exactly where a fork's own bugs live.
This repo is the honest version of the transfer: the entire pyramid from dalek-ed25519-verified, rebuilt from scratch against Anza's source. Its own pinned snapshot (anza-cryptography-source), its own Charon/Aeneas extraction, its own gen/ tree, its own compiled certificates, its own axiom audit. Field 𝔽ₚ at radix 2⁵¹, the complete twisted-Edwards group law, Scalar52 arithmetic mod ℓ, and the EdDSA acceptance criterion at the apex — each proven about the Lean image of Solana's Rust, with the build failing unless the apex axiom cone is exactly the documented SHA-512/wire-format boundary and nothing else.
Doing it four times (upstream, Solana, RISC Zero, Betrusted) turned out to be its own experiment in proof engineering. The theorem statements are morally identical; the proofs are not copy-paste, because each extraction carries its fork's little differences through to the Lean side. Where the proofs went through unchanged, that's evidence the fork preserved semantics. Where they needed adjustment, the adjustment is a precise map of where the fork actually diverges — a diff at the level of meaning rather than lines. I know of no cheaper way to get that map, and "cheap" here still meant a serious campaign per target.
The supply-chain framing is the one I'd defend in a design review: if your system's security reduces to a fork of a well-studied library, your assurance story has a hole exactly the shape of the fork delta. This closes that hole for one fork, at the arithmetic-and-verify layer, mechanically, with the axioms enumerated. Not more, not less.