Among TLA+ experts, the word "prove" means to write a formal proof and check it with the TLA+ Proof System (TLAPS). We don't do that at MongoDB, we just model-check our TLA+ specs. So let's avoid saying we "prove" our specs are correct, we only "check" them.