The Go re-implementation of Swiss Post's e-voting protocol grew up — it now runs as mutually distrusting parties over Rust-signed transport, its return codes are genuinely cast-as-intended, and, the headline, every cryptographic operation renders itself as typeset mathematics with live values, the instant it executes.
The four ed25519 verification pyramids each ended their first post with an honest asterisk — the signature apex was proven at the byte level, and lifting it to the point level was deferred. That deferral is now closed, on all four forks: decompress is extracted and proven, the modular square root is proven, compress is canonical, and the acceptance criterion now reads as a real curve-point equation.
Verification of the Pallas field layer in zcash/pasta_curves — Montgomery-form 4×64-limb arithmetic, with the 255-bit modulus's primality machine-checked via a Lucas/Pratt certificate. A do-over of an earlier attempt that axiomatized exactly the statements that needed proving.
The third target of the ed25519 verification family - RISC Zero's curve25519-dalek fork (v4.1.3), the one that runs inside zkVM guests. A ZK proof attests that code ran; it does not attest that the code is correct. These certificates cover the half the SNARK can't.
A ground-up reimplementation of Switzerland's official internet voting cryptographic protocol as a single Go binary. The reference production system is 14 Java repositories, 500K+ lines of code, and requires 50 GB of RAM. This distills the cryptographic core into 52 files and 2 dependencies.