saymrwulf

I verify the systems society uses to agree on things. Signatures, votes, certificates, money, consensus — built, accelerated, and increasingly machine-checked. Trust-systems engineering for institutions: the cryptographic substrate (PKI, HSM, PQC) that survives the move from operations to research and back.

The thesis has been the same for twenty years: how order arises from local rules in noisy adversarial networks, and what cryptographic primitives make that order legible to regulators, auditors, and downstream systems.

Start here

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, RISC Zero, Betrusted).
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 — Switzerland's federal e-voting protocol, distilled from 500K lines of Java to 52 Go files.
crisis — DAG-BFT consensus by virtual voting, with a ten-chapter slow-motion visualizer.

Where else

blog.zkdefi.org — one post per repo, the reasoning behind the code. Best reading order: blog post first, then repo.
zkdefi.com — the CV.

What this instance is

The authoritative mirror of every repository at github.com/saymrwulf, pulled every 24 hours, plus a daily reconciler for new repos. Issues are not mirrored — open them upstream on GitHub. If GitHub ever disagrees with this instance, this instance is the one I operate.