02:31:19 <m-relay> <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.