After working on a few non-trivial medium-to-long length TLAPS proofs, I encountered a general issue where certain proof obligations that passed without issues during the initial verification process would fail when the module was rerun without caches to reproduce the proof verification. The failure of these proof obligations was non-deterministic, exhibiting unpredictable changes across different systems, and even on the same system across different runs without proof caches. Most of these failing obligations were deeper down in the proof (1500-2000+ lines into the proof), and the issues seemed to be easily resolvable. In my experience, I managed to resolve all such issues within minutes, most within seconds. I have observed two groups of failing proof obligations:
Most failing proof obligations can be easily verified by running at the leaf level.
Others can be made to pass by specifying a back-end and a timeout duration (e.g. specifying SMTT(5), the first back-end when no back-ends are specified, which is invoked with a 5-second timeout by default, can make a difference), or contrarily removing the specified back-end/timeout if there is one.
In the Google Group post, @muenchnerkindl mentioned that this was a long-standing problem, suspected to be caused by an issue with handling timeout in the context of parallel checking.
This issue is in reference to my post in the TLA+ Google Group on Feb 3, 2023.
After working on a few non-trivial medium-to-long length TLAPS proofs, I encountered a general issue where certain proof obligations that passed without issues during the initial verification process would fail when the module was rerun without caches to reproduce the proof verification. The failure of these proof obligations was non-deterministic, exhibiting unpredictable changes across different systems, and even on the same system across different runs without proof caches. Most of these failing obligations were deeper down in the proof (1500-2000+ lines into the proof), and the issues seemed to be easily resolvable. In my experience, I managed to resolve all such issues within minutes, most within seconds. I have observed two groups of failing proof obligations:
In the Google Group post, @muenchnerkindl mentioned that this was a long-standing problem, suspected to be caused by an issue with handling timeout in the context of parallel checking.