Info

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.

Top User Comments

xgen-internal-githook commented on Fri, 22 Nov 2024 22:46:04 +0000: Author: {'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@emptysquare.net', 'username': 'ajdavis'} Message: SERVER-97559 Don't say we prove our TLA+ specs are correct (#29488) GitOrigin-RevId: 27a5342a5e0c92458c3447b4a0739aae82cd8809 Branch: master https://github.com/mongodb/mongo/commit/7c982b82dfa91d5e5597359adf86ca43f6e67cd9

Steps to Reproduce