Saksam is right about improvements to provers often breaking some
proofs. However, I'm afraid that people may find more previously
successful proofs breaking than they should. This is because there
were bugs in the previous version that could have allowed TLAPS to
prove false assertions. Fixing those bugs has made it not prove some
things it used to. We believe it is unlikely that any assertions
people actually proved with the previous version were not true.
However, if you find that this did happen, please send us the proof in
which it did. We will add it to our regression tests to help us
make sure that those bugs do not reappear.
We apologize for this, and we are working to make the prover again
prove the correct assertions that it used to.
Leslie