<k​ayabanerve:matrix.org> We need a formalized spec of the key gen (possibly already present in MRL-000X?) and the signing protocol. That would need proofs on top of it.