The first post-quantum leaf — our public notary book now speaks two languages
Here is the problem in one sentence: the digital signatures that protect almost everything today — your banking app, software updates, this very website — are expected to break if large quantum computers arrive.
The cryptographers' answer is a new generation of signature schemes designed to survive that. One of them, standardized by the US government as FIPS 205 and called SLH-DSA, is built entirely out of hash functions — mathematical meat grinders that are boring, old, and very hard to run backwards, quantum computer or not.
But a standard on paper is not the same as a program that gets it right. Programs have bugs. So we took a real, deployed implementation of SLH-DSA (written in Rust), translated the part that checks signatures into the language of a proof assistant called Lean, and then did something no amount of testing can do: we proved — in the mathematical sense, checked by a machine that refuses to be charmed — that this code accepts a signature exactly when it should, and never otherwise. Eleven theorems, with the main one saying, in effect: "this program says yes precisely when the math says yes."
What that does and does not mean — because honesty is the entire product here. We proved the checking of signatures. We did not prove the making of them, and we say so in writing, everywhere. We proved the translated program, not the compiled chip-level artifact. And a few well-marked ingredients (the hash functions themselves) are assumed, not proven — the same way every proof in this whole project treats them. Every one of these boundaries is written into the public record next to the claim.
Which brings us to the notary book. Since July we have run a small public service: an append-only log — think of a notary's ledger where pages can be added but never torn out or rewritten — where we record entries of the form "this exact version of this software was formally verified, and here is the receipt." Anyone can clone it and re-check every page of the ledger on their own machine with one command — and what is on those pages we can never take back. That is the point.
Today that ledger grew from 13 entries to 19. Four entries re-record our ed25519 libraries at their much-stronger current state (that story is the companion post). One re-records the ledger's own internal mathematics. And entry 18 is the first post-quantum entry: the SLH-DSA verifier proofs, in the book, checkable by anyone.
And one more thing changed, quietly and maybe most importantly. Every page of the ledger is signed, so you know it came from us. Until now that signature used today's cryptography (Ed25519). From now on, every new page carries two independent signatures: the old one, plus an SLH-DSA signature — the very scheme whose verifier we just proved correct. If quantum computers eventually break the first signature, the second one still stands. Old pages keep their single signature — a ledger that never rewrites its past doesn't pretend it signed things it didn't — and our checking tool says so honestly instead of complaining.
The two public keys you need in order to check us are published in two independent places each, and the whole thing verifies with a stock Python and OpenSSL. Fifteen minutes, no PhD required:
git clone https://github.com/saymrwulf/lean-transparency-log cd lean-transparency-log && python3 verify.py --all
If that prints RESULT: OK [full] on your machine, you didn't take our word for the ledger — every page, signature, and receipt checked yourself. The proofs behind the pages you can replay from their pinned commits; until you do, our claim stands on the record, catchable. Which was always the goal.