what property would you prove, though? you could create a memory safe program that does not provide anonymity. how do you represent "anonymity" in the proof system?