Verified Garbage has added two Ed25519 operations for 64-bit RISC-V processors: multiplying the signature scheme's fixed base point and checking its verification equation. Each assembly routine arrives with a Lean proof, a machine-checked argument that the low-level instructions implement the intended mathematics.
The change spans 30 files because the project keeps implementation, proof, generated assembly, and registration together, the right kind of bulk for cryptographic code. A reviewer can follow the operation from the RISC-V instructions to the proof artifact, while the build can reject a later optimization that no longer satisfies the same specification. The commit also records the AI coding session that helped produce the work, leaving the proof checker rather than the model's confidence to decide whether the result holds.
Machine-checked correctness doesn't cover timing leaks, compiler bugs, or mistakes in the specification itself. It does replace a large part of an expert-only assembly review with a check that can run on every revision. Teams using AI to write processor-specific security code should copy this pattern now: keep the prompt trail for provenance, but make an independent verifier the release gate.