TLA+ Proofs

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernan Vanzetto

Proceedings of the 18th International Symposium on Formal Methods (FM 2012), Dimitra Giannakopoulou and Dominique Mery, editors. Springer-Verlag Lecture Notes in Computer Science | , Vol 7436: pp. 147-154

This is a short paper describing TLAPS, the TLA+ proof system being developed at the Microsoft Research-INRIA Joint Centre.