Verifying Safety Properties With the TLA+ Proof System

Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh, UK. |

% This was essentially a progress report on the development of the TLAPS proof system. I believe it describes the state of the system, largely implemented by Chaudhuri, at the end of his post-doc position on the project.