I mean, you could take anything as an axiom so there are no real requirements for it. I would imagine you would want to demonstrate the P(collision|domain+oper

I mean, you could take anything as an axiom so there are no real requirements for it. I would imagine you would want to demonstrate the P(collision|domain+operating lifetime) << acceptable level or risk, and after you’d done that, take the uniqueness of hashes as a axiom for the proof system? That’s just speculation on my part, since I haven’t done much with formal proofs of working code