Comment by lumost

TLA+ doesnt prove the code. if they never read the proof, then how do we k ow that it proved the right things?