- **[dalek-ed25519-verified](https://zkdefi.org/saymrwulf/dalek-ed25519-verified)** — machine-checked proofs, in Lean 4, that the ed25519 code everyone ships is correct. Three production forks get the same treatment ([Solana](https://zkdefi.org/saymrwulf/anza-ed25519-verified), [RISC Zero](https://zkdefi.org/saymrwulf/risc0-ed25519-verified), [Betrusted](https://zkdefi.org/saymrwulf/betrusted-ed25519-verified)).
- **[verifying-crypto-with-lean](https://zkdefi.org/saymrwulf/verifying-crypto-with-lean)** — the 106-page book that teaches you to read (and extend) those proofs, from `1+1=2` up.
- **[swisspost-evoting-go-poc](https://zkdefi.org/saymrwulf/swisspost-evoting-go-poc)** — Switzerland's federal e-voting protocol, distilled from 500K lines of Java to 52 Go files.
- **[crisis](https://zkdefi.org/saymrwulf/crisis)** — DAG-BFT consensus by virtual voting, with a ten-chapter slow-motion visualizer.